Towards automatic proofs of lock-free algorithms

Conference object English OPEN
Fejoz , Loïc; Merz , Stephan;
  • Publisher: HAL CCSD
  • Subject: correctness | [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | lock-free | ACM : I.: Computing Methodologies/I.6: SIMULATION AND MODELING/I.6.4: Model Validation and Analysis | [ INFO.INFO-DS ] Computer Science [cs]/Data Structures and Algorithms [cs.DS] | refinement | algorithm

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 theore... View more
  • References (7)

    [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

    [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.

  • Metrics
Share - Bookmark