University of Sussex
Browse

File(s) under permanent embargo

An event-based structural operational semantics of multi-threaded Java

chapter
posted on 2023-06-07, 14:13 authored by Pietro Cenciarelli, Alexander Knapp, Bernhard ReusBernhard Reus, Martin Wirsing
A structural operational semantics of a significant sublanguage of Java is presented, including the running and stopping of threads, thread interaction via shared memory, synchronization by monitoring and notification, and sequential control mechanisms such as exception handling and return statements. The operational semantics is parametric in the notion of "event space" [6], which formalizes the rules that threads and memory must obey in their interaction. Different computational models are obtained by modifying the well-formedness conditions on event spaces while leaving the operational rules untouched. In particular, we implement the prescient stores described in [10, §17.8] which allow certain intermediate code optimizations, and prove that such stores do not affect the semantics of properly synchronized program

History

Publication status

  • Published

Journal

Formal Syntax and Semantics of Java

Publisher

Springer-Verlag

Volume

1523

Page range

157-200

Pages

404.0

Book title

Formal Syntax and Semantics of Java

Place of publication

Berlin, Germany

ISBN

9783540661580

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Editors

Jim Alves-Foss

Legacy Posted Date

2008-03-03

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC