JavaMemoryModel: Mutual exclusion effect of locks

From: Yue Yang (yyang@cs.utah.edu)
Date: Mon Jul 28 2003 - 22:58:28 EDT


The monitor enter and the corresponding monitor exit operation impose
a critical section effect for the code between them. That is, they should
be properly nested. Although this is an apparent requirement, the JMM
would not be complete without stating it.

I don't believe the latest rules outlined by Bill/Jeremy or Sarita would
be sufficient to enforce the mutual exclusion effect of locks.

Bill/Jeremy's spec requires the following:

"There is a total order between all lock and unlock actions on the same
monitor. There is a happens-befoe edge from an unlock action on monitor
m to all subsequent lock actions on m (where subsequent is defined
according to the total order over the actions on m)."

Consider the code below:

t1 t2
(1) lock m; (4) lock m;
(2) ... (5) ...
(3) unlock m; (6) unlock m;

The total order on operations with m could have been (1) (4) (3) (6),
which violates the mutual exclusion effect.

Serita's model requires a happens-before relation between I and J if
"I is a synchronization write and J is a synchronization read that returns
the value written by I". But it's not clear how the synchronization value
is defined for locks to prohibit the interleaving shown above.
(Sarita, please clarify if I'm wrong.)

- Yue

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



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