Proving that non-blocking algorithms don't block

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.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.3, p.507-535, May 1995 [doi>10.1145/203095.201069]
• 2: B. Alpern and F. B. Schneider. Defining liveness. Inf. Process. Lett., 21(4):181--185, 1985.
• 3: 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.
• 4: S. D. Brookes. Full abstraction for a shared-variable parallel language. Inf. Comput., 127(2):145--163, 1996.
• 5: Cristiano Calcagno , Peter W. O'Hearn , Hongseok Yang, Local Action and Abstract Separation Logic, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.366-378, July 10-14, 2007 [doi>10.1109/LICS.2007.30]
• 6: 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.
• 7: 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.
• 8: Byron Cook , Alexey Gotsman , Andreas Podelski , Andrey Rybalchenko , Moshe Y. Vardi, Proving that programs eventually do something good, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 9: 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.
• 10: 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.
• 11: 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.
• 12: Alexey Gotsman , Josh Berdine , Byron Cook , Mooly Sagiv, Thread-modular shape analysis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 13: Timothy L. Harris , Keir Fraser , Ian A. Pratt, A Practical Multi-word Compare-and-Swap Operation, Proceedings of the 16th International Conference on Distributed Computing, p.265-279, October 28-30, 2002
• 14: Danny Hendler , Nir Shavit , Lena Yerushalmi, A scalable lock-free stack algorithm, Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures, June 27-30, 2004, Barcelona, Spain [doi>10.1145/1007912.1007944]
• 15: Maurice Herlihy, Wait-free synchronization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.1, p.124-149, Jan. 1991 [doi>10.1145/114005.102808]
• 16: Maurice Herlihy , Victor Luchangco , Mark Moir, Obstruction-Free Synchronization: Double-Ended Queues as an Example, Proceedings of the 23rd International Conference on Distributed Computing Systems, p.522, May 19-22, 2003
• 17: M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008.
• 18: C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321--332. North-Holland, 1983.
• 19: Naoki Kobayashi , Davide Sangiorgi, A Hybrid Type System for Lock-Freedom of Mobile Processes, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_10]
• 20: Orna Lichtenstein , Amir Pnueli , Lenore D. Zuck, The Glory of the Past, Proceedings of the Conference on Logic of Programs, p.196-218, June 17-19, 1985
• 21: 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.
• 22: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 23: Henry Massalin , Calton Pu, A Lock-Free Multiprocessor OS Kernel, ACM SIGOPS Operating Systems Review, v.26 n.2, p.108, April 1992
• 24: Kenneth L. McMillan, Circular Compositional Reasoning about Liveness, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.342-345, September 27-29, 1999
• 25: Maged M. Michael, High performance dynamic lock-free hash tables and list-based sets, Proceedings of the fourteenth annual ACM symposium on Parallel algorithms and architectures, August 10-13, 2002, Winnipeg, Manitoba, Canada [doi>10.1145/564870.564881]
• 26: Maged M. Michael , Michael L. Scott, Simple, fast, and practical non-blocking and blocking concurrent queue algorithms, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.267-275, May 23-26, 1996, Philadelphia, Pennsylvania, United States [doi>10.1145/248052.248106]
• 27: J. Strother Moore, A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View, Formal Methods in System Design, v.14 n.2, p.213-228, March 1999 [doi>10.1023/A:1008624904634]
• 28: Peter W. OHearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, v.375 n.1-3, p.271-307, April, 2007 [doi>10.1016/j.tcs.2006.12.035]
• 29: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 30: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 31: 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.
• 32: H. Simpson. Four-slot fully asynchronous communication mechanism. IEE Proceedings, 137(1):17--30, 1990.
• 33: R. K. Treiber. Systems programming: Coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center, 1986.
• 34: V. Vafeiadis. Modular fine-grained concurrency verification. PhD Thesis, University of Cambridge Computer Laboratory, 2008.
• 35: 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.
• 36: M. Vardi. Verification of concurrent programs-the automata-theoretic framework. Ann. Pure Appl. Logic, 51:79--98, 1991.
• 37: Martin Vechev , Eran Yahav, Deriving linearizable fine-grained concurrent objects, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 38: William N. Scherer, III , Doug Lea , Michael L. Scott, Scalable synchronous queues, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, March 29-31, 2006, New York, New York, USA [doi>10.1145/1122971.1122994]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Theory, Verification

Keywords:
concurrent programming, formal verification, liveness, termination