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

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