At 8:58 PM -0600 7/28/03, Yue Yang wrote:
>
>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.
Perhaps we forgot to state it since it so obvious:
No thread can obtain a lock on a monitor while another thread holds a
lock on that monitor. This property is checked against the total
order over all lock/unlock operations on each monitor.
We'll add something like that to the spec. Does that handle it?
Bill
-------------------------------
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