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

Hi Alex,

Exactly! This seems so obvious today but appeared subtle
yesterday. ¯\_(ツ)_/¯

Regards,
Valentin www.kovalenko.link


On Wed, Feb 3, 2021 at 1:13 AM Alex Otenko <[email protected]>
wrote:

> 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