CANCELED- Practical Foundations for Scalable Concurrency

The traditional way to tame concurrency is to disallow it: "critical sections" of code can be protected by locks, preventing interference from concurrent threads, but also cutting down opportunities for parallelism.  The past two decades have produced a wealth of data structures that instead tolerate (or even embrace) concurrency for the sake of scaling with available parallelism.  But despite the importance of these "scalable" (e.g., lock-free) data structures, many basic questions about them have remained unanswered.  My work has focused on several such questions; this talk will cover two of them.

First, what are the fundamental abstractions for scalable concurrency?  I will present Reagents, the first high-level programming model for building lock-free data structures. Reagents solve a key problem for concurrency libraries: they allow library clients to combine data structure operations while retaining strong scalability and atomicity properties, and without requiring the clients to understand the underlying algorithms.

Second, how can we reason about scalable concurrency under realistic assumptions about shared memory?  The verification literature almost universally assumes that threads interact through a "strong" (sequentially consistent) shared memory.  But modern compilers and CPUs provide much weaker guarantees that cause many previously verified algorithms to fail.  I will present GPS, the first program logic to provide a full suite of modular verification techniques under a weak memory model.

Aaron Turon is a postdoctoral researcher in the Foundations of Programming group at the Max Planck Institute for Software Systems (MPI-SWS), supervised by Derek Dreyer.  He received his Ph.D. from Northeastern University in May 2013 under the supervision of Mitchell Wand, and his BA with Honors at the University of Chicago in 2007. Aaron's interests span programming languages and software verification, but his primary focus for the last several years has been the design and verification of high-performance concurrency libraries.