Jeremy Manson
William Pugh
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].
- 1.P. K. A. L. Cox and W. Zwaenepoel. Lazy release consistency for software distributed shared memory. In The Proceedings of the 19 th International Symposium of Computer Architecture, pages 13-21, May 1992. Google Scholar
Digital Library
- 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.Google Scholar
- 3.K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta, , and J. L. Hennessy. Memory consistency and event ordering in scalable shared-memory multiprocessors. In Proceedings of the Seventeenth International Symposium on Computer Architecture, pages 15-26, May 1990. Google ScholarDigital Library
- 4.J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison Wesley, 1996. Google ScholarDigital Library
- 5.The Java memory model. Mailing list and web page. http://www.cs.umd.edu/~pugh/java/memoryModel.Google Scholar
- 6.T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison Wesley, 2nd edition, 1999. Google ScholarDigital Library
- 7.A. J.-W. Maessen and X. Shen. Improving the Java memory model using CRF. In OOPSLA, pages 1-12, Oct. 2000. Google ScholarDigital Library
- 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.Google Scholar
- 9.W. Pugh. Fixing the Java memory model. In ACM Java Grande Conference, June 1999. Google ScholarDigital Library
- 10.W. Pugh. The double checked locking is broken declaration. http://www.cs.umd.edu/ users/ pugh/java/ memoryModel/ DoubleCheckedLocking.html, July 2000.Google Scholar
- 11.W. Pugh. The Java memory model is fatally flawed. Concurrency: Practice and Experience, 12(1):1-11, 2000.Google Scholar
Index Terms
- Core semantics of multithreaded Java
Recommendations
Specifying multithreaded Java semantics for program verification
ICSE '02: Proceedings of the 24th International Conference on Software EngineeringThe Java programming language supports multithreading where the threads interact among themselves via read/write of shared data. Most current work on multithreaded Java program verification assumes a model of execution that is based on interleaving of ...
Comments