> The model is that you have a global system that, in each
> step, executes one operation from one thread. Thus, there
> is a total order over the execution of all operations.
Why make this assumption? You don't seem to depend on it? It seems like
this could introduce accidental properties into the semantics that you
don't really intend.
> Each lock operation on a monitor m is immediately followed by
> an acquire operation on m, and each unlock operation is immediately
> preceded by a release operation on m. Similarly, each read of
> a volatile variable v is immediately followed by an acquire operation
> on v, and each write operation on v is immediately preceded
> by a release operation on m.
I must admit to not being fully conversant with the implications of saying
that an operation is an "acquire" or a "release."
I understand the following:
> When a thread t acquires monitor m,
> thread t updates its overwritten and previous information
> with that of the monitor ... [:]
>
> For each variable v,
> overwritten_t(v) = overwritten_t(v) union overwritten_m(v)
> previous_t(v) = previous_t(v) union previous_m(v)
>
> When a thread t performs a release on a monitor, the overwritten and
> previous information from the thread is merged into the overwritten
> and previous information for the monitor:
>
> For each variable v,
> overwritten_m(v) = overwritten_m(v) union overwritten_t(v)
> previous_m(v) = previous_m(v) union previous_t(v)
However, I do not fully understand the following:
> Acquire and releases on volatile variables work the same way as
> for monitors ...
Do you mean there is a function "overwritten_v" for each volatile variable
"v", and that the above two acquire/release formulas hold for this
variable? For example, for a read/acquire of volatile variable "v", we
would have the formula:
For each variable v',
overwritten_t(v') = overwritten_t(v') union overwritten_v(v')
previous_t(v') = previous_t(v') union previous_v(v')
This would occur just prior to the read rather than just after, right? If
so, perhaps you should say "acquire/read" rather than "read/acquire" (but
continue to use "write/release").
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:21 EDT