<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><h2 class="node__title node-title"><a href="https://www.cs.princeton.edu/events/event/practical-foundations-scalable-concurrency">Practical Foundations for Scalable Concurrency</a></h2>
<span class="event-speaker">
<a href="http://www.mpi-sws.org/%7Eturon/">Aaron Turon</a> </span>
<span class="event-speaker-from">
(<a href="http://www.mpi-sws.org/index.php">Max Planck Institute for Software Systems (MPI-SWS)</a><br>Thursday, February 20, 4:30pm<br>Computer Science 105<br><br></span>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.<br>
<br>
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.<br>
<br>
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.<br>
<br>
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.<br>
<br></div></body></html>