An Operational Semantics including ‘Volatile’ for Safe Concurrency

By: John Boyland


In this paper, we define a novel “write-key” operational semantics for a kernel language with fork-join parallelism, synchronization and “volatile” fields. We prove that programs that never suffer write-key errors are exactly those that are “data race free” and also those that are “correctly synchronized” in the Java memory model. This 3-way equivalence is proved using Twelf.

Cite as:

John Boyland, “An Operational Semantics including ‘Volatile’ for Safe Concurrency”, Journal of Object Technology, Volume 8, no. 4 (June 2009), pp. 33-53, doi:10.5381/jot.2009.8.4.a2.

PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn

The JOT Journal   |   ISSN 1660-1769   |   DOI 10.5381/jot   |   AITO   |   Open Access   |    Contact