Alexey Gotsman
Viktor Vafeiadis
ABSTRACT
A concurrent data-structure implementation is considered non-blocking if it meets one of three following liveness criteria: wait-freedom, lock-freedom, or obstruction-freedom. Developers of non-blocking algorithms aim to meet these criteria. However, to date their proofs for non-trivial algorithms have been only manual pencil-and-paper semi-formal proofs. This paper proposes the first fully automatic tool that allows developers to ensure that their algorithms are indeed non-blocking. Our tool uses rely-guarantee reasoning while overcoming the technical challenge of sound reasoning in the presence of interdependent liveness properties.
- M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. Program. Lang. Syst., 17(3):507--534, 1995. Google Scholar
Digital Library
- B. Alpern and F. B. Schneider. Defining liveness. Inf. Process. Lett., 21(4):181--185, 1985.Google ScholarCross Ref
- J. Berdine, B. Cook, D. Distefano, and P. W. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In CAV'06: Conference on Computer Aided Verification, volume 4144 of LNCS, pages 386--400. Springer, 2006. Google ScholarDigital Library
- S. D. Brookes. Full abstraction for a shared-variable parallel language. Inf. Comput., 127(2):145--163, 1996.Google ScholarCross Ref
- C. Calcagno, P. O'Hearn, and H. Yang. Local action and abstract separation logic. In LICS'07: Symposium on Logic in Computer Science, pages 366--378. IEEE, 2007. Google ScholarDigital Library
- C. Calcagno, M. J. Parkinson, and V. Vafeiadis. Modular safety checking for fine-grained concurrency. In SAS'07: Static Analysis Symposium, volume 4634 of LNCS, pages 233--248. Springer, 2007. Google ScholarDigital Library
- R. Colvin and B. Dongol. Verifying lock-freedom using well-founded orders. In ICTAC'07: International Colloquium on Theoretical Aspects of Computing, volume 4711 of LNCS, pages 124--138. Springer, 2007. Google ScholarDigital Library
- B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In POPL'07: Symposium on Principles of Programming Languages, pages 265--276. ACM, 2007. Google ScholarDigital Library
- S. Doherty, L. Groves, V. Luchangco, and M. Moir. Formal verification of a practical lock--free queue algorithm. In FORTE'04: Conference on Formal Techniques for Networked and Distributed Systems, volume 3235 of LNCS, pages 97--114. Springer, 2004.Google ScholarCross Ref
- B. Dongol. Formalising progress properties of non-blocking programs. In ICFEM'06: Conference on Formal Engineering Methods, volume 4260 of LNCS, pages 284--303. Springer, 2006. Google ScholarDigital Library
- X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP'07: European Symposium on Programming, volume 4421 of LNCS, pages 173--188. Springer, 2007. Google ScholarDigital Library
- A. Gotsman, J. Berdine, B. Cook, and M. Sagiv. Thread-modular shape analysis. In PLDI'07: Conference on Programming Language Design and Implementation, pages 266--277. ACM, 2007. Google ScholarDigital Library
- T. L. Harris, K. Fraser, and I. A. Pratt. A practical multi-word compare-and-swap operation. In DISC'02: Symposium on Distributed Computing, volume 2508 of LNCS, pages 265--279. Springer, 2002. Google ScholarDigital Library
- D. Hendler, N. Shavit, and L. Yerushalmi. A scalable lock-free stack algorithm. In SPAA'04: Symposium on Parallelism in Algorithms and Architectures, pages 206--215. ACM, 2004. Google ScholarDigital Library
- M. Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124--149, 1991. Google ScholarDigital Library
- M. Herlihy, V. Luchangco, and M. Moir. Obstruction-free synchronization: Double-ended queues as an example. In ICDCS'03: International Conference on Distributed Computing Systems, pages 522--529. IEEE, 2003. Google ScholarDigital Library
- M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008. Google ScholarDigital Library
- C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321--332. North-Holland, 1983.Google Scholar
- N. Kobayashi and D. Sangiorgi. A hybrid type system for lock-freedom of mobile processes. In CAV'08: Conference on Computer Aided Verification, volume 5123 of LNCS, pages 80--93. Springer, 2008. Google ScholarDigital Library
- O. Lichtenstein, A. Pnueli, and L. D. Zuck. The glory of the past. In Conference on Logics of Programs, volume 193 of LNCS, pages 196--218. Springer, 1985. Google ScholarDigital Library
- S. Magill, J. Berdine, E. M. Clarke, and B. Cook. Arithmetic strengthening for shape analysis. In SAS'07: Static Analysis Symposium, volume 4634 of LNCS, pages 419--436. Springer, 2007. Google ScholarDigital Library
- Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, 1992. Google ScholarDigital Library
- H. Massalin and C. Pu. A lock-free multiprocessor OS kernel (Abstract). Operating Systems Review, 26(2):108, 1992.Google ScholarCross Ref
- K. L. McMillan. Circular compositional reasoning about liveness. In CHARME'99: Conference on Correct Hardware Design and Verification Methods, volume 1703 of LNCS, pages 342--345. Springer, 1999. Google ScholarDigital Library
- M. M. Michael. High performance dynamic lock-free hash tables and list-based sets. In SPAA'02: Symposium on Parallelism in Algorithms and Architectures, pages 73--82. ACM, 2002. Google ScholarDigital Library
- M. M. Michael and M. L. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In PODC'96: Symposium on Principles of Distributed Computing, pages 267--275. ACM, 1996. Google ScholarDigital Library
- J. S. Moore. A mechanically checked proof of a multiprocessor result via a uniprocessor view. Formal Methods in System Design, 14(2):213--228, 1999. Google ScholarDigital Library
- P. W. O'Hearn. Resources, concurrency and local reasoning. Theor. Comput. Sci., 375(1--3):271--307, 2007. Google ScholarDigital Library
- A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, pages 123--144. Springer, 1985. Google ScholarDigital Library
- J. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS'02: Symposium on Logic in Computer Science, pages 55--74. IEEE, 2002. Google ScholarDigital Library
- S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. Myreen, and J. Alglave. The semantics of x86 multiprocessor machine code. This volume.Google Scholar
- H. Simpson. Four-slot fully asynchronous communication mechanism. IEE Proceedings, 137(1):17--30, 1990.Google Scholar
- R. K. Treiber. Systems programming: Coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center, 1986.Google Scholar
- V. Vafeiadis. Modular fine-grained concurrency verification. PhD Thesis, University of Cambridge Computer Laboratory, 2008.Google Scholar
- V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR'07: Conference on Concurrency Theory, volume 4703 of LNCS, pages 256--271. Springer, 2007. Google ScholarDigital Library
- M. Vardi. Verification of concurrent programs-the automata-theoretic framework. Ann. Pure Appl. Logic, 51:79--98, 1991.Google ScholarCross Ref
- M. T. Vechev and E. Yahav. Deriving linearizable fine-grained concurrent objects. In PLDI'08: Conference on Programming Languages Design and Implementation, pages 125--135. ACM, 2008. Google ScholarDigital Library
- I. William N. Scherer, D. Lea, and M. L. Scott. Scalable synchronous queues. In PPoPP'06: Symposium on Principles and Practice of Parallel Programming, pages 147--156. ACM, 2006. Google ScholarDigital Library
Index Terms
- Proving that non-blocking algorithms don't block
Recommendations
Proving that non-blocking algorithms don't block
POPL '09A concurrent data-structure implementation is considered non-blocking if it meets one of three following liveness criteria: wait-freedom, lock-freedom, or obstruction-freedom. Developers of non-blocking algorithms aim to meet these criteria. However, to ...
Proving that programs eventually do something good
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesIn recent years we have seen great progress made in the area of automatic source-level static analysis tools. However, most of today's program verification tools are limited to properties that guarantee the absence of bad events (safety properties). ...
Proving correctness of highly-concurrent linearisable objects
PPoPP '06: Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programmingWe study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical, coarse-grain synchronisation. Our examples are demonstrative of ...
Comments