7
IRUS Total
Downloads
  Altmetric

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models

File Description SizeFormat 
Libraries.pdfPublished version541.29 kBAdobe PDFView/Open
Title: On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
Authors: Raad, A
Doko, M
Rozic, L
Lahav, O
Vafeiadis, V
Item Type: Conference Paper
Abstract: Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (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.
Issue Date: 2-Jan-2019
Date of Acceptance: 31-Oct-2018
URI: http://hdl.handle.net/10044/1/75940
DOI: 10.1145/3290381
ISSN: 2475-1421
Publisher: Association for Computing Machinery (ACM)
Start Page: 68: 1
End Page: 68: 31
Journal / Book Title: Proceedings of the ACM on Programming Languages
Volume: 3
Copyright Statement: © 2019 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/).
Conference Name: ACM Principles of Programming Languages
Publication Status: Published
Start Date: 2019-01-13
Finish Date: 2019-01-19
Conference Place: Cascais, Portugal
Open Access location: https://dl.acm.org/doi/10.1145/3290381
Appears in Collections:Computing
Faculty of Engineering