AtomCaml: first-class atomicity via rollback

ABSTRACT

We have designed, implemented, and evaluated AtomCaml, an extension to Objective Caml that provides a synchronization primitive for atomic (transactional) execution of code. A first-class primitive function of type (unit->'a)->'a evaluates its argument (which may call other functions, even external C functions) as though no other thread has interleaved execution. Our design ensures fair scheduling and obstruction-freedom. Our implementation extends the Objective Caml bytecode compiler and run-time system to support atomicity. A logging-and-rollback approach lets us undo uncompleted atomic blocks upon thread pre-emption, and retry them when the thread is rescheduled. The mostly functional nature of the Caml language and the Objective Caml implementation's commitment to a uniprocessor execution model (i.e., threads are interleaved, not executed simultaneously) allow particularly efficient logging. We have evaluated the efficiency and ease-of-use of AtomCaml by writing libraries and microbenchmarks, writing a small application, and replacing all locking with atomicity in an existing, large multithreaded application. Our experience indicates the performance overhead is negligible, atomic helps avoid synchronization mistakes, and idioms such as condition variables adapt reasonably to the atomic approach.

REFERENCES

• 1: AtomCAML. http://www.cs.washington.edu/homes/miker/atomcaml.
• 2: David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
• 3: Brian N. Bershad , David D. Redell , John R. Ellis, Fast mutual exclusion for uniprocessors, Proceedings of the fifth international conference on Architectural support for programming languages and operating systems, p.223-233, October 12-15, 1992, Boston, Massachusetts, United States
• 4: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 5: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 6: Greg Bronevetsky , Daniel Marques , Keshav Pingali , Peter Szwed , Martin Schulz, Application-level checkpointing for shared memory programs, Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 7: Guang-Ien Cheng , Mingdong Feng , Charles E. Leiserson , Keith H. Randall , Andrew F. Stark, Detecting data races in Cilk programs that use locks, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.298-309, June 28-July 02, 1998, Puerto Vallarta, Mexico [doi>10.1145/277651.277696]
• 8: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 9: Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
• 10: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 12: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 13: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 14: Cormac Flanagan , Shaz Qadeer, Types for atomicity, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 15: Matthew Flatt , Robert Bruce Findler, Kill-safe synchronization abstractions, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 16: Lance Hammond , Brian D. Carlstrom , Vicky Wong , Ben Hertzberg , Mike Chen , Christos Kozyrakis , Kunle Olukotun, Programming with transactional coherence and consistency (TCC), Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 17: Tim Harris. Exceptions and side-effects in atomic blocks. In PODC Workshop on Concurrency and Synchronization in Java Programs, July 2004.
• 18: Tim Harris , Keir Fraser, Language support for lightweight transactions, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 19: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065952]
• 20: Maurice Herlihy , Victor Luchangco , Mark Moir , William N. Scherer, III, Software transactional memory for dynamic-sized data structures, Proceedings of the twenty-second annual symposium on Principles of distributed computing, p.92-101, July 13-16, 2003, Boston, Massachusetts [doi>10.1145/872035.872048]
• 21: Michael Hicks , Pankaj Kakkar , Jonathan T. Moore , Carl A. Gunter , Scott Nettles, PLAN: a packet language for active networks, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.86-93, September 26-29, 1998, Baltimore, Maryland, United States
• 22: Michael Hicks, Jonathan T. Moore, D. Scott Alexander, Carl A. Gunter, and Scott M. Nettles. PLANet: An active internetwork. In IEEE Computer and Communication Society INFOCOM Conference, pages 1124--1133, 1999.
• 23: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 24: Barbara Liskov , Robert Scheifler, Guardians and Actions: Linguistic Support for Robust, Distributed Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.381-404, July 1983 [doi>10.1145/2166.357215]
• 25: Jeremy Manson, Jason Baker, Antonio Cunei, Suresh Jagannathan, Marek Prochazka, Jan Vitek, and Bin Xin. Preemptible atomic regions for Real-time Java. Technical report, Purdue University, 2005.
• 26: V. Krishna Nandivada and Suresh Jagannathan. Dynamic state restoration using versioning exceptions. Higher-Order and Symbolic Computation. To appear.
• 27: Ravi Rajwar , James R. Goodman, Transactional lock-free execution of lock-based programs, Proceedings of the 10th international conference on Architectural support for programming languages and operating systems, October 05-09, 2002, San Jose, California
• 28: John H. Reppy, Concurrent programming in ML, Cambridge University Press, New York, NY, 1999
• 29: Michael F. Ringenburg , Dan Grossman, Types for describing coordinated data structures, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.25-36, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040297]
• 30: Algis Rudys , Dan S. Wallach, Transactional Rollback for Language-Based Systems, Proceedings of the 2002 International Conference on Dependable Systems and Networks, p.439-448, June 23-26, 2002
• 31: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 32: February 27, 2005. http://www.securityfocus.com/.
• 33: Nir Shavit and Dan Touitou. Software transactional memory. Distributed Computing, Special Issue(10):99--116, 1997.
• 34: Avraham Shinnar, David Tarditi, Mark Plesko, and Bjarne Steensgaard. Integrating support for undo with exception handling. Technical Report MSR-TR -2004-140, Microsoft Research, December 2004.
• 35: Olin Shivers , James W. Clark , Roland McGrath, Atomic heap transactions and fine-grain interrupts, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.48-59, September 27-29, 1999, Paris, France
• 36: Andrew P. Tolmach and Andrew W. Appel. A debugger for standard ML. Journal of Functional Programming, 5(2):155--200, 1995.
• 37: February 27, 2005. http://www.us-cert.gov/.
• 38: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
• 39: Adam Welc , Antony L. Hosking , Suresh Jagannathan, Preemption-Based Avoidance of Priority Inversion for Java, Proceedings of the 2004 International Conference on Parallel Processing (ICPP'04), p.529-538, August 15-18, 2004 [doi>10.1109/ICPP.2004.60]
• 40: Adam Welc, Suresh Jagannathan, and Antony L. Hosking. Transactional monitors for concurrent objects. In European Conference on Object-Oriented Programming, 2004.
• 41: Jeannette M. Wing, Manuel Fähndrich, J. Gregory Morrisett, and Scott Nettles. Extensions to standard ML to support transactions. In ACM SIGPLAN Workshop on ML and its Applications, 1992.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

General Terms:
Languages

Keywords:
atomicity, concurrent programming, objective caml, transactions