On locality and the exchange law for concurrent processes

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