Add Owicki-Gries annotations

[maul-esel]

This PR adds Owicki-Gries annotations as proofs for concurrent programs, as well as algorithms to compute such annotations after verification.

---

🚧 This is work in progress 🚧

---

Specifically, we add:

• basic classes for describing and validating Owicki-Gries annotations.

• 2 algorithms for the construction of Owicki-Gries annotations:

  • a naive algorithm (which creates very large annotations, but can be useful as a baseline for comparison)
  • the empire automaton-based algorithm described in our POPL'26 paper

  We previously implemented some other algorithm variants, but as they have been superseeded by the POPL'26 algorithm, they are no longer part of this PR. With one exception:

• a partial implementation of a refined algorithm based on directed empires: while not yet complete, this may be a promising base for future improvements to our Owicki-Gries computation.

• changes in backtranslation and correctness witness (v2.1) generation that allow us to output correctness witnesses for concurrent programs from Owicki-Gries proofs.

[matthiaszumkeller]

Thank you for preparing this merge. I added some additional comments.

[maul-esel]

In another project building of this work (branch wip/dk/civlized-og) we've just discovered a bug (or multiple bugs) that should be investigated and fixed before this is merged:

• With the attached file fork-join-01.bpl, the generated O/G proof seems to be insufficient: the invariant between fork and join does not contain any information about x, and thus the proof should be insufficient to show the assert.

  • In the project, we ask a deductive verifier to confirm the proof; and indeed it fails to do so because of this issue.

• Yet, no asserts fail. Do we not internally validate the proof when -ea is passed? Or is our validator defect?

• Also, inserting some blank lines in the program (fork-join-01.backup-bpl) seems to "fix" this problem: we get a stronger invariant, and the proof is confirmed by the external validator.

  Apparently, there is a nondeterminism bug (likely, inserting blank lines changes the line numbers of some actions, which changes their hashcode, and affects some hashset iteration order).

fork-join01.backup.bpl.txt
fork-join01.bpl.txt
settings.epf.txt
toolchain.xml

[schuessf]

With the attached file fork-join-01.bpl, the generated O/G proof seems to be insufficient: the invariant between fork and join does not contain any information about x, and thus the proof should be insufficient to show the assert.

Is it really necessary to have an invariant stronger than true between fork and join? In this example, we already have x == 1 as an invariant at the exit location of the thread, so I would expect this to be sufficient to show the assert in the main thread.

In the project, we ask a deductive verifier to confirm the proof; and indeed it fails to do so because of this issue.

Maybe the validator (or your modelling) has a different understanding of the join that allows more behavior?

Also, inserting some blank lines in the program (fork-join-01.backup-bpl) seems to "fix" this problem: we get a stronger invariant, and the proof is confirmed by the external validator.
Apparently, there is a nondeterminism bug (likely, inserting blank lines changes the line numbers of some actions, which changes their hashcode, and affects some hashset iteration order).

Still, we should investigate this nondeterministic behavior!

[matthiaszumkeller]

• With the attached file fork-join-01.bpl, the generated O/G proof seems to be insufficient: the invariant between fork and join does not contain any information about x, and thus the proof should be insufficient to show the assert.

  • In the project, we ask a deductive verifier to confirm the proof; and indeed it fails to do so because of this issue.

• Yet, no asserts fail. Do we not internally validate the proof when -ea is passed? Or is our validator defect?

We do check validity of the OG-proof internally and at least to me, the resulting proof seems valid wrt. the Petri net representation of the program. It is true, that no information about variable x is contained in the invariant between fork and join . However, for the transition representing the join in the Petri net, there are three predecessor places: {6#L13true,4#threadEXITtrue,threadThread1of1ForFork0InUse}. Two of them do not contain any information about x in their invariants, they ensure that the ghostvariable is set to the value 3 associated with the exit of the thread. However the third place (threadThread1of1ForFork0InUse) does contain xin its invariant, more specifically if ghost==3, then it ensures that the formula x==1 holds. Therefore, the transition corresponding to the join seems to satisfy inductivity and the postcondition contains the invariant x==1. Am I missing something, or are there any other validity concerns that I did not consider?

• Also, inserting some blank lines in the program (fork-join-01.backup-bpl) seems to "fix" this problem: we get a stronger invariant, and the proof is confirmed by the external validator.
  Apparently, there is a nondeterminism bug (likely, inserting blank lines changes the line numbers of some actions, which changes their hashcode, and affects some hashset iteration order).

I also think, that the non-deterministic behavior should be investigated.

Update:
I again looked at the output of the Ultimate toolchain for the program and it seems to be the case that the invariant of threadThread1of1ForFork0InUse is missing in the result after backtranslation. Maybe this could cause the issue?

[schuessf]

However, for the transition representing the join in the Petri net, there are three predecessor places: {6#L13true,4#threadEXITtrue,threadThread1of1ForFork0InUse}. Two of them do not contain any information about x in their invariants, they ensure that the ghostvariable is set to the value 3 associated with the exit of the thread. However the third place (threadThread1of1ForFork0InUse) does contain xin its invariant, more specifically if ghost==3, then it ensures that the invariant x==1 holds. Therefore, the transition corresponding to the join seems to satisfy inductivity and the postcondition contains the invariant x==1. Am I missing something, or are there any other validity concerns?

Oh, I see. So I guess we do not output the invariant for threadThread1of1ForFork0InUse if we consider the Boogie-program, since this location is just an auxiliary-location that does not belong to any location in the Boogie program. As a result, the annotation is valid for the Petri program but not for the Boogie program. I suppose we somehow still need to consider invariants at auxiliary locations during backtranslation.

This also seems to be the reason for non-determinism, it depends whether we put the invariant at threadThread1of1ForFork0InUse or 6#L13true.

[matthiaszumkeller]

This also seems to be the reason for non-determinism, it depends whether we put the invariant at threadThread1of1ForFork0InUse or 6#L13true.

Nice catch! I think that I found the location where the non-determinism occurs. In the legal focus, method chooseBestRegion chooses the smallest region (currently our only heuristics) that contains predecessor places of the transition to be focused. In this example, it can choose between those two regions [threadThread1of1ForFork0InUse], [6#L13true] (the third one contains two elements) and the regions are given as a set. If it is very inconvenient to also include the auxilliary places in the resulting backtranslation, we could maybe also filter regions with auxilliary places (that are predecessors of the transition) / adjust the comparator to choose another region if possible.

[schuessf]

Nice catch! I think that I found the location where the non-determinism occurs. In the legal focus, method chooseBestRegion chooses the smallest region (currently our only heuristics) that contains predecessor places of the transition to be focused. In this example, it can choose between those two regions [threadThread1of1ForFork0InUse], [6#L13true] (the third one contains two elements) and the regions are given as a set. If it is very inconvenient to also include the auxilliary places in the resulting backtranslation, we could maybe also filter regions with auxilliary places (that are predecessors of the transition) / adjust the comparator to choose another region if possible.

I guess we could check for the auxiliary places in the legal focus as a heuristics (even if it is not quite nice). But I am still wondering whether the loss of precision when omitting the invariants for auxiliary places a) only occurs in combination with the legal focus and b) could be always fixed with such a simple heuristics (which I am quite skeptical).

[maul-esel]

Thanks to both of you for investigating this! This explains why we could get a seemingly invalid annotation after backtranslation but not trigger an error before.

Let's maybe continue the discussion how to fix this in another channel to not overload this PR.