Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 13:45 - 14:07 at Sala II - Weak Memory Chair(s): Scott Owens

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

Thu 17 Jan

Displayed time zone: Belfast change

13:45 - 14:51
Weak MemoryResearch Papers at Sala II
Chair(s): Scott Owens University of Kent, UK
13:45
22m
Talk
On Library Correctness under Weak Memory Consistency
Research Papers
Azalea Raad MPI-SWS, Germany, Marko Doko MPI-SWS, Germany, Lovro Rožić MPI-SWS, Germany, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Pre-print Media Attached File Attached
14:07
22m
Talk
Bridging the Gap Between Programming Languages and Hardware Weak Memory Models
Research Papers
Anton Podkopaev Higher School of Economics, JetBrains Research, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Pre-print Media Attached File Attached
14:29
22m
Talk
Grounding Thin-Air Reads with Event Structures
Research Papers
Soham Chakraborty Max Planck Institute for Software Systems, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Media Attached File Attached