nvestigating Java Concurrency Using Abstract State Machines

  • Yuri Gurevich
  • Wolfram Schulte
  • Charles Wallace
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1912)


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.


Main Memory Load Action Read Action Execution Engine Store Action 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    E. Börger. Why use Evolving Algebras for hardware and software engineering? In Proceedings of SOFSEM, 1995.Google Scholar
  3. 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. 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. 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. 6.
    A. Gontmakher and A. Schuster. Java consistency: Non-operational characterizations for Java memory behavior. Technion/CS Technical Report CS0922, 1997.Google Scholar
  7. 7.
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.Google Scholar
  8. 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. 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. 10.
    Y. Gurevich. May 1997 draft of the ASM guide. Available at [22], 1997.Google Scholar
  11. 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. 12.
    C. Horstmann and G. Cornell. Core Java 1.1, volume II: Advanced Features. Sun Microsystems Press, 1998.Google Scholar
  13. 13.
    Sun Microsystems. Java technology home page.
  14. 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. 15.
    D. Lea. Concurrent Programming in Java. Addison-Wesley, 1997.Google Scholar
  16. 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. 17.
    S. Oaks and H. Wong. Java Threads. O’Reilly and Associates, 1997.Google Scholar
  18. 18.
    G. Plotkin. Structural Operational Semantics (Lecture notes). Technical Report DAIMI FN-19, Aarhus University, 1981.Google Scholar
  19. 19.
    W. Pugh. Fixing the Java memory model. In Proceedings of ACM Java Grande, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Yuri Gurevich
    • 1
  • Wolfram Schulte
    • 1
  • Charles Wallace
    • 2
  1. 1.Microsoft ResearchRedmondUSA
  2. 2.University of DelawareNewarkUSA

Personalised recommendations