iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/3-540-64299-4_47
Verifying a compiler optimization for multi-threaded Java | SpringerLink
Skip to main content
Springer Nature Link
Log in

Verifying a compiler optimization for multi-threaded Java

  • Contributed Papers
  • Conference paper
  • First Online:
Recent Trends in Algebraic Development Techniques (WADT 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1376))

Included in the following conference series:

Abstract

The specification for the object-oriented concurrent language Java [3] is rather loose with respect to the interaction of shared memory and the local working memories of different threads. This allows maximal freedom in the language implementation. Such freedom is reflected in the semantics provided in [2], where threads-memory interaction is formalized in terms of structures called event spaces. Two kinds of memories are described in the Java specification: a “normal” memory and a more liberal one, where values can sometimes be stored even before they are produced as results of computation. Here we compare two structural operational semantics of a sublanguage of Java modelling the two types of memory. The two semantics share the same set of operational rules but put different requirements (expressed as first order theories) on the notion of event space. We prove a result which is informally stated in

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Ken Arnold and James Gosling. The Java Programming Language. Addison-Wesley, Reading, Mass., 1996.

    Google Scholar 

  2. Pietro Cenciarelli, Alexander Knapp, Bernhard Reus, and Martin Wirsing. From Sequential to Multi-Threaded Java: An Event-Based Operational Semantics. In Proc. 6 th Int. Conf. Algebraic Methodology and Software Technology, Lect. Notes Comp. Sci., Berlin, 1997. Springer. To appear.

    Google Scholar 

  3. James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, Reading, Mass., 1996.

    Google Scholar 

  4. Doug Lea. Concurrent Programming in Java. Addison-Wesley, Reading, Mass., 1997.

    Google Scholar 

  5. Gordon D. Plotkin. Structural Operational Semantics (Lecture notes). Technical Report DAIMI FN-19, Aarhus University, 1981 (repr. 1991).

    Google Scholar 

  6. Glynn Winskel. An Introduction to Event Structures. In Jacobus W. de Bakker, editor, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency,, volume 354 of Lect. Notes Comp. Sci., Berlin, 1988. Springer.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Ludwig-Maximilians-Universität, München

    Bernhard Reus, Alexander Knapp, Pietro Cenciarelli & Martin Wirsing

Authors
  1. Bernhard Reus
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Knapp
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pietro Cenciarelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martin Wirsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Francesco Parisi Presicce

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reus, B., Knapp, A., Cenciarelli, P., Wirsing, M. (1998). Verifying a compiler optimization for multi-threaded Java. In: Presicce, F.P. (eds) Recent Trends in Algebraic Development Techniques. WADT 1997. Lecture Notes in Computer Science, vol 1376. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-64299-4_47

Download citation

  • DOI: https://doi.org/10.1007/3-540-64299-4_47

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64299-2

  • Online ISBN: 978-3-540-69719-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation