Communications of the ACM
ACM Awards 2016 Gödel Prize to Inventors of Concurrent Separation Logic
ACM's Special Interest Group on Algorithms and Computation Theory and the European Association for Theoretical Computer Science on Monday awarded Stephen Brookes and Peter W. OHearn the 2016 Gdel Prize.
Credit: ACM
ACM's Special Interest Group on Algorithms and Computation Theory (SIGACT) and the European Association for Theoretical Computer Science on Monday awarded the creators of Concurrent Separation Logic (CSL) the 2016 Gödel Prize.
Carnegie Mellon University professor Stephen Brookes and Facebook engineering manager Peter W. O'Hearn presented the concept of CSL in separate papers, with O'Hearn's work concentrating on fluency with logic, while Brookes' focus was a demonstration of the logic's soundness using the CSL model.
CSL has been the basis for nearly all research papers developing theoretical concurrent program logics in the last 10 years. The papers include research 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 terms of practicality, CSL bears a close resemblance to the programming idioms often used by working engineers. Proofs are significantly simplified because the logic matches the common programming idioms.
CSL's simple organization and structure also enable automation, so many tools and methods in the research community use it as a foundation.
From Inside HPC
View Full Article
Abstracts Copyright © 2016 Information Inc., Bethesda, Maryland, USA
No entries found