Discussion: Better(?) Logically-Atomic Triples
Hey everyone, I am doing some groundwork on logical atomicity for weak memory and I got annoyed by the "current" definition of atomic triples:
- The quantification over the "real" precondition P seems unnecessary.
- The box around the shift is an artifact of working directly with (persistent) triples.
This is the reference definition of atomic triple (taken from @zhangz's iris-atomic@13900169bafb6b6ef1d091236dba493eaa25cc95):
∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
α x ∗
((α x ={Ei, Eo}=∗ P) ∧
(∀ v, β x v ={Ei, Eo}=∗ Q v))
) -∗ {{ P }} e @ ⊤ {{ Q }}.
I propose the following change:
atomic_shift Eo Ei α β Φ :=
|={Eo,Ei}=> ∃ x : A,
α x ∗
((α x ={Ei,Eo}=∗ ▷ atomic_shift Eo Ei α β Φ) ∧
∀ y, β x y ={Ei,Eo}=∗ Φ y).
atomic_wp Eo Ei α β := ∀ Φ, atomic_shift Eo Ei α β Φ -∗ WP e @ Eo { Φ }
It should be easy enough to derive a notion of logically-atomic triples (as opposed to weakestpre) the same way we derive normal triples.
I did some initial testing by porting iris-atomic/atomic_incr.v to this definition. Apart from some inconveniences regarding boxes in the client (orthogonal to logically-atomic triples; just a proof setup problem), the proof of the spec and the client remain mostly the same. One additional (albeit entirely trivial) Löb induction had to be introduced in the client to prove the atomic shift. The spec proof already had a Löb induction and so will almost any other proof of that kind I think.
You can see the changes to the proof here: janno/iris-atomic@06d9dc7d. The definition is here: janno/iris-atomic@ba66f8bd.
Before I continue to work with this new definition in my own development I would like to gather feedback. What does everyone think of it?
I am specifically worried about examples that somehow manage to run out of steps and thus cannot get rid of the ▷
modality. I can't imagine what those would look like but they might exist. Additionally, the added complexity of requiring iLöb
in client proofs may be considered a substantial disadvantage of this definition by some.
P.S.: This is orthogonal to (and thus hopefully compatible with) the work on using telescopes to represent an arbitrary number of binders in atomic triples. I made some progress on that, too. But it's not done.