Previous article

Next article

---

An Operational Semantics including “Volatile” for Safe Concurrency John Boyland, University of Wisconsin–Milwaukee, USA

REFEREED ARTICLE PDF Version

Abstract

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 boyland@cs.uwm.edu. See also http://www.cs.uwm.edu/faculty/boyland.