Progress guarantee for parallel programs via bounded lock-freedom

ABSTRACT

Parallel platforms are becoming ubiquitous with modern computing systems. Many parallel applications attempt to avoid locks in order to achieve high responsiveness, aid scalability, and avoid deadlocks and livelocks. However, avoiding the use of system locks does not guarantee that no locks are actually used, because progress inhibitors may occur in subtle ways through various program structures. Notions of progress guarantee such as lock-freedom, wait-freedom, and obstruction-freedom have been proposed in the literature to provide various levels of progress guarantees.

In this paper we formalize the notions of progress guarantees using linear temporal logic (LTL). We concentrate on lock-freedom and propose a variant of it denoted bounded lock-freedom, which is more suitable for guaranteeing progress in practical systems. We use this formal definition to build a tool that checks if a concurrent program is bounded lock-free for a given bound. We then study the interaction between programs with progress guarantees and the underlying system (e.g., compilers, runtimes, operating systems, and hardware platforms). We propose a means to argue that an underlying system supports lock-freedom. A composition theorem asserts that bounded lock-free algorithms running on bounded lock-free supporting systems retain bounded lock-freedom for the composed execution.

REFERENCES

• 1: Lawrence Bush. Lock free linked list using compare & swap. http://www.cs.rpi.edu/ bushl2/project web/page5.html, April 2002.
• 2: David L. Detlefs , Paul A. Martin , Mark Moir , Guy L. Steele, Jr., Lock-free reference counting, Distributed Computing, v.15 n.4, p.255-271, December 2002 [doi>10.1017/s00446-002-0079-z]
• 3: Brijesh Dongol. Formalising progress properties of non-blocking programs. In Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, pages 284--303, 2006.
• 4: Cynthia Dwork , Nancy Lynch , Larry Stockmeyer, Consensus in the presence of partial synchrony, Journal of the ACM (JACM), v.35 n.2, p.288-323, April 1988 [doi>10.1145/42282.42283]
• 5: Faith Ellen Fich, Victor Luchangco, Mark Moir, and Nir Shavit. Obstruction-free algorithms can be practically wait-free. In DISC, pages 78--92, 2005.
• 6: Anders Gidenstam, Marina Papatriantafilou, Håkon Sundell, and Philippas Tsigas. Practical and efficient lock-free garbage collection based on reference counting. Technical Report 04, Chalmers University of Technology and Göteborg University, 2005.
• 7: Anders Gidenstam, Marina Papatriantafilou, and Philippas Tsigas. Allocating memory in a lock-free manner. In Proceedings of the 13th Annual European Symposium on Algorithms, number 3669 in LNCS, pages 329--342. Springer-Verlag, October 2005.
• 8: Brian Goetz, Tim Peierls, Joshua Block, Joseph Bowbeer, David Holmes, and Doug Lea. Java Concurrency in Practice. Addison-Wesley, 2006.
• 9: Alexey Gotsman , Byron Cook , Matthew Parkinson , Viktor Vafeiadis, Proving that non-blocking algorithms don't block, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
• 10: 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]
• 11: Maurice Herlihy , Victor Luchangco , Paul Martin , Mark Moir, Nonblocking memory management support for dynamic-sized data structures, ACM Transactions on Computer Systems (TOCS), v.23 n.2, p.146-196, May 2005 [doi>10.1145/1062247.1062249]
• 12: 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
• 13: Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, March 2008.
• 14: Prasad Jayanti, A Complete and Constant Time Wait-Free Implementation of CAS from LL/SC and Vice Versa, Proceedings of the 12th International Symposium on Distributed Computing, p.216-230, September 24-26, 1998
• 15: Henry Massalin, Synthesis: an efficient implementation of fundamental operating system services, Columbia University, New York, NY, 1992
• 26: Michael Merritt , Gadi Taubenfeld, Computing with Infinitely Many Processes, Proceedings of the 14th International Conference on Distributed Computing, p.164-178, October 04-06, 2000
• 27: Distributed Computing, pages 164---178. Springer--Verlag, 2000.
• 28: Maged M. Michael, Scalable lock-free dynamic memory allocation, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 29: and Implementation, ACM SIGPLAN Notices, Washington, DC, June 2004. ACM Press.
• 30: Maged M. Michael, Safe memory reclamation for dynamic lock-free objects using atomic reads and writes, Proceedings of the twenty-first annual symposium on Principles of distributed computing, July 21-24, 2002, Monterey, California [doi>10.1145/571825.571829]
• 31: Symposium on Principles of Distributed Computing, pages 21---30, July 2002.
• 32: Maged M. Michael. Practical lock--free and wait--free LL/SC/VL implementations using 64--bit CAS. In Proceedings of the 18th International Conference
• 33: on Distributed Computing, volume 3274 of LNCS, pages 144---158. Springer--Verlag, October 2004.
• 34: Maged M. Michael, Scalable lock-free dynamic memory allocation, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 35: Design and Implementation, pages 35---46, June 2004.
• 36: Maged M. Michael and Michael L. Scott. Simple, fast, and practical non--blocking and blocking concurrent queue algorithms. In Proceedings of the
• 37: 15th International Symposium on Principles of Distributed Computing, pages 267---275, May 1996.
• 38: Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing
• 39: heisenbugs in concurrent programs. In OSDI 08: Operating Systems Design and Implementation, pages 267---280, 2008.
• 40: Filip Pizlo, Daniel Frampton, Erez Petrank, and Bjarne Steensgard. STOPLESS: A real--time garbage collector for multiprocessors. In Mooly Sagiv,
• 41: editor, ISMM'07 Proceedings of the Fifth International Symposium on Memory Management, pages 159---172, Montr´
• 42: eal, Canada, October 2007. ACM
• 43: Press.
• 44: Filip Pizlo , Erez Petrank , Bjarne Steensgaard, A study of concurrent real-time garbage collectors, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 45: Programming Languages Design and Implementation, ACM SIGPLAN Notices, pages 33---44, Tucson, AZ, June 2008. ACM Press.
• 46: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, p.46-57, September 30-October 31, 1977
• 47: John D. Valois, Lock-free linked lists using compare-and-swap, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.214-222, August 20-23, 1995, Ottowa, Ontario, Canada [doi>10.1145/224964.224988]
• 48: computing, pages 214---222, Ottawa, Ontario, CA, 1995.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Synchronization; Concurrency; Threads

General Terms:
Performance, Reliability, Theory, Verification

Keywords:
bounded lock-freedom, lock-freedom, model checking, parallel computation, progress guarantees