Please use this identifier to cite or link to this item:
|Title:||Formal verification of scalable nonzero indicators||Authors:||Zhang, S.J.
|Issue Date:||2009||Citation:||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.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.