@inproceedings{zhang2009formal,
author = {Zhang, Shao Jie and Liu, Yang and Sun, Jun and Dong, Jin Song and Liu, Yanhong A. and Chen, Wei},
title = {Formal Verification of Scalable NonZero Indicators},
booktitle = {The 21st International Conference on Software Engineering and Knowledge Engineering (SEKE'2009), Boston, U.S.A., July 2009.},
year = {2009},
month = {July},
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.},
url = {http://approjects.co.za/?big=en-us/research/publication/formal-cerification-scalable-nonzero-indicators/},
edition = {The 21st International Conference on Software Engineering and Knowledge Engineering (SEKE'2009), Boston, U.S.A., July 2009.},
}