Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2009
Abstract
Concurrent algorithms are notoriously difficult to design correctly, and high performance algorithms that make little or no use of locks even more so. In this paper, we describe a formal verification of a recent concurrent data structure Scalable NonZero Indicators. The algorithm supports incrementing, decrementing, and querying the shared counter in an efficient and linearizable way without blocking. The algorithm is highly non-trivial and it is challenging to prove the correctness. We have proved that the algorithm satisfies linearizability, by showing a trace refinement relation from the concrete implementation to its abstract specification. These models are specified in CSP and verified automatically using the model checking toolkit PAT.
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 21st International Conference on Software Engineering & Knowledge Engineering (SEKE'2009), Boston, July 1-3
First Page
406
Last Page
411
ISBN
1891706241
City or Country
USA
Citation
SUN, Jun; LIU, Yang; SUN, Jun; DONG, Jin Song; CHEN, Wei; and LIU, Yanhong A..
Formal verification of scalable nonzero indicators. (2009). Proceedings of the 21st International Conference on Software Engineering & Knowledge Engineering (SEKE'2009), Boston, July 1-3. 406-411.
Available at: https://ink.library.smu.edu.sg/sis_research/4962
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.