2016 Godel Prize Recognizes Major Advances in Verification of Concurrent Programs
Stephen Brookes and Peter W. O’Hearn Honored for Invention of Concurrent Separation Logic
NEW YORK, NY, May 9, 2016 – 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 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), to be held July 12-15 in Rome, Italy.
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 facilitate 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 in Computer Science from Queen’s University, Kingston, Canada.
The Gödel Prize is named in honor 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 20th century. The award is presented annually by ACM’s Special Interest Group on Algorithms and Computation Theory (SIGACT) and the European Association for Theoretical Computer Science (EATCS). It recognizes major contributions to mathematical logic and the foundations of computer science and includes an award of $5,000.
About ACM
ACM, the Association for Computing Machinery, is the world's largest educational and scientific computing society, uniting educators, researchers, and professionals to inspire dialogue, share resources, and address the field's challenges. ACM strengthens the computing profession's collective voice through strong leadership, promotion of the highest standards, and recognition of technical excellence. ACM supports the professional growth of its members by providing opportunities for life-long learning, career development, and professional networking.
About ACM SIGACT
The ACM Special Interest Group on Algorithms and Computation Theory fosters and promotes the discovery and dissemination of high quality research in the domain of theoretical computer science. The field includes algorithms, data structures, complexity theory, distributed computation, parallel computation, VLSI, machine learning, computational biology, computational geometry, information theory, cryptography, quantum computation, computational number theory and algebra, program semantics and verification, automata theory, and the study of randomness. Work in this field is often distinguished by its emphasis on mathematical technique and rigor.
About EATCS
The European Association for Theoretical Computer Science is an international organization aimed at promoting research in the wide field of the foundations of computer science (ranging from formal languages, abstract computation models, algorithm design and complexity analysis, to applications of logic and semantics in programming). It facilitates the exchange of ideas and results among computer scientists, in particular through the organization of the annual International Conference on Automata, Languages and Programming (ICALP).
Contact:
Jim Ormond
212-626-0505
[email protected]
Michael Mitzenmacher
ACM SIGACT Chair
617-496-7172
[email protected]