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 Bacon, Robert Storm, and Ashis Tarafdar. Guava: A dialect of Java without data races. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 382--400, October 2000.]]
3. Brian N. Bershad, David D. Redell, and John R. Ellis. Fast mutual exclusion for uniprocessors. In 5th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 223--233, 1992.]]
4. Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 211--230, November 2002.]]
5. Chandrasekhar Boyapati and Martin Rinard. A parameterized type system for race-free Java programs. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 56--59, October 2001.]]
6. Greg Bronevetsky, Daniel Marques, Keshav Pingali, Peter Szwed, and Martin Schulz. Application-level checkpointing for shared memory programs. In International Conference on Architectural Support for Programming Languages and Operating Systems, pages 235--247, 2004.]]
7. Guang-Ien Cheng, Mingdong Feng, Charles E. Leiserson, Keith H. Randall, and Andrew F. Stark. Detecting data races in Cilk programs that use locks. In ACM Symposium on Parallel Algorithms and Architectures, pages 298--309, June 1998.]]
8. Jong-Deok Choi, Keunwoo Lee, Alexey Loginov, Robert O'Callahan, Vivek Sarkar, and Manu Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In ACM Conference on Programming Language Design and Implementation, pages 258--269, June 2002.]]
9. Cormac Flanagan and Martín Abadi. Types for safe locking. In European Symposium on Programming, volume 1576 of Lecture Notes in Computer Science, pages 91--108. Springer-Verlag, 1999.]]
10. Cormac Flanagan and Stephen N. Freund. Type-based race detection for Java. In ACM Conference on Programming Language Design and Implementation, pages 219--232, 2000.]]
11. Cormac Flanagan and Stephen N. Freund. Atomizer: A dynamic atomicity checker for multithreaded programs. In ACM Symposium on Principles of Programming Languages, pages 256--267, 2004.]]
12. Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In ACM Conference on Programming Language Design and Implementation, pages 234--245, 2002.]]
13. Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. In ACM Conference on Programming Language Design and Implementation, pages 338--349, June 2003.]]
14. Cormac Flanagan and Shaz Qadeer. Types for atomicity. In ACM International Workshop on Types in Language Design and Implementation, pages 1--12, January 2003.]]
15. Matthew Flatt and Robert Bruce Findler. Kill-safe synchronization abstractions. In ACM Conference on Programming Language Design and Implementation, pages 47--58, Washington DC, June 2004.]]
16. Lance Hammond, Brian D. Carlstrom, Vicky Wong, Ben Hertzberg, Mike Chen, Christos Kozyrakis, and Kunle Olukotun. Programming with transactional coherence and consistency (tcc). In International Conference on Architectural Support for Programming Languages and Operating Systems, pages 1--13, 2004.]]
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 and Keir Fraser. Language support for lightweight transactions. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 388--402, October 2003.]]
19. Tim Harris, Simon Marlow, Simon Peyton Jones, and Maurice Herlihy. Composable memory transactions. In ACM Symposium on Principles and Practice of Parallel Programming, 2005.]]
20. Maurice Herlihy, Victor Luchangco, Mark Moir, and William N. Scherer III. Software transactional memory for dynamic-sized data structures. In ACM Symposium on Principles of Distributed Computing, pages 92--101, 2003.]]
21. Michael Hicks, Pankaj Kakkar, Jonathan T. Moore, Carl A. Gunter, and Scott Nettles. PLAN: A packet language for active networks. In ACM SIGPLAN International Conference on Functional Programming Languages (ICFP), pages 86--93, 1998.]]
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, 18(12):717--721, December 1975.]]
24. Barbara Liskov and Robert Scheifler. Guardians and actions: Linguistic support for robust, distributed programs. ACM Transactions on Programming Languages and Systems, 5(3):381--404, 1983.]]
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 and James R. Goodman. Transactional lock-free execution of lock-based programs. In 10th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 5-17, San Jose, CA, October 2002.]]
28. John H. Reppy. Concurrent Programming in ML. Cambridge University Press, 1999.]]
29. Michael F. Ringenburg and Dan Grossman. Types for describing coordinated data structures. In ACM International Workshop on Types in Language Design and Implementation, pages 25--36, January 2005.]]
30. Algis Rudys and Dan S.Wallach. Transactional rollback for languagebased systems. In International Conference on Dependable Systems and Networks, June 2002.]]
31. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A dynmaic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4):391--411, 1997.]]
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, and Roland McGrath. Atomic heap transactions and fine-grain interrupts. In ACM International Conference on Functional Programming, pages 48--59, 1999.]]
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 and Thomas R. Gross. Object race detection. In ACM Conference on Object Oriented Programming, Systems, Languages, and Applications, pages 70--82, October 2001.]]
39. Adam Welc, Antony L. Hosking, and Suresh Jagannathan. Preemption-based avoidance of priority inversion for Java. In International Conference on Parallel Processing, 2004.]]
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

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features

        • Concurrent programming structures