The Nonlinearity of volatile in Java

by John Boyland.

Abstract

Linear logic and related logics (such as separation logic and fractional permissions) have proven useful in verifying %non-interference in concurrent programs because they make it easy to reason about heap separation properties. However ``volatile'' fields in Java are difficult to reason about in strictly linear fashion. Volatile is much more easier handled using non-linear concepts such as immutability and ownership.

BibTeX Style Reference

@inproceedings(boyland/retert/zhao:07iterators,
  title = {The Non-Linearity of \texttt{volatile} in Java}
  author =      {John Boyland}
  booktitle = 	{ECOOP 2008 Workshop on Aliasing, Confinement and Ownership in object-oriented programming},
  editor = 	{Peter M\"{u}ller}
  month = 	jul,
  year = 	2008,
  nothing =	{})

How to Get a Copy

The PDF is available here. The slides for the presentation are also available.