[concurrency-interest] Enforcing total sync order on modern hardware

Oleksandr Otenko oleksandr.otenko at oracle.com
Tue Mar 24 11:48:24 EDT 2015

I must add that of course the totality of order between r1=y and y=1 is 
not the totality of order of all reads and writes - it is only the 
representation of atomicity of reads and writes of the same variable, 
which is reasonable to assume in any system.

What I stress on, is that IRIW results do /not/ require the order of 
/all/ reads and writes to be total - IRIW results can be proven from 
just /transitive closure/ of program order and synchronizes-with (even 
if you choose to construct the latter in some way different from JMM - 
not invoking total synchronization order).


On 24/03/2015 14:32, Oleksandr Otenko wrote:
> 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 <mailto: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:
> T1:
> x=1;
> 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
> T2:
> y=1;
> r2=y;
> r3=x;
> 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.
> Alex
>> ---
>> Marko
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20150324/445c5dee/attachment.html>

More information about the Concurrency-interest mailing list