JMM- conservative and formal point of view.

[John Hening]

The following picture comes from: https://shipilev.net/blog/2014/jmm-pragmatics/

As I understand this slide points that JMM does not constitute that a volatile write does not work as a (Load/Store)Store barrier, and it doesn't in fact.

But, JVM is allowed to reorder a such situation only in special cases, when the execution will be equivalent as if write(x,1) wouldn't be reorderd with release(g). In another words, here that reordering is allowed if and only if JVM is able to prove that it is equivalent to the situation without reordering.

The question is:

So, for considering correctness of program (and only correctness) can we assume that volatile store works as (Load/Store)Store barrier in fact?

However, a such simpilified view doesn't explain why JVM is able in some cases to hostile:

volatile x;
for(..)
  x += 1;

What do you think?

[Aleksey Shipilev]

On 05/16/2018 07:33 PM, John Hening wrote:
> Subject: JMM- conservative and formal point of view.

There is no "conservative" JMM point of view. There is JSR 133 Cookbook for Compiler Writers that
describes the conservative implementation, but it is not the JMM itself. Reductio ad absurdum:
suppose JSR 133 Fanfic for Concurrency Experts would say the easy way to be JMM conformant is to
acquire lock before entering any thread -- basically implementing Global Interpreter Lock. Would you
be willing to take the existence of GIL in some implementations as the guidance for writing reliable
software? I hope not.

> As I understand this slide points that JMM does not constitute that a volatile write does not work
> as a (Load/Store)Store barrier, and it doesn't in fact.

Double negation is confusing here. That slide points out that roach motel semantics basically says
that some transformations are easy (putting stuff "into" the acq/rel block), and others are still
possible, but hard. There are cases where it is not hard, actually: for example, when we know the
access is provably thread-local.

> But, JVM is allowed to reorder a such situation only in special cases, when the execution will be

> *equivalent as if write(x,1) wouldn't be reorderd with release(g)*. In another words, here that

> reordering is allowed if and only if JVM is able to prove that it is equivalent to the situation
> without reordering.

Caveat: when the *outcome* would be equivalent to some allowed JMM execution. It does not mean the
actual implementation should issue machine instructions in any given order.


> The question is:
>
> So, for considering *correctness* of program (and only *correctness*) can we assume that volatile

> store works as (Load/Store)Store barrier in fact?

No. The fluff about barriers is implementation details, which gets confusing very quickly as
implementations screw with your code.

I ranted about this a week ago at GeeCON:
https://shipilev.net/talks/geecon-May2018-jmm.pdf

-Aleksey

[John Hening]

Caveat: when the *outcome* would be equivalent to some allowed JMM execution. It does not mean the
actual implementation should issue machine instructions in any given order.

Obviously yes.

Aleksey, thanks for your response and presentation. I regret that I didn't take part in Geecon :(. I need to rethink a whole JMM, unfortunately :(.

By the way, in your transcription you said:

    int a;

    volatile boolean ready = false;

    void actor(IntResult1 r) {
        while (!ready){};
        r.r1 = a;
    }

    void observer() {
        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? 

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.

a = 42
a = 41
ready = true
a = 43

is equivalent to

a = 41;
a = 42;
ready = true;
a = 43;

[Aleksey Shipilev]

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

[John Hening]

Aleksey, thanks for your explanation. By the way, your presentation (I mean slides) is great- when it comes to the content and not only :-).

[John Hening]

@Aleksey,

At that weekend I've spent my time to understand deeply your presentation. Now, I think that I understand it much better (I don't risk saying that I understand it ;)). Thanks again for doing great job!

W dniu środa, 16 maja 2018 19:33:22 UTC+2 użytkownik John Hening napisał: