Concurrency and local reasoning under reverse exchange

• A relation-algebraic semantic model for true concurrency and separating conjunction.
• Proof of an exchange law between sequential and concurrent composition.
• Further semantic background, in particular on so-called precise program commands.
• Proofs of several variants of Hoare-style inference rules for concurrency and locality.
• Application of these rules in some examples.

Quite a number of aspects of concurrency are reflected by the inequational exchange law (P⁎Q);(R⁎S)⩽(P;R)⁎(Q;S) between sequential composition ; and concurrent composition ⁎. In particular, recent research has shown that, under a certain semantic definition, validity of this law is equivalent to that of the familiar concurrency rule for Hoare triples. Unfortunately, while the law holds in the standard model of concurrent Kleene algebra, its is not true in the relationally based setting of algebraic separation logic. However, we show that under mild conditions the reverse inequation (P;R)⁎(Q;S)⩽(P⁎Q);(R⁎S) still holds there. From this reverse exchange law we derive slightly restricted but still reasonably useful variants of the concurrency rule. Moreover, using a corresponding definition of locality, we obtain also a variant of the frame rule, where ⁎ now is interpreted as separating conjunction. These results allow using the relational setting also for modular and concurrency reasoning. Finally, we interpret the results further by discussing several variations of the approach.