[concurrency-interest] Enforcing total sync order on modern hardware
TEREKHOV at de.ibm.com
Tue Mar 24 11:42:50 EDT 2015
Dekker is about store-load barrier and not about write atomicity (there is
only one observer of writes).
IRIW is about write atomicity and not about store-load barrier.
Oleksandr Otenko <oleksandr.otenko at oracle.com>@cs.oswego.edu on 24.03.2015
Sent by: concurrency-interest-bounces at cs.oswego.edu
To: Marko Topolnik <marko at hazelcast.com>
cc: concurrency-interest <Concurrency-interest at cs.oswego.edu>, Alexander
Terekhov/Germany/IBM at IBMDE
Subject: Re: [concurrency-interest] Enforcing total sync order on modern
On 24/03/2015 12:54, Marko Topolnik wrote:
On Tue, Mar 24, 2015 at 1:47 PM, Oleksandr Otenko <
oleksandr.otenko at oracle.com> wrote:
I don't know why you call IRIW a test of TSO, if total order of
reads is also important. Don't forget the load-load barrier,
which is implicit on x86, and a small theorem about what
happens when you don't order concurrent reads totally.
But note that you still don't need a total _global_ order of reads
for IRIW, it just has to be preserved locally for each processor.
Some, but not all, reorderings of concurrent reads are indistinguishable
from a certain fixed global total order of reads. What does this give you
apart from freedom of implementation?
Dekker's idiom exercises this more strongly because there has to be
global ordering between stores and loads by different processors.
Global ordering in Dekker's idiom you are talking about is also present in
IRIW. Dekker's idiom specifies more in program order:
r0=x; // program order po(r0=x, x=1); in IRIW it is in synchronization
order, so may be so(r0=x, x=1) or the other way around
r1=y; // "global order" between r1=y and y=1 executed by different
processors in Dekker's idiom is also present in IRIW
The outcome r1==0, r3==0 is disallowed through the same reasoning in
Dekker's idiom as in IRIW: since r1==0, y=1 must not happen before r1=y;
then r3=x, being after y=1 in program order, must also not precede r1=y,
and transitively cannot precede x=1. You need this step that from "Y must
not precede X" follows that "X happens-before Y" - but that's what makes
the order total.
In IRIW you have the same chain of reasoning. Even if you get rid of
synchronization order, but keep synchronizes-with and transitive closure,
then from observing r0==1 and r2==1 you still have the same edges. The key
here still is the conclusion that since r1==0, y=1 must not happen before
r1=y, which is the only part that requires total ordering - cannot be
partially ordered. But it is exactly the same bit that cannot be partially
ordered in Dekker's idiom: r1=y happens-before y=1 because otherwise r1=y
should observe 1. If you don't have mutual exclusion in ordering r1=y and
y=1 in Dekker's idiom, why would the outcome r1==0, r3==0 be forbidden?
I've seen others criticizing IRIW as being not realistic, but can you
support Dekker's idiom (which I reckon is realistic) without proving IRIW
at the same time? I wonder how that's possible. Or what gets forsaken.
Transitive closure goes? Ok, I see that happening; but then it is not about
total order as such.
Concurrency-interest mailing list
Concurrency-interest at cs.oswego.edu
More information about the Concurrency-interest