PoP Seminar Talk

A denotational framework for relaxed memory concurrent programs

Stephen Brookes, Professor of Computer Science at Carnegie Mellon University
Thursday, 05 October, 2023; 3:30pm
NSH 4305
Host: Jan Hoffmann

Abstract

We introduce a denotational framework for coherent relaxed memory models, in which executions guarantee that all threads “see” the writes to each individual variable in the same relative order. Each memory model also allows per-thread relaxation of the relative order of certain kinds of action. The semantics is “truly concurrent”, using partially ordered multisets of actions (pomsets), a natural generalization of traces. The semantic constructions, such as sequential and parallel composition, are parameterized by the memory model, embodied by a combination of a relaxation relation and a linearity guarantee. We focus on three historically important memory models: SC, TSO and PSO, which guarantee (progressively weaker forms of) coherence. For SC we recover the usual trace semantics familiar from traditional accounts. We illustrate how the semantic models work by examining litmus tests, small programs whose executional behavior differs across memory models. We discuss related work, and point the way to future developments.

Bio

Stephen Brookes is well known internationally for his seminal contributions to semantics for concurrent programs and logics for reasoning about program behaviour. He earned both his bachelor’s degree in Mathematics and his Ph. D. in Computer Science at Oxford University, joined Carnegie Mellon University as a research computer scientist in 1981, and has been a full professor there since 2006. His doctoral dissertation, supervised by Tony Hoare, was titled A Model for Communicating Sequential Processes. His work with Bill Roscoe led to the development of the failures-divergences model of CSP. Over the years Brookes has developed a trace-based framework for giving semantics to a range of parallel paradigms, including shared-memory, synchronous and asynchronous communication. His work on Parallel Algol shows how these ideas can be extended to deal with a language that combines concurrency with higher-order procedures. A long-term aim of his research has been to improve the design and analysis of correct concurrent programs. His recent work on Concurrent Separation Logic, in collaboration with Peter O’Hearn, is a major development in this direction. CSL supports correctness proofs for software that involves pointer manipulation and shared-memory concurrency, both notoriously difficult to get right. This work has had significant impact in both theory and in practice. Brookes and O’Hearn were awarded the 2016 Gödel Prize, given jointly by European Association for Theoretical Computer Science (EATCS) and the Association for Computing Machinery Special Interest Group on Algorithms and Computational Theory (ACM SIGACT). Currently, Brookes is working on truly concurrent semantic models for relaxed memory concurrency.