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

What you are describing is the definition of the closure of po and sw
consistent with so, which is hb.

Alex

On Wed, 3 Feb 2021, 01:39 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).
>
> 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. 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).
>
> 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).
> Therefore, hb(wx, wy) necessary leads to so(wx, releaseX), so(releaseX,
> acquireY), so(acquireY, wy), which gives so(wx, wy).
>
> I would highly appreciate it if someone could confirm this reasoning.
>
> 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