TY - GEN
T1 - Formal verification of scalable nonzero indicators
AU - Zhang, Shao Jie
AU - Liu, Yang
AU - Sun, Jun
AU - Dong, Jin Song
AU - Chen, Wei
AU - Liu, Yanhong A.
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/77954823180
M3 - Conference contribution
AN - SCOPUS:77954823180
SN - 1891706241
SN - 9781891706240
T3 - Proceedings of the 21st International Conference on Software Engineering and Knowledge Engineering, SEKE 2009
SP - 406
EP - 411
BT - Proceedings of the 21st International Conference on Software Engineering and Knowledge Engineering, SEKE 2009
T2 - 21st International Conference on Software Engineering and Knowledge Engineering, SEKE 2009
Y2 - 1 July 2009 through 3 July 2009
ER -