Dependable, Autonomic and Secure Computing, IEEE International Symposium on (2009)
Dec. 12, 2009 to Dec. 14, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DASC.2009.25
On shared memory multiprocessors, synchronization often turns out to be a performance bottleneck and the source of poor fault-tolerance. By avoiding locks, the significant benefit of lock (or wait)-freedom for real-time systems is that the potentials for deadlock and priority inversion are avoided. The lock-free algorithms often require the use of special atomic processor primitives such as CAS (Compare And Swap) or LL /SC (Load Linked/Store Conditional). However, many machine architectures support either CAS or LL /SC , but not both. In this paper, we present a lock-free implementation of the ideal semantics of LL /SC using only pointer-size CAS , and show how to use refinement mapping to prove the correctness of the algorithm.
Lock-free, Verification, refinement mapping, PVS
Yan Fu, Hui Gao, Wim H. Hesselink, "Verification of a Lock-Free Implementation of Multiword LL/SC Object", Dependable, Autonomic and Secure Computing, IEEE International Symposium on, vol. 00, no. , pp. 31-36, 2009, doi:10.1109/DASC.2009.25