An Operational Semantics including ‘Volatile’ for Safe Concurrency.
John Boyland · The Journal of Object Technology · 2009
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.