Core semantics of multithreaded Java

ABSTRACT

Java has integrated multithreading to a far greater extent than most programming languages. It is also one of the only languages that specifies and requires safety guarantees for improperly synchronized programs. It turns out that understanding these issues is far more subtle and difficult than was previously thought. The existing specification makes guarantees that prohibit standard and proposed compiler optimizations; it also omits guarantees that are necessary for safe execution of much existing code. Some guarantees that are made (e.g., type safety) raise tricky implementation issues when running unsynchronized code on SMPs with weak memory models.

This paper reviews those issues. It proposes a new core semantics for Java that allows for aggressive compiler optimization and addresses the safety and multithreading issues. Due to space constraints, certain side issues are addressed only in the full version of the semantics [8].

REFERENCES

• 1: Pete Keleher , Alan L. Cox , Willy Zwaenepoel, Lazy release consistency for software distributed shared memory, Proceedings of the 19th annual international symposium on Computer architecture, p.13-21, May 19-21, 1992, Queensland, Australia
• 2: G. Gao and V. Sarkar. Location consistency - a new memory model and cache consistency protocol. Technical Report 16, CAPSL, Univ. of Deleware, Feb. 1998.
• 3: Kourosh Gharachorloo , Daniel Lenoski , James Laudon , Phillip Gibbons , Anoop Gupta , John Hennessy, Memory consistency and event ordering in scalable shared-memory multiprocessors, Proceedings of the 17th annual international symposium on Computer Architecture, p.15-26, May 28-31, 1990, Seattle, Washington, United States
• 4: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 5: The Java memory model. Mailing list and web page. http://www.cs.umd.edu/~pugh/java/memoryModel.
• 6: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 7: Jan-Willem Maessen , Xiaowei Shen, Improving the Java memory model using CRF, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-12, October 2000, Minneapolis, Minnesota, United States
• 8: J. Manson and W. Pugh. Semantics of multithreaded java. Technical Report CS-TR-4215, Dept. of Computer Science, University of Maryland, College Park, Mar. 2001.
• 9: 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]
• 10: W. Pugh. The double checked locking is broken declaration. http://www.cs.umd.edu/ users/ pugh/java/ memoryModel/ DoubleCheckedLocking.html, July 2000.
• 11: W. Pugh. The Java memory model is fatally flawed. Concurrency: Practice and Experience, 12(1):1-11, 2000.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Java

General Terms:
Design, Languages, Performance