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

On Wed, Feb 3, 2021 at 2:56 AM Valentin Kovalenko via Concurrency-interest <
[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.
>

It is all about pretending a total order exists. So even if you have 2
unrelated writes, you can pretend a total order on the synchronisation
actions exists by either ordering wx before wy, or by ordering wy before wx.

It is like there are parallel universes and in each universe you can
pretend for example a total order over the synchronization actions exist.
The primary task is to determine if there is at least one universe that
matches the requirements of the memory model (e.g. sequential consistency
or TSO).


> However, if I try to imagine a program that produces executions with
> hb(wx, wy) and so(wy, wx) - I fail miserably.
>

Yes. You have run into a universe where the synchronization order is in
conflict with the happens-before order. So drop this universe and continue
with the other ones. If you can't find any universe that matches the
requirement, then your execution isn't consistent with the memory model.

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