publication . Conference object . 2008

Towards automatic proofs of lock-free algorithms

Fejoz, Loïc; Merz, Stephan;
Open Access English
  • Published: 07 Jul 2008
  • Publisher: HAL CCSD
Abstract
International audience; The verification of lock-free data structures has traditionally been considered as difficult. We propose a formal model for describing such algorithms. The verification conditions generated from this model can often be handled by automatic theorem provers.
Subjects
free text keywords: ACM: I.: Computing Methodologies/I.6: SIMULATION AND MODELING/I.6.4: Model Validation and Analysis, correctness, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], lock-free, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], refinement, algorithm

[1] D. De´harbe, P. Fontaine, S. Ranise, and C. Ringeissen. Decision procedures for the formal analysis of software. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Intl. Coll. Theoretical Aspects of Computing (ICTAC 2007), volume 4281 of Lecture Notes in Computer Science, pages 366-370, Tunis, Tunisia, 2007. Springer. See also http://harvey.loria.fr/.

[2] H. Gao. Design and verification of lock-free parallel algorithms. PhD thesis, University of Groningen, Apr. 2005.

[3] T. L. Harris, K. Fraser, and I. A. Pratt. A practical multi-word compare-and-swap operation. In Proceedings of the 16th International Symposium on Distributed Computing, 2002.

[4] M. Herlihy. Wait-free synchronization. ACM Transactions on Programming Languages and Systems, 13(1):124-149, January 1991.

[5] M. M. Michael and M. L. Scott. Nonblocking algorithms and preemption-safe locking on multiprogrammed shared - memory multiprocessors. Journal of Parallel and Distributed Computing, 51(1):1-26, 1998.

[6] S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Commun. ACM, 19(5):279-285, 1976.

[7] N. Shavit and D. Touitou. Software transactional memory. In Distributed Computing, pages 204- 213, 1995.

Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Conference object . 2008

Towards automatic proofs of lock-free algorithms

Fejoz, Loïc; Merz, Stephan;