Stephen Brookes
Carnegie Mellon University

A Grainless Semantics for Parallel Programs with Shared Mutable Data


Traditional models of shared memory parallel programs assume a fixed notion of granularity, for instance by treating integer reads and writes as atomic actions.  Such assumptions are unrealistic in practice, and program analysis based on fixed granularity models is of limited utility. These models also ignore race conditions, in which one process writes to a variable being used by another.  We describe a new semantic model, based on “footstep traces”. This semantics treats a potential race condition as a catastrophe, and embodies a classic principle proposed by Dijkstra:  processes should be “loosely coupled”, with interference occurring only at synchronization points. The model makes fewer distinctions between programs than traditional trace models, helping to mitigate the combinatorial explosion triggered by interleaving.  The footstep trace semantics of a synchronization-free program is equivalent to a non-deterministic state transformation, so the new model supports “sequential” reasoning about synchronization-free code fragments.  Footstep trace semantics is independent of granularity assumptions, and more abstract than earlier models, yet suitable for compositional reasoning about race-freedom, partial correctness and total correctness.  The new model can be used to validate the soundness of concurrent separation logic, a resource-sensitive logic for reasoning about concurrent programs that manipulate pointers. The soundness proof shows that every provable program is race-free.

Friday, September 30, 2005
3:30 p.m.
Wean Hall 5409*

Principles of Programming Seminars