On Grainless Footprint Semantics for Shared-memory Programs

We develop an improved grainless denotational semantics for shared-memory parallel programs, building on ideas from earlier trace-based models with local states and footprints [S. Brookes. A Grainless Semantics for Parallel Programs with Shared Mutable State. Proc. 21st Conference on Mathematical Foundations of Programming Semantics (MFPS XXI). Birmingham, 17–21 May, 2005]. The key new idea is a more refined approach to race detection, leading to a model with better abstraction properties. Rather than treat a race condition as a “global” catastrophe [S. Brookes. A Semantics for Concurrent Separation Logic. Invited paper, CONCUR 2004, Philippa Gardner and Nobuko Yoshida (Eds.), Springer LNCS 3170, London, August/September 2004, pp. 16–34; S. Brookes. A Grainless Semantics for Parallel Programs with Shared Mutable State. Proc. 21st Conference on Mathematical Foundations of Programming Semantics (MFPS XXI). Birmingham, 17–21 May, 2005], we track information about variables whose value may be tainted by a race, and retain accurate information about unaffected variables. As in the prior work, we abstract away from state changes that occur in between synchronization points, in a manner consistent with Dijkstra's Principle [E. W. Dijkstra. Cooperating sequential processes. In: Programming Languages, F. Genuys (editor), pp. 43–112. Academic Press, 1968]. We obtain a model in which only synchronization operations (for locking and unlocking binary semaphores) are deemed to be atomic, which matches the usual implementation of these constructs in an abstract manner. Apart from this, no other atomicity assumptions are made, so our model is truly grainless. Our semantics supports compositional program analysis based on “sequential” reasoning for sequential code fragments, even when this code occurs in parallel contexts, and yields a simple semantic characterization of race-free code. The semantics validates the static constraints on “critical variables” imposed in concurrent programming methodology [C.A.R. Hoare. Towards a Theory of Parallel Programming. In Operating Systems Techniques, C.A.R. Hoare and R.H. Perrott, editors, pp. 61–71, Academic Press, 1972; S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach, Comm. ACM. 19(5):279–285, May 1976] and serves as a foundation for reasoning about safe partial correctness, as in concurrent separation logic [P.W. O'Hearn. Resources, Concurrency, and Local Reasoning. Invited paper, CONCUR 2004, Philippa Gardner and Nobuko Yoshida (Eds.), Springer LNCS 3170, London, August/September 2004, pp. 49–67]. The new treatment of race detection allows for more refined analysis of racy programs. By framing our ideas and concepts in a general manner we hope that our results may be applied in a wider setting