On 05/16/2018 09:19 PM, John Hening wrote:
> By the way, in your transcription you said:
> |
> inta;
>
> volatilebooleanready =false;
>
> voidactor(IntResult1r){
> while(!ready){};
> r.r1 =a;
> }
>
> voidobserver(){
> a =41;
> a =42;
> ready =true;
> a =43;
> }
> |
>
>
> You said that possible values for r1 are 42 and 43. I cannot understand why
> 41 is impossible. What
> does prevent write(a, 41) and write(a, 42) from being reordered?
Formally, there is no plausible JMM execution that yields both read(ready):true
and read(a):41,
which means observing 41 is forbidden in any conforming implementation.
Proof sketch starts from the realization that in all executions where we
observed r(ready):true it
is inevitable that:
w(ready, true) --hb--> r(ready):true
...which transitively extends to:
w(a, 41) --hb--> w(a, 42) --hb--> w(ready, true) --hb--> r(ready):true
--hb--> r(a):?
Happens-before consistency mandates that reads have to see either the latest
writes in
happens-before order, or any other write that does not connected by
happens-before. So, in the
execution above, you can only have r(a):42 [latest in HB], or r(a):43 [race].
But all of that is too low-level for day-to-day work. What you need is a more
high-level
abstraction: ready = true "released" the consistent view of stores in actor,
and once observer read
"ready == true", it "acquired" that consistent view. That's what safe
publication (or
release-acquire) basically is. Moreover, if there are no races, you cannot see
inconsistent (racy)
values, and then your program behaves as if it is sequentially-consistent (and
with caveats, this is
what SC-DRF says).
This high-level understanding plays well when you retract the thinking to
single-threaded case. What
exactly prevents the single thread seeing 41 in this example? What exactly
prevents the reordering
of two stores? ;)
void test() {
a = 41;
a = 42;
r1 = a;
}
You can use the similar JMM proof to work out that only 42 is allowed. But on
high level, it is the
same "consistent view", and release-acquire just extends it to the
multi-threaded case.
> JMM is a weak model. It means that JMM is allowed to reorder all normal
> memory operations provided
> that reordered program is equivalent in one-threaded environment. In my
> example I see nothing
> prevents reordering.
That's where the problem lies: once you think about the reorderings, you are
slipped into thinking
about the implementation, then barriers show up, and everything gets too
confusing. The trick is to
slap yourself every time "barrier" or "reordering" bubbles up :) Hardware and
runtime would speak to
each other to maintain the illusion that release-acquire works as you would
expect.
Coming back to the original slide you mentioned, roach motel semantics
basically says that it is
almost always safe for the implementation to move operations into the
release-acquire. It is harder
to prove that moving operations out is safe, but it is sometimes easily
provable too.
It is an interesting exercise to understand the implementation for
mechanical-sympathetic reasons
e.g. for performance modeling, but not so much for correctness proofs.
-Aleksey
--
You received this message because you are subscribed to the Google Groups
"mechanical-sympathy" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to mechanical-sympathy+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
signature.asc
Description: OpenPGP digital signature
