Very limited shared promotion

[Timon Gehr]

On 19.06.19 23:03, Walter Bright wrote:
> On 6/19/2019 6:45 AM, Timon Gehr wrote:
>> On 19.06.19 11:13, Walter Bright wrote:
>>>
>>> Using the resulting value of x:
>>>
>>>    int x;
>>>    void fun(scope ref shared(int) x) { ... }
>>>    fun(x); // implicit promotion to shared in this case
>>>    int y = x; // add this line
>>>
>>> And now there's a problem. The compiler thinks x is thread local, so 
>>> it doesn't add synchronization to the read of x.
>>
>> Probably `fun` should be `immutable` or `shared` as well. Otherwise 
>> there is no way to tell at the call site that it does not also capture 
>> `x` mutably, in which case the implicit promotion couldn't be allowed.
> 
> `scope` prevents capture of a reference to `x`, mutable or not, that 
> persists after the return from `fun`.
> ...

I was talking about this:

int x0;
void fun(scope ref shared(int) x1){
     assert(&x0 is &x1); //uh, oh
     // ...
}
fun(x);

> ...
>>
>> The compiler can allow the implicit conversion because in @safe code 
>> there is no way to send `scope` data to other threads and @trusted 
>> code has to respect `scope` guarantees.
> 
> The scope guarantees are NOT sequential consistency data-race-free 
> guarantees for multithreaded access.
> ...

Right now, in `@safe` code it guarantees that there is _no_ 
multithreaded access, no? How do you leak a `scope` reference to another 
thread? If there is _no_ multithreaded access, you don't get any data 
races, so `scope` guarantees no data races on the `scope`d memory 
location given that the reference wasn't accessible from multiple 
threads before.

> 
>>> In other words, adding `scope` does not guarantee SC-DRF (Sequential 
>>> Consistency - Data Race Free).
>> I think it does. The challenge is to ensure that the implicit 
>> promotion to `shared` doesn't result in `shared`/unshared aliasing. I 
>> don't think there is a problem with implicitly casting back to 
>> unshared, as the called function promises not to leak the references.
> 
> It does not. A write to an atomic is:
> 
>      write variable
>      read fence
> 
> A read from an atomic is:
> 
>      read fence
>      read variable
> 
> SC-DRF of atomics absolutely depends on this. The example code does:
> 
>    thread 1:
>      write x
>      read fence
> 
>    thread 2:
>      read x
> 
> This is wrong wrong wrong from what I know about atomics.
> ...

Yes, what's above certainly does not work. My point was that that is not 
what the code would do, at least not legally. If the above happens, 
there would be some `@trusted` code somewhere that you can blame for it.

Sending a `scope` variable to another thread is a `@system` operation. 
In order to ensure that `scope` guarantees are met, the `@trusted` code 
that performs the send needs to add memory barriers that ensure that all 
writes to the `scope` variable are visible on the current thread before 
it returns. So on thread 2 you would actually also have barriers before 
`x` is accessed again.

Let's consider a case _without_ implicit promotion:

shared(int) x=0; // x is shared all the way
static void foo(scope ref shared(int) x)@trusted{
     // possibly send &x to other threads that mutate it and
     // then forget about &x
     // ...
}
foo(x);
int y=x; // read x
enforce(x==y); // read x again

My claim is that if the enforcement fails, this indicates a bug in 
`foo`, because it violates guarantees you can derive from the fact that 
`x` is a local variable that is only passed to some other code via a 
`scope`d parameter: when `x` is read for the first time, we know that 
actually no other thread can have a reference to it which it can use for 
a write, so its value has to remain constant.

It should therefore be possible to read `x` without any further barriers 
after `foo` returns. This is because `foo` already needs to ensure all 
writes from other threads are visible.

It is possible that I am missing something (even though what you wrote 
is not it). Is there a possible implementation of `foo` that would be 
correct (in a language that does not have any implicit `shared` 
promotion), but for which a data race on `x` would result if we didn't 
add another fence before reading `x` after `foo` has returned?

> 
> ...
> 
> 5. When a data-race-free solution is found that doesn't follow fencing 
> protocols, it doesn't work.

We are on the same page on this. :)