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 =	{})

@article(boyland:09concur,
  title = {An Operational Semantics including Volatile for Safe Concurrency}},
  author =      {John Boyland},
  journal = "Journal of Object Technology",
  month = jun,
  year = 2009,
  volume = 8,
  number = 4,
  pages = 33-53)

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. The JOT article is online, but the PDF available from the JOT website is defective. Please use my corrected copy instead.


Last Modified: January 3, 2011

An Operational Semantics including Volatile for Safe Concurrency / boyland@cs.uwm.edu