DocumentCode :
3093446
Title :
Verification of a Lock-Free Implementation of Multiword LL/SC Object
Author :
Gao, Hui ; Fu, Yan ; Hesselink, Wim H.
Author_Institution :
Sch. of Comput. Sci. & Eng., Univ. of Electron. Sci. & Technol. of China, Chengdu, China
fYear :
2009
fDate :
12-14 Dec. 2009
Firstpage :
31
Lastpage :
36
Abstract :
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.
Keywords :
fault tolerance; real-time systems; shared memory systems; synchronisation; fault tolerance; load linked-store conditional object; machine architectures; multiword LL/SC object; real-time systems; shared memory multiprocessors; synchronization; Algorithm design and analysis; Computer science; Content addressable storage; Data structures; Delay; Fault tolerance; Mathematics; Real time systems; System recovery; Yarn; Lock-free; PVS; Verification; refinement mapping;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Dependable, Autonomic and Secure Computing, 2009. DASC '09. Eighth IEEE International Conference on
Conference_Location :
Chengdu
Print_ISBN :
978-0-7695-3929-4
Electronic_ISBN :
978-1-4244-5421-1
Type :
conf
DOI :
10.1109/DASC.2009.25
Filename :
5380331
Link To Document :
بازگشت