A Grainless Semantics for Parallel Programs with Shared Mutable Data

We provide a new denotational semantic model, based on “footstep traces”, for parallel programs which share mutable state. The structure of this model embodies a classic principle proposed by Dijkstra: processes should be treated independently, with interference occurring only at synchronization points. As a consequence the model makes fewer distinctions between programs than traditional trace models, which may help to mitigate the combinatorial explosion triggered by interleaving. For a sequential or synchronization-free program the footstep trace semantics is equivalent to a non-deterministic state transformation, so the new model supports “sequential” reasoning about synchronization-free code fragments. We show that footstep trace semantics is strictly more abstract than action trace semantics and suitable for compositional reasoning about race-freedom and partial correctness. The new model can be used to establish the soundness of concurrent separation logic. We include some example programs to facilitate comparison with earlier models, and we discuss briefly the relationship with a recent model by John Reynolds in which actions have discernible starts and finishes.