Previous article

Next article

An Operational Semantics including “Volatile” for Safe Concurrency

John Boyland, University of Wisconsin–Milwaukee, USA


PDF Icon
PDF Version


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.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the author


John Boyland is an Associate Professor in the Department of EE & Computer Science at the University of Wisconsin–Milwaukee. He can be reached at See also

John Boyland: "An Operational Semantics including “Volatile” for Safe Concurrency", in Journal of Object Technology, vol. 8, no. 4, Special Issue: Workhop FTfJP and IWACO at ECOOP 08, June 2009, pp. 33-53

Previous article

Next article