On Locality and the Exchange Law for Concurrent Processes

Abstract: This paper studies algebraic models for concurrency, in light of recent work on Concurrent Kleene Algebra and Separation Logic. It clarifies that there is a strong connection between the Concurrency and Frame Rules of Separation Logic and a variants of the excahnge law of Category Theory. The algebraic laws admit two standard models: one uses sets of traces, and the other is state-based, using assertions and weakest preconditions. We relate the latter to standard models of the heap as a partial function. We exploit the power of algebra to unify models and classify their variations.