JavaMemoryModel: "synchronizes with"

From: Doug Lea (dl@cs.oswego.edu)
Date: Thu Mar 25 2004 - 08:10:44 EST


Thanks to Bart for proposing a rigorous definition of "synchronizes with".
A proposed further variant is below.

But first, more motivation. As I've already whined about, the
terminology here is at best crummy. If you try to teach or explain the
central happens-before relation, you will probably see students and
programmers say things like: "does this event happen before this other
event that it happens before?". And get confused, and give up or screw
up. Concurrent programming is hard enough without introducing yet
another path to error. If we don't supply a better way to discuss and
describe it, people will still do so in terms of "barriers" and the
like, as Sarita, especially, is so unhappy about. (Digression: for
compiler/JVM developers, it IS fine to discuss most issues in terms of
barriers, since one of their main tasks is to figure out how and when
to place barrier instructions.)

Bart nicely expanded on my suggestion to use "synchronizes with"
instead here. I think we can adopt an equally rigorous usage that
will still also allow use of "happens before" in main spec, by
identifying "synchronizes-with" with the second clause of the HB
definition. As in:

I happens-before J if:
  1) I is before J in program order
  2) I synchronizes-with J
  3) I happens-before K happens-before J for some K

I synchronizes-with J if:
   I is an unlock or volatile write, and J is a matching unlock or
   volatile read that comes after I in the total order of
   synchronization actions.
   [Or whatever exact wording JSR133 decides to go with here.]

This would allow use of the term "synchronizes with" in most of the
important cases where people need to think about this. You might want
to try this out yourself on some of the posted test cases or classic
examples like double-check to see how it sounds. To me, it seems a
bit more intuitive, more supportive of ad-hoc informal reasoning, and
less prone to error than using only "happens-before".

I propose that the JLS and JSR133 spec adopt this terminology or
some similar further refinement.

-Doug
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:01 EDT