Improve history thread ID may_create

[sim642]

The may_create function for our history-based thread IDs from the ESOP paper is quite conservative.
After thinking about it for a while (in comparison to is_must_parent, I noticed many cases where may_create can be more precise and incrementally implemented them here.

I haven't constructed programs where all these thread IDs and their improvements would actually show up and matter, so these may be very obscure (or even infeasible for some other reasons I didn't notice).
Also, I'm not sure if it is now optimal, possibly not yet in the "both are non-unique" case.

TODO

• Add unit tests.
• Add regression tests.
• Rename the two functions.
• Make prefix list un-reversed? Being reversed is only useful for efficient "appending", but the prefixes should be very short. Reversing those lists for various predicates (which may be called many times) might be the more overwhelming inefficiency.
• Benchmark for (unlikely) precision improvement or performance regression.
• From GobCon: consider over-approximated $$C$$ implications.

[michael-schwarz]

I wonder how often (if at all) any of this actually hits: As soon as the creator is not the must-parent, it's already game over:

analyzer/src/cdomains/mHP.ml

Lines 55 to 60 in b9caf63

	let definitely_not_started (current, created) other =
	if (not (TID.is_must_parent current other)) then
	false
	else
	let ident_or_may_be_created creator = TID.equal creator other || TID.may_create creator other in
	if ConcDomain.ThreadSet.is_top created then

[sim642]

Indeed, since those are our only usages of must_be_parent and may_create, they might not and I didn't consider that so far.
Although there we require current to be must parent, but creator is checked for may_create. The naming in the code is maybe a bit confusing, because creator (from $$C$$) is created by current.

I did a test run with coverage locally and (even to by surprise) all lines and branches are covered. But the actual usefulness of this will become clear when I try to construct regression test programs around these hypothetical improvements.

[sim642]

I managed to simplify and optimize it to something reasonable by using a simple (but efficient) GobList.remove_common_prefix function. The old way of checking of p is a prefix of p' was

P.equal p (P.common_suffix p p')

which is very roundabout: it constructs the common prefix (via list reversals) just to check for equality (which goes through the entire list again).

In many cases the check

S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s')

does capture everything that's needed, but it's far from obvious that it's all that's needed (for optimality).
By using information from checks (e.g. s is empty, or p is prefix of p' or vice versa) and well-formedness (p has unique elements, and p and s are disjoint), a lot less needs to be actually checked – in some cases nothing at all!

---

I've now realized that the naming of the two functions is also a bit weird. I would rename:

1. is_must_parent → must_be_ancestor because in standard terminology parent means immediate,
2. may_create → may_be_ancestor to make naming uniform.

[sim642]

I went through all the unit tests for the improved cases and tried to construct a real program for each one. Five of them have a corresponding regression test now that also checks for the improved precision from this. For others I documented why a real program for data race regression testing at least isn't possible.
There may be a use for may_create in the future that doesn't guarantee is_must_parent checks before it. And even for the time being, the change to may_create cannot even harm performance because in those cases the new logic isn't used anyway.

[sim642]

A before vs after benchmark run on SV-COMP ConcurrencySafety with 60s timeout gives zero verdict differences and performance differences are also just within measurement noise.

As to the over-approximated $$C$$ sets, I don't see how it would matter: this predicate even doesn't use it. The only place in thread spawning where it does matter is thread creation in a loop, where main could directly create main, {foo} (not just main, foo). But as these thread IDs, main, {foo} could equivalently be created by main, foo recursively. Since both predicates are about ancestors (not immediate parents), this shouldn't matter. main is considered both must and may ancestor of main, {foo}.

[michael-schwarz]

I saw you have a pending thesis on verifying the correctness of this. Do we want to wait for this or should I attempt to review it such that we can then merge it?

[sim642]

I offered a thesis topic on formally verifying this but there's no student working on it (and I'm not sure if there ever will be), so we shouldn't wait for that. I've left a lot of comments for the various cases along with tests, so I hope that's sufficiently clear and convincing that this should be right.

[michael-schwarz]

Why this comment?

[sim642]

I think the reason was that there are at least two improvements after that commit (dbd4874 and c2c596f) which are supposed to improve precision, but they're not observed by the tests. That might possibly be related to the other unit test TODOs about certain cases being untestable by construction.
Since then I refactored the code, so perhaps it's no longer true. At least according to code coverage, all cases seem to be covered by something.

[michael-schwarz]

Then we can maybe just remove the comment?

[michael-schwarz]

What is the plan with this TODO?

[michael-schwarz]

What is the plan with this TODO?