Stephen Brookes Will Receive Gödel Prize for Inventing Concurrent Separation Logic

Discovery Has Major Influence on Theory of Programming Languages

Stephen Brookes, Carnegie Mellon University professor of computer science, and Peter W. O’Hearn, engineering manager at Facebook and professor of computer science at University College London, will receive the 2016 Gödel Prize for their invention of Concurrent Separation Logic (CSL), a major advance in the design and analysis of programs that can take advantage of multicore and multiprocessor systems.

Brookes and O’Hearn, then a professor of computer science at Queen Mary, University of London, collaborated on developing CSL and introduced the ideas in separate papers published in 2007.

“My congratulations to Steve Brookes for winning the prestigious 2016 Gödel Prize together with Peter O’Hearn,” said Frank Pfenning, head of CMU’s Computer Science Department. “It is a fitting tribute to their fundamental scholarly work, which has had a tremendous impact on academic research in the theory of programming languages and is now beginning to have impact in industry.”

The Gödel Prize recognizes major contributions to mathematical logic and the foundations of computer science and is presented annually by the Association for Computing Machinery’s Special Interest Group on Algorithms and Computation Theory and the European Association for Theoretical Computer Science. The prize will be presented at the 43rd International Colloquium on Automata, Languages and Programming, July 12-15 in Rome.

CSL provides a logic that computer scientists can use to write and reason about specifications for concurrency — the decomposition of programs, algorithms or problems into units of undetermined order. Decomposition is the basis for parallel execution of programs or algorithms, which can enhance the overall speed of computing systems. But concurrency makes programs difficult to understand and to write correctly.

A long-term aim of Brookes’ research, supported in part by the National Science Foundation, has been to improve the design and analysis of correct concurrent programs. The invention of CSL is a major development in this direction.

O’Hearn’s paper, “Resources, Concurrency, and Logical Reasoning,” described how to reason with CSL. Brookes’ paper, “A Semantics for Concurrent Separation Logic,” introduced a clever semantic model to demonstrate the soundness of CSL, which was essential for the logic to be widely accepted and applied.

Recently, Brookes has begun work on semantic models for weak memory concurrency.

Brookes, who earned both his bachelor’s degree in mathematics and his Ph.D. in computer science at Oxford University, joined Carnegie Mellon as a research computer scientist in 1981, rising to the rank of professor in 2006.

Steven Rudich, CMU professor of computer science, received the Gödel Prize in 2007.