Jeremy Manson <jmanson@cs.umd.edu> wrote:
> [Movement of memory operations out of synchronized blocks]
> isn't prevented because of memory semantics. It is prevented
> because introducing it would violate the requirement that any
> reordering remain operationally equivalent to the original ordering.
Thanks for the clarification.
I hope "operationally equivalent" doesn't involve some notion of
"correctness". Otherwise, I can imagine JVM/compiler implementors saying
"well, programs written like that aren't correct anyway so I won't even try
to preserve their operation". After all, there are lots of useful,
functional programs that aren't actually "correct" (well, most of them
probably).
By the way, do you have a name for your proposed model? The "operational
semantics" model is a bit vague.
----- Original Message -----
From: "Jeremy Manson" <jmanson@cs.umd.edu>
To: <javamemorymodel@cs.umd.edu>
Sent: Friday, March 30, 2001 3:48 PM
Subject: Re: JavaMemoryModel: Re: movement into synchronized blocks
> Because of the fences in CRF, it's easy to see what movement is allowed:
> memory operations can move into a lock region but can't move out.
>
> The operational semantics model is less direct in this regard.
>
> I can't see, from the operational definitions of lock and writeNormal,
> why a write can't move up out of a lock region. (Or may be it can.)
>
The trick is that it isn't prevented because of memory semantics. It is
prevented because introducing it would violate the requirement that any
reordering remain operationally equivalent to the original ordering. So you
have to prove you aren't changing the semantics of the program by moving the
write/read out of the lock region. For example, you can't introduce
deadlock. This is tricky, but since proving this sort of thing is possible
(I could imagine some sort of hoisting with variables which could be proven
thread-local), we should allow it.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:31 EDT