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, x17.8] which allow certain intermediate code optimizations, and prove that such stores do not affect the semantics of properly synchronized programs.
CITATION STYLE
Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1999). An event-based structural operational semantics of multi-threaded java. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1523, 157–200. https://doi.org/10.1007/3-540-48737-9_5
Mendeley helps you to discover research relevant for your work.