Dear memory modelers:
I for one would find it really helpful to have an operational model that
reflects the semantics we are aiming for. By that I mean something that
allows the maximum reordering, etc., in the shared memory. The case of
concern is data races, I believe.
I am not proposing a particular model, but maybe it would have a flavor
like this:
writes propagate to a memory that keeps multiple, not necessarily
in-sync, copies of each memory location, with no guarantee on the
delay in a write action reaching a particular copy
correct use of synchronization primitives (mutexes in particular)
guarantees that all copies are updated and in-sync, and no write
actions are still propagating
writes by the same thread to the same location happen in the same
order (namely execution order) at every copy
a read simply reads the value of any copy
there number of copies is finite (maybe it can even vary), and it is
at least one
In other words, this allows arbitrary "flipping" around between the values
written by unsynchronized writes (races), and this will "settle" only by
using synchronization primitives (by which I mean to include volatiles).
there is a total order of all volatile writes (i.e., across all
threads) to the same location, consistent with program order in each
thread; the writes are applied to each copy in that same order.
Note that if there is a write then a read of a volatile by the same thread,
then the read must return the value written, or some later (by the total)
value.
This STILL requires capturing what is legal within a thread, and I know the
hard part is what a compiler may do, but my previous email was intended to
advance the cause on that score.
Part of the point here is that I think an operational model like this is
easier to visualize and explain, and easier to demonstrate the possibility
or absence of certain behaviors ....
If, in not following quite as closely or deeply, I am missing the point,
then just keep plowing ahead ....
-- Eliot
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT