[concurrency-interest] Enforcing total sync order on modern hardware
Oleksandr Otenko
oleksandr.otenko at oracle.com
Thu Mar 19 13:07:17 EDT 2015
Your scenario is exactly IRIW.
T9 is x=1
Wv1 is y=1
Rrt9 is r0=x
Rv0 is r1=y
T6 is initial x=0
Rwt6 is a constraint that you want to consider only total orders with
y=1 preceding x=1
It is equivalent to the independent reader thread doing r2=y, then r3=x,
and observing r2==1, r3==0. That is, you have reformulated IRIW in such
a way so that we consider only one specific outcome, not all possible
outcomes.
T1:
x=1
T2:
y=1
T3:
r0=x;
r1=y;
T4:
r2=y;
r3=x;
JMM forbids the outcome (r0,r1,r2,r3) = (1,0,1,0) - ie one thread
thinking x=1 happened before y=1, the other thread thinking y=1 happened
before x=1.
What you are missing from the diagram here:
http://cs.oswego.edu/pipermail/concurrency-interest/2015-March/014118.html
is a synchronizes-with edge from Wv1 to Rv0 - because you didn't
convince yourself that one must exist. If it does exist, then Rv0 will
observe the latest write from synchronization order it synchronizes with.
The presence of that edge is proven in the same way as for IRIW: we
demonstrate an even stronger statement that Rwt6 is before T9 in
synchronization order; otherwise, Rwt6 must observe T9 (the rule about
consistency of read operations - reads observe the last write they
synchronize-with). Then from program orders it follows that Wv1 appears
before Rv0 in synchronization order, so Rv0 synchronizes-with Wv1 and
observes v==1 as the last write it synchronizes-with.
Alex
On 19/03/2015 13:21, Marko Topolnik wrote:
>
> On Tue, Mar 17, 2015 at 10:42 PM, Stephan Diestelhorst
> <stephan.diestelhorst at gmail.com
> <mailto:stephan.diestelhorst at gmail.com>> wrote:
>
>
> IRIW is ruled out by both AMD and Intel. Not a problem.
>
>
> My scenario is not quite IRIW.
...
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20150319/77fc0650/attachment.html>
More information about the Concurrency-interest
mailing list