Publications

BibTex format

@techreport{Xiong:2017:10.25561/94920,
author = {Xiong, S and da, Rocha Pinto P and Ntzik, G and Gardner, P},
booktitle = {Departmental Technical Report: 17/1},
doi = {10.25561/94920},
publisher = {Department of Computing, Imperial College London},
title = {Abstract specifications for concurrent maps (extended version)},
url = {http://dx.doi.org/10.25561/94920},
year = {2017}
}

Download

RIS format (EndNote, RefMan)

TY  - RPRT
AB  - Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified.  The key issue lies in the development of  modular specifications, which provide clear logical boundaries  between clients and implementations.  A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.
AU  - Xiong,S
AU  - da,Rocha Pinto P
AU  - Ntzik,G
AU  - Gardner,P
DO  - 10.25561/94920
PB  - Department of Computing, Imperial College London
PY  - 2017///
TI  - Abstract specifications for concurrent maps (extended version)
T1  - Departmental Technical Report: 17/1
UR  - http://dx.doi.org/10.25561/94920
UR  - https://www.doc.ic.ac.uk/research/technicalreports/2017/DTRS17-1.pdf
UR  - http://hdl.handle.net/10044/1/94920
ER  -

Download

ProfessorPhilippaGardner

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)