An Operational Semantics including Volatile for Safe Concurrency

by John Boyland.

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.

BibTeX Style Reference

@inproceedings(boyland:08concur,
  title = {An Operational Semantics including Volatile for Safe Concurrency}},
  author =      {John Boyland},
  booktitle = 	{ECOOP 2008 Workshop on Formal Techniques for
	         Java-like Programs},
  editor = 	{Marieke Huisman},
  month = 	jul,
  year = 	2008,
  nothing =	{})

How to Get a Copy

The paper is available, as in the source of the Twelf proof. The slides of the talk at FTfJP '08 are available.

Last Modified: June 6, 2008