Stephen Brookes and Peter W. O’Hearn receive the 2016 Gödel Prize

2016 GÖDEL PRIZE RECOGNIZES MAJOR ADVANCES IN VERIFICATION OF CONCURRENT PROGRAMS

Stephen Brookes and Peter W. O’Hearn Honoured for the Invention of Concurrent Separation Logic

The Association for Computing Machinery’s Special Interest Group on Algorithms and Computation Theory (SIGACT) and the European Association for Theoretical Computer Science (EATCS) have announced that Stephen Brookes and Peter W. O’Hearn are the recipients of the 2016 Gödel Prize for their invention of Concurrent Separation Logic. The prize will be presented at the 43^rd International Colloquium on Automata, Languages and Programming (ICALP 2016), to be held July 12-15 in Rome, Italy. Congratulations to Peter and Steve!

In computer science, concurrency is the decomposition of programs, algorithms or problems into units whose order is not determined; concurrent program units might occur in arbitrary order, even overlapping in time. Such a decomposition is the basis for the parallel execution of programs or algorithms, which can considerably enhance the overall speed of execution of multicore and multiprocessor systems. However, concurrent execution can make programs difficult to understand and get right, because different execution orders can lead to different results, and because different threads of execution can interfere with one another. Computer scientists use logic to write, and to reason about, specifications of concurrency in computer software systems.

In their separate papers— Brookes’ “A Semantics for Concurrent Separation Logic” and O’Hearn’s “Resources , Concurrency and Logical Reasoning,” the 2016 Gödel Prize recipients introduced and advanced the idea of Concurrent Separation Logic (CSL), which has had a far-reaching impact in both theoretical and practical realms. O'Hearn's paper introduces CSL and is very much about fluency with the logic – how to reason with it – rather than its meta-theory. The latter is the concern of Brookes' paper, which demonstrates soundness of the logic via a clever new model; this was essential for CSL to be widely accepted and applied.

In the theoretical realm, almost all research papers developing concurrent program logics in the last decade are based on CSL; including work on permissions; refinement and atomicity; on adaptations to assembly languages and weak memory models; on higher-order variants; and on the logics for termination of concurrent programs. In the practical realm, the beauty of CSL is in its similarity to the programming idioms commonly used by working engineers. The fact that the logic matches the common programming idioms has the effect of greatly simplifying proofs. CSL’s simplicity and structure also facilitates automation. As a result, numerous tools and techniques in the research community are based on it, and it is attracting attention in companies such as Facebook, Microsoft and Amazon.

Stephen Brookes is Professor of Computer Science at Carnegie Mellon University. A long-term aim of his research, culminating in his foundational work on Concurrent Separation Logic, has been to facilitate the design and analysis of correct concurrent programs. He has recently begun work on semantic models for weak memory concurrency. His work on Concurrent Separation Logic was partially funded by the National Science Foundation (NSF). He obtained his BA degree in Mathematics and his PhD in Computer Science, both from Oxford University.

Peter W. O’Hearn is an Engineering Manager at Facebook and a Professor of Computer Science at University College London. He cofounded a verification startup, Monoidics, which was acquired by Facebook in 2013. O’Hearn has also held academic positions at Queen Mary University of London and at Syracuse University. He is a past recipient of a Royal Society Wolfson Research Merit Award and a Most Influential POPL Paper award, and held a Royal Academy of Engineering/Microsoft Research Chair. He obtained his BS in Computer Science from Dalhousie University, Nova Scotia, and his MS and PhD Degrees in Computer Science from Queen’s University, Kingston, Canada.

The Gödel Prize is named in honour of Kurt Gödel, who was born in Austria-Hungary (now the Czech Republic) in 1906. Gödel's work has had immense impact upon scientific and philosophical thinking in the 20^th century. The award is presented annually by ACM’s Special Interest Group on Algorithms and Computation Theory (SIGACT) (http://sigact.acm.org) and the European Association for Theoretical Computer Science (EATCS) (http://eatcs.org/). It recognizes major contributions to mathematical logic and the foundations of computer science and includes an award of $5,000.