Information Science and Engineering, International Conference on (2009)
Nanjing, Jiangsu China
Dec. 26, 2009 to Dec. 28, 2009
The significant benefit of lock (or wait)-freedom for real-time systems is that by avoiding locks the potentials for deadlock and priority inversion are avoided. The lock-free algorithms often require the use of special atomic processor instructions such as CAS (compare and swap) or LL/SC(load linked/store conditional). However, many machine architectures support either CAS or LL/SC with restricted semantics. In this paper, we present a Practical lock-free implementation of the ideal semantics of LL/SC using only pointer-size CAS. To ensure our implementation is not flawed, we used the higher-order interactive theorem prover PVS for mechanical support.
Yan Fu, Hui Gao, Wim H. Hesselink, "Practical Lock-Free Implementation of LL/SC Using Only Pointer-Size CAS", Information Science and Engineering, International Conference on, vol. 00, no. , pp. 320-323, 2009, doi:10.1109/ICISE.2009.841