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

The definition of happens-before is such that it is consistent with
synchronization order (see JMM spec).

Alex

On Wed, 3 Feb 2021, 00:56 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.
>
> 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