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

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