An Operational Semantics including “Volatile”
for Safe Concurrency
John Boyland, University of Wisconsin–Milwaukee, USA
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: "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 http://www.jot.fm/issues/issue_2009_06/article2/