A type system for preventing data races and deadlocks in the java virtual machine language: 1

ABSTRACT

In previous work on SafeJava we presented a type system extension to the Java source language that statically prevents data races and deadlocks in multithreaded programs. SafeJava is expressive enough to support common programming patterns, its type checking is fast and scalable, and it requires little programming overhead. SafeJava thus offers a promising approach for making multithreaded programs more reliable. This paper presents a corresponding type system extension for the Java virtual machine language (JVML). We call the resulting language SafeJVML. Well-typed SafeJVML programs are guaranteed to be free of data races and deadlocks. Designing a corresponding type system for JVML is important because most Java code is shipped in the JVML format. Designing acorresponding type system for JVML is nontrivial because of important differences between Java and JVML. In particular, the absence of block structure in JVML programs and the fact that they do not use named local variables the way Java programs do make the type systems for Java and JVML significantly different. For example, verifying absence of races and deadlocks in JVML programs requires performing an alias analysis, something that was not necessary for verifying absence of races and deadlocks in Java programs. This paper presents static and dynamic semantics for Safe JVML. It also includes a proof that the SafeJVML type system is sound and that it prevents data races and deadlocks. To the best of our knowledge, this is the first type system for JVML that statically ensures absence of synchronization errors.

REFERENCES

• 1: Jonathan Aldrich , Valentin Kostadinov , Craig Chambers, Alias annotations for program understanding, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 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: Anindya Banerjee , David A. Naumann, Representation independence, confinement and access control [extended abstract], Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-177, January 16-18, 2002, Portland, Oregon
• 4: Peter Bertelsen. Dynamic semantics of Java bytecode. In Workshop on Principles of Abstract Machines, 1998.
• 5: Chandrasekhar Boyapati , Martin C. Rinard, Safejava: a unified type system for safe programming, Massachusetts Institute of Technology, 2004
• 6: 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
• 7: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira, Ownership types for object encapsulation, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-223, January 15-17, 2003, New Orleans, Louisiana, USA
• 8: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira , Chuang-Hue Moh , Steven Richman, Lazy modular upgrades in persistent object stores, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 9: 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
• 10: Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 11: Robert O'Callahan, A simple, comprehensive type system for Java bytecode subroutines, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-78, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292549]
• 12: Dave Clarke , Sophia Drossopoulou, Ownership, encapsulation and the disjointness of type and effect, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 13: David G. Clarke , John M. Potter , James Noble, Ownership types for flexible alias protection, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.48-64, October 18-22, 1998, Vancouver, British Columbia, Canada
• 14: Cormac Flanagan , Martín Abadi, Object Types against Races, Proceedings of the 10th International Conference on Concurrency Theory, p.288-303, August 24-27, 1999
• 15: 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
• 16: 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
• 17: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268961]
• 18: Stephen Neil Freund , John C. Mitchell, Type systems for object-oriented intermediate languages, Stanford University, Stanford, CA, 2000
• 19: Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.6, p.1196-1250, Nov. 1999 [doi>10.1145/330643.330646]
• 20: Stephen N. Freund , John C. Mitchell, A formal framework for the Java bytecode language and verifier, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.147-166, November 01-05, 1999, Denver, Colorado, United States
• 21: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 22: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 23: Futoshi Iwama , Naoki Kobayashi, A new type system for JVM lock primitives, Proceedings of the ASIAN symposium on Partial evaluation and semantics-based program manipulation, p.71-82, September 12-14, 2002, Aizu, Japan [doi>10.1145/568173.568182]
• 24: G. Klein , M. Wildmoser, Verified Bytecode Subroutines, Journal of Automated Reasoning, v.30 n.3-4, p.363-398, 2003 [doi>10.1023/A:1025095122199]
• 25: Neel Krishnaswami , Jonathan Aldrich, Permission-based ownership: encapsulating state in higher-order typed languages, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 26: Cosimo Laneve and Gaetano Bigliardi. A type system for JVM threads. In The Third ACM SIGPLAN Workshop on Types in Compilation (TIC), September 2000.
• 27: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 28: William Pugh, Fixing the Java memory model, Proceedings of the ACM 1999 conference on Java Grande, p.89-98, June 12-14, 1999, San Francisco, California, United States [doi>10.1145/304065.304106]
• 29: Zhenyu Qian, A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subrountines, Formal Syntax and Semantics of Java, p.271-312, January 1999
• 30: Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Languages, Verification

Keywords:
SafeJava, data races, deadlocks, ownership types