Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (e.g. locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot of work on verifying such libraries in a sequentially consistent (SC) environment, little is known about how to specify and verify them under weak memory consistency (WMC).
We propose a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is sufficient to encode standard models such as SC, (R)C11 and TSO. Additionally, we specify several concurrent libraries, including mutual exclusion locks, reader-writer locks, exchangers, queues, stacks and sets. We then use our framework to verify multiple weakly consistent implementations of locks, exchangers, queues and stacks.
|Slides (PDF) (Libraries-POPL-2019-Talk.pdf)||1.57MiB|
Conference DayThu 17 JanDisplayed time zone: Belfast change
13:45 - 14:51
|On Library Correctness under Weak Memory Consistency|
Azalea RaadMPI-SWS, Germany, Marko DokoMPI-SWS, Germany, Lovro RožićMPI-SWS, Germany, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, GermanyLink to publication DOI Pre-print Media Attached File Attached
|Bridging the Gap Between Programming Languages and Hardware Weak Memory Models|
Anton PodkopaevHigher School of Economics, JetBrains Research, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS, GermanyLink to publication DOI Pre-print Media Attached File Attached
|Grounding Thin-Air Reads with Event Structures|
Research PapersLink to publication DOI Media Attached File Attached