Abstract

Abstract: Concurrent separation logic is a Hoare-style logic for safe partial correctness of shared-memory parallel programs that operate on mutable state. In prior work we gave a denotational semantics, based on action traces, whose structure directly reflects the underlying RAM model, and we used the semantics to establish soundness of this logic. Later work by Calcagno, O`Hearn and Yang introduced a more general class of state models called separation algebras, designed to abstract away from the RAM and other specific models used elsewhere in work on separation logics. They formulated a notion of local action, represented mathematically as a (non-deterministic) state transformer that mutates state in a local manner. They gave a trace-based semantics, and an abstract version of separation logic, interpreted over arbitrary separation algebras. A major aim of their work was to formulate a semantic model that made ``locality`` explicit in a general, widely applicable manner. Their semantic construction makes several different design choices in contrast to the RAM -based action traces model, leading to some quirks in the modelling of parallel composition. In this paper we present a more straightforward way to design an action trace semantics based on local actions, leading to an elegant generalization of our prior model that makes sense over arbitrary separation algebras. The new model can easily be extended (by incorporating infinite traces) to support reasoning about safety and liveness properties, including safe total correctness, in addition to safe partial correctness. The model can also be seen to embody Dijkstra`s Principle, that loosely coupled processes should be regarded as independent, except at synchronization points. The adjustments are rather natural, and our semantics can also be used to offer a general soundness proof of abstract concurrent separation logic.