With the proliferation of multi-core processors, shared-memory concurrent programming has become increasingly important. Nevertheless, despite decades of research, there are still no adequate answers to the following fundamental questions:
- What is the right semantics for concurrent programs in higher-level languages?
- Which reasoning principles apply to realistic shared-memory concurrency?
Concerning the first question, the challenge lies in simultaneously allowing efficient implementation on modern hardware with compiler optimizations, while exposing a well-behaved programming model. Both the Java and C/C++ standards tried to address this question, but their solutions were discovered to be flawed. They either allow spurious "out-of-thin-air" program behaviors or incur a prohibitive runtime cost. In the main part of the talk, I will present a solution to this problem based on a novel idea of promises, which supports efficient implementations and useful programming guarantees.
As for the second question, I will outline my ongoing efforts to identify (i) logical laws for deductive reasoning about concurrent programs; and (ii) programming disciplines that enable the application of well-established verification techniques.
Ori Lahav is a postdoctoral researcher at Max Planck Institute for Software Systems (MPI-SWS). His research interests include programming languages, formal methods and verification, semantics and logic. Previously, Ori was a postdoctoral researcher at the Programming Languages Group at Tel Aviv University. He obtained his Ph.D. from Tel Aviv University in 2014 under the supervision of Arnon Avron. Ori received a Dan David Prize scholarship for young researchers in 2014, the Kleene award for the best student paper at LICS 2013, and a Wolf Prize for excellent graduate students in 2012.