Restore irept sharing

[NathanJPhillips]

A PR by @reuk some time ago prevented sharing when references are held to sub-parts but didn't re-enable sharing in situations where it is actually safe to do so. This PR amends that.

This should improve performance, particularly in memory usage.

[smowton]

@reuk perhaps you'd like to give an opinion, even if you're unable to contribute code at the moment?

[smowton]

Looks good!

[smowton]

@martin-cs I know you've done memory profiling of cbmc before, do you have any opinion on the importance of irep sharing?

[NathanJPhillips]

@tautschnig - I believe you may have some performance tests. Could you check that this improves performance? If it doesn't then something has gone wrong.

[tautschnig]

tl;dr I'm wondering whether #1742 should just be reverted?

1. Apart from the fact that AppVeyor shows that this isn't quite right, why do we need changes to expr.{h,cpp}? This must be about irept only as otherwise it is no longer safe to inherit from irept.
2. The test seems really useful, but what is it that actually is broken right now?
3. Which change specifically (among those in Owen jones diffblue/small shared ptr #1742) was it that caused the problem?

We had a data structure that lived nearly untouched for about 15 years. And now we have to touch it for a second time in a fairly short time frame. That's not a way of earning trust.

[smowton]

The breakage: functions that leak non const references to sub structures (whether the operands vector or a sub-irep in that vector (or the named sub etc)) forbid sharing the irep, for fear those references could have been retained and then used to mutate a shared irep without causing a CoW break. This introduces some utilities that perform some useful mutation and then drop all references to internals (eg. add-to-operands), so they can safely leave sharing enabled for the mutated irep.

[kroening]

I'd go for reverting #1742 for the moment. The proposed change can live as a branch for some time, until we've done proper benchmarking.

[tautschnig]

In line with what @kroening said I'd propose:

1. Add the unit test from this PR to the repository and, as will prove necessary, revert the main commit of Owen jones diffblue/small shared ptr #1742. That's now in preparation in Revert irept change that stopped sharing and add unit test #1860.
2. Cherry-pick the commit of Owen jones diffblue/small shared ptr #1742 into this PR to re-instantiate those changes, and then fix them within this PR.

This will enable us to get back to a known-good baseline, even though it might not be as safe as what #1742 had provided. From that baseline we can then try to get to a solution that is also safe.

The unit test is a pretty big win of this process as it will ensure that we stay on a good route.

[NathanJPhillips]

tl;dr

131 lines, of which 60ish were a unit test?

I'm wondering whether #1742 should just be reverted?

I've addressed this idea on #1860

Apart from the fact that AppVeyor shows that this isn't quite right,

The error there doesn't make sense to me yet, anyone got any helpful pointers on how to address it?

why do we need changes to expr.{h,cpp}? This must be about irept only as otherwise it is no longer safe to inherit from irept.

exprt was unnecessarily using irept methods that are not safe to use in conjunction with sharing. I updated it to use irept methods that are safe to use with sharing.

The test seems really useful, but what is it that actually is broken right now?

The test asserts that sharing can be maintained whenever it is safe and not when it isn't safe.

We had a data structure that lived nearly untouched for about 15 years. And now we have to touch it for a second time in a fairly short time frame. That's not a way of earning trust.

Addressed in my comment on #1860

[tautschnig]

exprt was unnecessarily using irept methods that are not safe to use in conjunction with sharing. I updated it to use irept methods that are safe to use with sharing.

I thought it was now impossible to use methods that are unsafe to use in conjunction with sharing?

[NathanJPhillips]

exprt was unnecessarily using irept methods that are not safe to use in conjunction with sharing. I updated it to use irept methods that are safe to use with sharing.

I thought it was now impossible to use methods that are unsafe to use in conjunction with sharing?

You can use them, but they break sharing! Sorry for my bad explanation. If we don't alter exprt then it will use irept methods that are not sharing-safe in its methods that should be sharing-safe. To allow those exprt methods to be used with the maximum possible sharing they had to be rewritten in terms of irept methods that allow sharing to continue.

For example, you can add an operand as a single operation that doesn't leak any references that could later be updated, so this is sharing-safe, but if you implement it in terms of operands(), which calls get_sub(), the latter method has to mark the irept as no longer safe to be shared.

[martin-cs]

@smowton : memory profiling and sharing. Sharing is vital; we need it and it must work correctly and efficiently.

[martin-cs]

This looks nice in a "use the API, not the internals" kind of way.

[martin-cs]

This rather suggests that the semantics of "move" and "copy" are the same, which, for a reference counted thing, is ... a little concerning.

[NathanJPhillips]

The difference is that copy takes its argument by value and moves the copied value into the operands. If I was rewriting the API I'd have a single call that took by value and allowed you to move or copy into that but this PR isn't to update the API.
Let me clarify this with example code:
Preferred API:

void add(value by_value) { impl.add(std::move(by_value)); }
// Usage
value value;
add(value);  // Copies value in, the copy is moved into the internals
add(std::move(value));  // Moves value in, which is then moved again into the internals

Existing API:

void copy(value by_value) { move(by_value); }
void move(value &by_ref) { impl.add(std::move(by_ref)); }  // Interface left over from pre-std::move days
// Usage
value value;
copy(value);  // Copies value in
move(value);  // Moves value in without std::move at call site :/

[NathanJPhillips]

Added comment line to draw attention to the copy by value in the arguments.

[martin-cs]

I guess I was thinking about the impact on reference counting.

[NathanJPhillips]

The pass by value in the argument causes an increase in the reference count. The move version doesn't have the copy caused by the pass by value and so doesn't increase the reference count. Another comment required to say this?

[martin-cs]

The flag is kinda critical; any chance of some documentation for it?

[NathanJPhillips]

The documentation is now in the header file.

[NathanJPhillips]

The AppVeyor crash was caused by existing unsafe behaviour in CBMC shown up by this optimisation - this is fixed by #1896 and cherry-picking that commit into this PR (just until that PR is merged) has fixed the problem.

[NathanJPhillips]

@tautschnig - this PR is now rebased on the head of develop that includes the fix that was causing AppVeyor problems and so is passing CI. How are you feeling about moving forwards with this, having had a couple of weeks to consider it? Are your initial objections satisfied or do you want to keep a request for changes review on this?

[tautschnig]

What's the urgency on this one? I'm happy to be overridden if there is a pressing need to get this merged in the next days. Otherwise I'd like to take a detailed look in the second half of next week, if that's ok?

[NathanJPhillips]

I'd rather you had a detailed look. We'll wait for you.

[NathanJPhillips]

@tautschnig - still no urgency but a little reminder to look at this when you get time.

[tautschnig]

My apologies for having been quiet about this. In my opinion, the following needs to happen:

1. Revert Owen jones diffblue/small shared ptr #1742.
2. Introduce unit tests that effectively act as specification of how an irept is expected to behave.
3. Implement improvements (such as Owen jones diffblue/small shared ptr #1742) while not breaking any of the then-existing unit tests.

#1860 partly addressed 1 and 2; I have started working on more unit tests. I'll try to get this done ASAP.
This PR should then bring in #1742 again, together with the fixes that are in here, to address item 3.

Problems must be fixed by first rolling back - rolling forward is not a way to address bugs introduced in a particular change.

[NathanJPhillips]

That way ahead won't work - even after this PR there will be less irept sharing than was there before #1742. In fact there are potentially more changes you could make after this one to increase sharing further if you could accept an irept-reference-wrapper type interface to methods like op0().
If you can't accept any decrease in sharing then you're stuck with the version that allows possibly incorrect behaviour by leaking references to shared irept's. If you can then there's no need to revert. You have a choice between two "buggy" versions, one that increases memory use or one that allows incorrect behaviour.

[tautschnig]

You have a choice between two "buggy" versions, one that increases memory use or one that allows incorrect behaviour.

Yes, I am aware of that choice, but they have different impact: one necessarily affects the customer through increased memory usage, while the other one just requires more care by developers. In my world, it's always about the customer.

[tautschnig]

@NathanJPhillips While this proposal addresses some bugs, I am worried about the fact that these went undetected before (in particular in the performance test that I did myself). Of course you've added a nice unit test to put checks in place, but could you please explain how you noticed the problem in the first place?

[NathanJPhillips]

It was while writing unit tests for the mutable extension to the depth-first iterator. I needed to check that the mutate operation had broken sharing so that we were mutating a new copy but in doing so I put a sanity check up front that sharing was already in place and noticed it wasn't.

[NathanJPhillips]

I still find it really weird that you keep calling the intended behaviour of a PR that you approved a bug. You can say that you didn't understand the intended behaviour and that you think that behaviour is undesirable, but a bug to me implies something unintentional. #1742 intentionally broke sharing in order to make things safer.

[tautschnig]

Yes, I did not understand the intended behaviour; the unintentional part about it is that I was not expecting that failure to understand.

[tautschnig]

Quoting from #834: "The observable effect of this patch is that code such as the following no longer has unexpected behaviour." -- so that's what I expected to be the observable effect; it did not say that "less sharing" was among the observable effects/intended behaviour.

[tautschnig]

I am attaching the heap profiles of current develop (5cbb758), this PR rebased against 5cbb758, and 1860 (also on top of 5cbb758). The test run is the same as #1971 uses, and the diff tool from #1971 might aid in the comparison.

[NlightNFotis]

Hello.

I am closing this PR as it appears stale and no longer in a viable state to be merged. If you would like this to be merged at some point in the future, feel free to reopen the PR and rebase on top of develop.