nvestigating Java Concurrency Using Abstract State Machines
We present a mathematically precise, platform-independent model of Java concurrency using the Abstract State Machine method. We cover all aspects of Java threads and synchronization, gradually adding details to the model in a series of steps. We motivate and explain each concurrency feature, and point out subtleties, inconsistencies and ambiguities in the official, informal Java specification.
KeywordsMain Memory Load Action Read Action Execution Engine Store Action
Unable to display preview. Download preview PDF.
- 1.I. Attali, D. Caromel, and M. Russo. A formal executable semantics for Java. In Proceedings of the OOPSLA’ 98 Workshop on the Formal Underpinnings of Java, 1998.Google Scholar
- 2.E. Börger. Why use Evolving Algebras for hardware and software engineering? In Proceedings of SOFSEM, 1995.Google Scholar
- 3.E. Börger and W. Schulte. A programmer friendly modular definition of the semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java. Springer, 1998.Google Scholar
- 4.P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. From sequential to multithreaded Java: An event-based operational semantics. In M. Johnson, editor, Alge-braic Methodology and Software Technology, pages 75–90. Springer, 1997.Google Scholar
- 5.E. Coscia and G. Reggio. A proposal for a semantics of a subset of multi-threaded “good” Java programs. In Proceedings of the OOPSLA’ 98 Workshop on the Formal Underpinnings of Java, 1998.Google Scholar
- 6.A. Gontmakher and A. Schuster. Java consistency: Non-operational characterizations for Java memory behavior. Technion/CS Technical Report CS0922, 1997.Google Scholar
- 7.J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.Google Scholar
- 8.Y. Gurevich. Evolving Algebras: an attempt to discover semantics. In G. Rozenberg and A. Salom∢, editors, Current Trends in Theoretical Computer Science, pages 266–292. World Scientific, 1993.Google Scholar
- 9.Y. Gurevich. Evolving Algebras 1993: Lipari guide. In E. Börger (editor), Specification and Validation Methods, Oxford University Press, 1995, 9–36.Google Scholar
- 10.Y. Gurevich. May 1997 draft of the ASM guide. Available at , 1997.Google Scholar
- 11.Y. Gurevich, W. Schulte and C. Wallace. Investigating Java concurrency using Abstract State Machines. Technical Report 2000-04, Department of Computer & Information Sciences, University of Delaware, 1999.Google Scholar
- 12.C. Horstmann and G. Cornell. Core Java 1.1, volume II: Advanced Features. Sun Microsystems Press, 1998.Google Scholar
- 13.Sun Microsystems. Java technology home page. http://java.sun.com/.
- 14.A. Jolin. Java’s atomic assignment: The key to simpler data access across threads. Java Report 3(8), 27–36, 1998.Google Scholar
- 15.D. Lea. Concurrent Programming in Java. Addison-Wesley, 1997.Google Scholar
- 16.M. MacBeth, K. McGuigan and P. Hatcher. Executing Java threads in parallel in a distributed memory environment. In Proceedings of IBM CASCON, 1998.Google Scholar
- 17.S. Oaks and H. Wong. Java Threads. O’Reilly and Associates, 1997.Google Scholar
- 18.G. Plotkin. Structural Operational Semantics (Lecture notes). Technical Report DAIMI FN-19, Aarhus University, 1981.Google Scholar
- 19.W. Pugh. Fixing the Java memory model. In Proceedings of ACM Java Grande, 1999.Google Scholar