Re: is HB consistent with SO for not otherwise related synchronization actions?

On Wed, Feb 3, 2021 at 3:40 AM Valentin Kovalenko via Concurrency-interest <
[email protected]> wrote:

> I believe, I found how to formally prove this.
>
> Same thread.
> If hb(wx, wy) and the actions wx, wy are performed by the same thread,
> then we have so(wx, wy) trivially due to both so and hb being consistent
> with the program order (po).
>

Correct.

If wx,wy are synchronization actions, then they are part of both so and po.

>
>
> Different threads.
> A more interesting situation is when wx and wy are performed by different
> threads, let us label them X and Y respectively. The only way to have a
> happens-before relation between actions performed by different threads X
> and Y is to have a synchronizes-with relation between a pair of
> synchronization actions in these threads.
>

Correct

>
> In other words, given hb(wx, wy), the execution must have actions releaseX
> performed by X and acquireY performed by Y, such that
> synchronizes-with(releaseX, acquireY) and po(wx, releaseX), po(acquireY,
> wy).
>

Your example is open for multiple interpretations. So I'll make it concrete
and hope it reflects what you have in mind.

int a;
volatile int b;

thread1(){
  a=1;
  b=1;
}

thread(){
  int rb=b;
  int ra=a;
  if(rb==1 && ra==0) println("violation");
}

And let's assume we see rb==1; what can we tell about a.

So we have the following:
po(a=1,b=1)
so(b=1,rb=b)
po(rb=b, ra=a)

So we have a hb(a=1,ra=a)=po(a=1,b=1), so(b=1,rb=b),po(rb=b, ra=a)

So we are good because the read of a should see the write of a and hence
"violation" can't be printed.


> Now we can see that hb(wx, wy) necessary leads to so(wx, releaseX),
> sw(releaseX, acquireY), so(acquireY, wy); and sw(releaseX, acquireY)
> necessary means so(releaseX, acquireY).
>

I'm not sure what wx,wy for actions are. If they are regular loads/stores
then they are not part of the so because they are not synchronization
actions.



> Therefore, hb(wx, wy) necessary leads to so(wx, releaseX), so(releaseX,
> acquireY), so(acquireY, wy), which gives so(wx, wy).
>

The question is if wx,wy are synchronization actions. If they are not, then
they are not part of so.  So in my example the so doesn't order (a=1,b=1)
and it doesn't order (rb=b, ra=a)

If a and b would both be volatile and hence become synchronization actions,
then the so would contain

(a=1,b=1),(b=1,rb=b),(rb=b,ra=a)


>
> I would highly appreciate it if someone could confirm this reasoning.
>

The definition of the so is that it is a total order over all
synchronization actions that is consistent with the po of each of the
threads.

So in case of the universes; it would filter out any universes that
- doesn't have a total order over all synchronization actions
- the total order of the synchronization actions isn't consistent with the
po of each of the threads.

Based on the so you can determine the sw order since it is a sub order of
so.

And based on the po and the sw, you can determine the hb order, i.e. the
transitive closure of the union of the po and the sw.


>
> Regards,
> Valentin www.kovalenko.link
>
>
> On Tue, Feb 2, 2021 at 5:53 PM Valentin Kovalenko <
> [email protected]> wrote:
>
>> Hi all,
>>
>> Imagine that we have only partial information about an execution (as is
>> almost always true in practice):
>> there are synchronization actions wx and wy such that happens-before(wx,
>> wy). These actions are not otherwise explicitly related, we may think of
>> them as being volatile writes to two different variables x and y.
>>
>> According to JMM, they are also ordered with the total synchronization
>> order. The order so(wx, wy) is a possibility that clearly does not violate
>> any JMM constraints. Interestingly, so(wy, wx) also does not seem to
>> violate anything, and, thus, should also be allowed.
>>
>> However, if I try to imagine a program that produces executions with
>> hb(wx, wy) and so(wy, wx) - I fail miserably. Whatever I imagine is needed
>> to have hb(wx, wy) in an execution, causes this execution to have so(wx,
>> wy).
>>
>> So maybe happens-before order is always consistent with the
>> synchronization order (if this is not the case, could someone come up with
>> a counterexample)? If this is the case, is there a way to formally deduce
>> it from JMM without resorting to the argument "I can't imagine a program
>> that produces executions with hb not being consistent with so"?
>>
>> Thank you,
>> Valentin www.kovalenko.link
>>
> _______________________________________________
> Concurrency-interest mailing list
> [email protected]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>

_______________________________________________
Concurrency-interest mailing list
[email protected]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest