Concurrency and local reasoning under reverse exchange

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