Please use this identifier to cite or link to this item:
|Title:||Formal verification of scalable nonzero indicators|
|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|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 16, 2017
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.