Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/40029
Title: Formal verification of scalable nonzero indicators
Authors: Zhang, S.J.
Liu, Y. 
Sun, J. 
Dong, J.S. 
Chen, W.
Liu, Y.A.
Issue Date: 2009
Source: Zhang, S.J.,Liu, Y.,Sun, J.,Dong, J.S.,Chen, W.,Liu, Y.A. (2009). Formal verification of scalable nonzero indicators. Proceedings of the 21st International Conference on Software Engineering and Knowledge Engineering, SEKE 2009 : 406-411. ScholarBank@NUS Repository.
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.
Source Title: Proceedings of the 21st International Conference on Software Engineering and Knowledge Engineering, SEKE 2009
URI: http://scholarbank.nus.edu.sg/handle/10635/40029
ISBN: 1891706241
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Page view(s)

52
checked on Dec 16, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.