Ownership types for safe programming: preventing data races and deadlocks

ABSTRACT

This paper presents a new static type system for multithreaded programs; well-typed programs in our system are guaranteed to be free of data races and deadlocks. Our type system allows programmers to partition the locks into a fixed number of equivalence classes and specify a partial order among the equivalence classes. The type checker then statically verifies that whenever a thread holds more than one lock, the thread acquires the locks in the descending order.Our system also allows programmers to use recursive tree-based data structures to describe the partial order. For example, programmers can specify that nodes in a tree must be locked in the tree order. Our system allows mutations to the data structure that change the partial order at runtime. The type checker statically verifies that the mutations do not introduce cycles in the partial order, and that the changing of the partial order does not lead to deadlocks. We do not know of any other sound static system for preventing deadlocks that allows changes to the partial order at runtime.Our system uses a variant of ownership types to prevent data races and deadlocks. Ownership types provide a statically enforceable way of specifying object encapsulation. Ownership types are useful for preventing data races and deadlocks because the lock that protects an object can also protect its encapsulated objects. This paper describes how to use our type system to statically enforce object encapsulation as well as prevent data races and deadlocks. The paper also contains a detailed discussion of different ownership type systems and the encapsulation guarantees they provide.

References

1. O. Agesen, S. N. Freund, and J. C. Mitchell. Adding type parameterization to the Java language. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1997.
2. J. Aldrich, V. Kostadinov, and C. Chambers. Alias annotations for program understanding. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), November 2002.
3. P. S. Almeida. Balloon types: Controlling sharing of state in data types. In European Conference for Object-Oriented Programming (ECOOP), June 1997.
4. D. F. Bacon, R. E. Strom, and A. Tarafdar. Guava: A dialect of Java without data races. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2000.
5. C. Boyapati, R. Lee, and M. Rinard. Safe runtime downcasts with ownership types. Technical Report TR-853, MIT Laboratory for Computer Science, June 2002.
6. C. Boyapati, B. Liskov, and L. Shrira. Ownership types and safe lazy upgrades in object oriented databases. Technical Report TR-858, MIT Laboratory for Computer Science, July 2002.
7. C. Boyapati and M. Rinard. A parameterized type system for race-free Java programs. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2001.
8. G. Bracha, M. Odersky, D. Stoutamire, and P. Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1998.
9. P. Brinch-Hansen. The programming language Concurrent Pascal. In IEEE Transactions on Software Engineering SE-1(2), June 1975.
10. S. Chaki, S. K. Rajamani, and J. Rehof. Types as models: Model checking message-passing programs. In Principles of Programming Languages (POPL), January 2002.
11. J. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Programming Language Design and Implementation (PLDI), June 2002.
12. D. G. Clarke and S. Drossopoulou. Ownership, encapsulation and disjointness of type and effect. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), November 2002.
13. D. G. Clarke, J. Noble, and J. M. Potter. Simple ownership types for object containment. In European Conference for Object-Oriented Programming (ECOOP), June 2001.
14. D. G. Clarke, J. M. Potter, and J. Noble. Ownership types for flexible alias protection. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1998.
15. T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, 1991.
16. K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Principles of Programming Languages (POPL), January 1999.
17. M. Day, R. Gruber, B. Liskov, and A. C. Myers. Subtypes vs. where clauses: Constraining parametric polymorphism. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1995.
18. R. DeLine and M. Fahndrich. Enforcing high-level protocols in low-level software. In Programming Language Design and Implementation (PLDI), June 2001.
19. D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, December 1998.
20. A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. In ACM/ONR Workshop on Parallel and Distributed Debugging (AOWPDD), May 1991.
21. D. R. Engler, D. Y. Chen, S. Hallem, A. Chon, and B. Chelf. Bugs as deviant behavior: A general approach to inferring errors in systems code. In Symposium on Operating Systems Principles (SOSP), October 2001.
22. C. Flanagan and S. N. Freund. Type-based race detection for Java. In Programming Language Design and Implementation (PLDI), June 2000.
23. M. Flatt, S. Krishnamurthi, and M. Felleisen. Classes and mixins. In Principles of Programming Languages (POPL), January 1998.
24. J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
25. D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Region-based memory management in Cyclone. In Programming Language Design and Implementation (PLDI), June 2001.
26. J. Hogg. Islands: Aliasing protection in object-oriented languages. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1991.
27. J. Hogg, D. Lea, A. Wills, and D. de Champeaux. The Geneva convention on the treatment of object aliasing. In OOPS Messenger 3(2), April 1992.
28. A. Igarashi and N. Kobayashi. A generic type system for the Pi-calculus. In Principles of Programming Languages (POPL), January 2001.
29. J. A. Korty. Sema: A lint-like tool for analyzing semaphore usage in a multithreaded UNIX kernel. In USENIX Winter Technical Conference, January 1989.
30. V. Kuncak, P. Lam, and M. Rinard. Role analysis. In Principles of Programming Languages (POPL), January 2002.
31. B. W. Lampson, J. J. Horning, R. L. London, J. G. Mitchell, and G. J. Popek. Report on the programming language Euclid. In Sigplan Notices, 12(2), February 1977.
32. K. R. M. Leino. Data groups: Specifying the modification of extended state. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 1998.
33. K. R. M. Leino and G. Nelson. Data abstraction and information hiding. Research Report 160, Compaq Systems Research Center, November 2000.
34. K. R. M. Leino, A. Poetzsch-Heffter, and Y. Zhou. Using data groups to specify and check side effects. In Programming Language Design and Implementation (PLDI), June 2002.
35. T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1997.
36. A. Lister. The problem of nested monitor calls. In Operating Systems Review 11(3), July 1977.
37. J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Principles of Programming Languages (POPL), January 1988.
38. N. Minsky. Towards alias-free pointers. In European Conference for Object-Oriented Programming (ECOOP), July 1996.
39. A. Moeller and M. I. Schwartzbach. The pointer assertion logic engine. In Programming Language Design and Implementation (PLDI), June 2001.
40. P. Muller and A. Poetzsch-Heffter. Universes: A type system for controlling representation exposure. In A. Poetzsch-Heffter and J. Meyer, editors, Programming Languages and Fundamentals of Programming. 1999.
41. A. C. Myers, J. A. Bank, and B. Liskov. Parameterized types for Java. In Principles of Programming Languages (POPL), January 1997.
42. M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. Transactions on Programming Languages and Systems (TOPLAS) 20(1), January 1998.
43. S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. In Symposium on Operating Systems Principles (SOSP), October 1997.
44. N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, January 1993.
45. M. Viroli and A. Natali. Parametric polymorphism in Java: An approach to translation based on reflective features. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2000.
46. C. von Praun and T. Gross. Object-race detection. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2001.
47. P. Wadler. Linear types can change the world. In M. Broy and C. Jones, editors, Programming Concepts and Methods. 1990.
48. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. In Information and Computation 115(1), November 1994.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language features

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification