Imperial College London
Portrait Picture

DrAzaleaRaad

Faculty of Engineering, Department of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8271azalea.raad Website

 
 
//

Location

 

426Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Raad:2019:10.1145/3290381,
author = {Raad, A and Doko, M and Rozic, L and Lahav, O and Vafeiadis, V},
doi = {10.1145/3290381},
pages = {68: 1--68: 31},
publisher = {Association for Computing Machinery (ACM)},
title = {On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models},
url = {http://dx.doi.org/10.1145/3290381},
year = {2019}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Raad,A
AU  - Doko,M
AU  - Rozic,L
AU  - Lahav,O
AU  - Vafeiadis,V
DO  - 10.1145/3290381
EP  - 1
PB  - Association for Computing Machinery (ACM)
PY  - 2019///
SN  - 2475-1421
SP  - 68
TI  - On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
UR  - http://dx.doi.org/10.1145/3290381
UR  - https://dl.acm.org/doi/10.1145/3290381
UR  - http://hdl.handle.net/10044/1/75940
ER  -
Download