Ori Lahav (Tel-Aviv University)
Wednesday, 17.2.2021, 11:30
A concurrency semantics (aka a memory model) for a programming language defines the allowed behaviors of multithreaded programs. For programmers, sequential consistency (i.e., standard interleaving-based semantics) is considered as the most intuitive model. However, it is too costly to implement. Designing a satisfactory substitute is highly challenging as it requires to carefully balance the conflicting desires of programmers, compilers, and hardware. In this talk I will introduce this challenge and the key ideas behind the prototype example of the C/C++ concurrency model from 2011. Then, I will demonstrate the drawback of the C/C++ approach, notoriously known as the "out-of-thin-air" problem. I will conclude by describing the "promising semantics" solution, and remaining challenges.
Ori is a faculty member in the School of Computer Science at Tel Aviv University. He did his PhD at Tel Aviv University under the supervision of Arnon Avron in the field of logic for computer science. In 2014, he was a postdoctoral researcher at Tel Aviv University hosted by Mooly Sagiv. After that, until September 2017, he was a postdoctoral researcher at MPI-SWS in Germany hosted by Viktor Vafeiadis and Derek Dreyer. Ori's current main areas of research are programming languages and verification. Recently, Ori was awarded an ERC Starting Grant for the project titled "Verification-Aware Programming Language Concurrency Semantics".