Sunday, 25.12.2016, 10:30
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:
1. What is the right semantics for concurrent programs in higher-level
2. Which reasoning principles apply to realistic shared-memory
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.