Thu Dec 24 09:54:15 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr000
"DpdR Fre SyncdWW Wse Rfe SyncsRR"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | | lwz r3,0(r2) ;
li r3,1 | | xor r4,r3,r3 ;
stw r3,0(r4) | | lwzx r5,r4,r6 ;
exists (y=2 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 27,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(11)
_litmus_P2_3_: xor 8,30,30
_litmus_P2_4_: lwzx 10,8,9
_litmus_P1_0_: li 7,2
_litmus_P1_1_: stw 7,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acssrr000 Allowed
Histogram (17 states)
41 :>2:r1=0; 2:r3=2; 2:r5=0; y=2;
30035985:>2:r1=0; 2:r3=0; 2:r5=0; y=2;
2732006:>2:r1=1; 2:r3=2; 2:r5=1; y=2;
8613240:>2:r1=2; 2:r3=1; 2:r5=1; y=1;
3736979:>2:r1=0; 2:r3=2; 2:r5=0; y=1;
26835246:>2:r1=0; 2:r3=0; 2:r5=1; y=2;
5367526:>2:r1=0; 2:r3=2; 2:r5=1; y=2;
24276794:>2:r1=1; 2:r3=1; 2:r5=1; y=2;
1253213:>2:r1=0; 2:r3=1; 2:r5=1; y=1;
1285742:>2:r1=0; 2:r3=2; 2:r5=1; y=1;
44021679:>2:r1=2; 2:r3=2; 2:r5=1; y=2;
961477:>2:r1=0; 2:r3=0; 2:r5=1; y=1;
14706205:>2:r1=0; 2:r3=1; 2:r5=1; y=2;
48122107:>2:r1=2; 2:r3=2; 2:r5=1; y=1;
47902323:>2:r1=1; 2:r3=1; 2:r5=1; y=1;
43940335:>2:r1=2; 2:r3=2; 2:r5=0; y=1;
96209102:>2:r1=0; 2:r3=0; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=9b30562cd1bddc4b5f352f23bca61947
Cycle=DpdR Fre SyncdWW Wse Rfe SyncsRR
Relax acssrr000 No ACSyncsRR
Safe=Fre Wse SyncdWW DpdR
Time acssrr000 77.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr001
"DpdR Fre SyncdWW Rfe SyncsRR Fre Rfe SyncsRR"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 3:r2=y; 3:r6=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) | | lwz r3,0(r2) ;
li r3,1 | | | xor r4,r3,r3 ;
stw r3,0(r4) | | | lwzx r5,r4,r6 ;
exists (y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=2 /\ 3:r5=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 31,0(11)
_litmus_P3_3_: xor 8,31,31
_litmus_P3_4_: lwzx 10,8,9
_litmus_P2_0_: li 8,2
_litmus_P2_1_: stw 8,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 11,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acssrr001 Allowed
Histogram (101 states)
1 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=2;
12 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=0; y=2;
4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=2;
4 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=2;
33 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=0; y=2;
3988 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
77761 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
16877 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
5396 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
48430 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
85956 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
83444 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
22488 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
321311:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
187753:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
19193 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
50199 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
454679:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
62968 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
206905:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
114177:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
89691 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
81292 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
77532 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
317472:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
242754:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
87066 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
162293:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
248029:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
581950:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
635031:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
478086:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
367591:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
1038338:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
249276:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1634502:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
253374:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
1528583:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
506933:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
358950:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
2577895:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
2843236:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
561087:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
1157544:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
1031079:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
107190:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
84056 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
1187386:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
1302883:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=1;
1187601:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
646913:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
505071:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
2148617:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
600116:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
2907773:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
373167:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
2398221:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
1024067:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; 3:r5=1; y=1;
758772:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=1;
520387:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
720287:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
7639932:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
4532506:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
13777814:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
2250359:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
2037458:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
3386350:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
940039:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
2145084:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
3216464:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
356495:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
3746461:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
712545:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; 3:r5=1; y=2;
8894949:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
17481027:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
16110250:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
6403503:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
665597:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
1790739:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=2;
2330572:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
3507041:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=0; y=1;
4934285:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
12480304:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
39521755:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
11782021:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
796918:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
1928906:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
1353984:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
3484353:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
11913854:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=1;
2759576:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=2;
805842:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3:r5=1; y=2;
9309112:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=1; y=1;
11042371:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 3:r5=1; y=2;
2932843:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; 3:r5=1; y=1;
9754598:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
5505237:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3:r5=1; y=2;
24192161:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
18163281:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; 3:r5=0; y=1;
4424661:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; 3:r5=1; y=2;
5645083:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; 3:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=2 /\ 3:r5=0) is NOT validated
Hash=c38aef8c23a4338efd925a04a5a3da9c
Cycle=DpdR Fre SyncdWW Rfe SyncsRR Fre Rfe SyncsRR
Relax acssrr001 No ACSyncsRR
Safe=Fre SyncdWW DpdR
Time acssrr001 103.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr002
"DpdR Fre Rfe SyncsRR DpdR Fre Rfe SyncsRR"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r6=x; 3:r2=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
sync | stw r1,0(r2) | sync | stw r1,0(r2) ;
lwz r3,0(r2) | | lwz r3,0(r2) | ;
xor r4,r3,r3 | | xor r4,r3,r3 | ;
lwzx r5,r4,r6 | | lwzx r5,r4,r6 | ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 2:r1=1 /\ 2:r3=1 /\ 2:r5=0)
Generated assembler
_litmus_P3_0_: li 7,1
_litmus_P3_1_: stw 7,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(11)
_litmus_P2_3_: xor 8,31,31
_litmus_P2_4_: lwzx 10,8,9
_litmus_P1_0_: li 8,1
_litmus_P1_1_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 31,0(11)
_litmus_P0_3_: xor 8,31,31
_litmus_P0_4_: lwzx 10,8,9
Test acssrr002 Allowed
Histogram (36 states)
1 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
6 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
9 :>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
10 :>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
22294 :>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
330186:>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
282757:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
254742:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
254963:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
1252016:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
318912:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
1314381:>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
881958:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=0;
958570:>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
2744243:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=0;
2348715:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
5292063:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=1; 2:r5=1;
2864778:>0:r1=0; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
13518291:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
8573343:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=1; 2:r5=1;
5434103:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
13584259:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
5482022:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
18603345:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=1;
18559162:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
5661373:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
17808624:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=1;
25219776:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
2411727:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=0;
57748677:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
45426250:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=0; 2:r3=0; 2:r5=0;
17758463:>0:r1=0; 0:r3=0; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
24969548:>0:r1=1; 0:r3=1; 0:r5=1; 2:r1=0; 2:r3=0; 2:r5=0;
5705614:>0:r1=1; 0:r3=1; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=1;
5563454:>0:r1=0; 0:r3=0; 0:r5=0; 2:r1=1; 2:r3=1; 2:r5=0;
8851365:>0:r1=0; 0:r3=1; 0:r5=1; 2:r1=1; 2:r3=1; 2:r5=1;
Ok
Witnesses
Positive: 1, Negative: 319999999
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 2:r1=1 /\ 2:r3=1 /\ 2:r5=0) is validated
Hash=4668b7b5f45d26e158378716e571271f
Cycle=DpdR Fre Rfe SyncsRR DpdR Fre Rfe SyncsRR
Relax acssrr002 Ok ACSyncsRR
Safe=Fre DpdR
Time acssrr002 84.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr003
"Fre SyncdWW Rfe SyncsRR DpdR Fre Rfe SyncsRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r6=y; 2:r2=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) | | lwz r3,0(r2) ;
li r3,1 | xor r4,r3,r3 | | ;
stw r3,0(r4) | lwzx r5,r4,r6 | | ;
exists (y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 8,1
_litmus_P2_1_: stw 8,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acssrr003 Allowed
Histogram (72 states)
8587 :>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=1; y=1;
353834:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=2; y=1;
18083 :>1:r1=0; 1:r3=1; 1:r5=1; 3:r1=0; 3:r3=1; y=1;
61350 :>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=2; 3:r3=1; y=1;
33067 :>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=0; 3:r3=1; y=1;
181177:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=0; 3:r3=2; y=2;
118583:>1:r1=0; 1:r3=1; 1:r5=1; 3:r1=0; 3:r3=2; y=1;
184458:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=1; y=2;
300498:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=1; y=2;
539112:>1:r1=0; 1:r3=1; 1:r5=1; 3:r1=2; 3:r3=1; y=1;
83139 :>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=2; y=1;
39986 :>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=0; 3:r3=2; y=1;
2463 :>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=1; y=1;
1360953:>1:r1=1; 1:r3=1; 1:r5=1; 3:r1=0; 3:r3=2; y=1;
303903:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=0; 3:r3=2; y=1;
68291 :>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=0; 3:r3=1; y=1;
402244:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=2; 3:r3=1; y=1;
369482:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=2; 3:r3=1; y=1;
647840:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=2; 3:r3=1; y=1;
58149 :>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=2; y=2;
132327:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=2; 3:r3=2; y=1;
1560132:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=0; 3:r3=1; y=2;
101699:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=0; 3:r3=2; y=2;
671051:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=2; 3:r3=1; y=1;
641935:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=1; 3:r3=2; y=2;
1806397:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=1; 3:r3=1; y=1;
440984:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=0; y=1;
70491 :>1:r1=1; 1:r3=1; 1:r5=1; 3:r1=0; 3:r3=1; y=1;
32864 :>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=2; y=2;
1449036:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=0; 3:r3=1; y=1;
516901:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=1; 3:r3=2; y=2;
1436143:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=1; 3:r3=1; y=1;
3230316:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=0; 3:r3=2; y=1;
5509924:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=1; 3:r3=1; y=1;
1435997:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=1; 3:r3=1; y=2;
7334704:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=2; 3:r3=2; y=1;
1049639:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=0; 3:r3=1; y=2;
1224106:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=1; 3:r3=2; y=2;
2257320:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=1; 3:r3=2; y=2;
3845448:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=2; 3:r3=2; y=1;
1723754:>1:r1=0; 1:r3=1; 1:r5=1; 3:r1=2; 3:r3=2; y=1;
3793770:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=0; 3:r3=1; y=2;
389834:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=0; y=1;
10502168:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=2; 3:r3=2; y=2;
16401258:>1:r1=1; 1:r3=1; 1:r5=1; 3:r1=2; 3:r3=2; y=1;
9976899:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=1; 3:r3=1; y=2;
2335919:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=1; 3:r3=1; y=1;
9105786:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=0; 3:r3=0; y=1;
1326855:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=0; y=2;
3072421:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=1; 3:r3=1; y=2;
7030480:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=2; 3:r3=2; y=1;
1898619:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=1; 3:r3=2; y=2;
8036015:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=2; 3:r3=2; y=1;
3791650:>1:r1=0; 1:r3=1; 1:r5=1; 3:r1=1; 3:r3=1; y=1;
13927481:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=0; 3:r3=0; y=2;
3033366:>1:r1=0; 1:r3=1; 1:r5=1; 3:r1=0; 3:r3=0; y=1;
4349130:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=0; 3:r3=0; y=1;
3531829:>1:r1=1; 1:r3=1; 1:r5=1; 3:r1=2; 3:r3=1; y=1;
10855114:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=0; 3:r3=0; y=2;
1499674:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=0; 3:r3=2; y=2;
26283344:>1:r1=0; 1:r3=0; 1:r5=1; 3:r1=1; 3:r3=1; y=2;
24915205:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=0; 3:r3=0; y=2;
12671720:>1:r1=0; 1:r3=0; 1:r5=2; 3:r1=2; 3:r3=2; y=2;
3309478:>1:r1=0; 1:r3=1; 1:r5=2; 3:r1=2; 3:r3=2; y=2;
22248015:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=0; 3:r3=0; y=1;
11234103:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=2; 3:r3=2; y=2;
2961959:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=0; 3:r3=0; y=2;
10004534:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=1; 3:r3=1; y=1;
8436037:>1:r1=1; 1:r3=1; 1:r5=2; 3:r1=2; 3:r3=2; y=2;
7596443:>1:r1=1; 1:r3=1; 1:r5=1; 3:r1=0; 3:r3=0; y=1;
24262675:>1:r1=1; 1:r3=1; 1:r5=1; 3:r1=1; 3:r3=1; y=1;
9611852:>1:r1=0; 1:r3=0; 1:r5=0; 3:r1=1; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=022d054a7e666fe8830d31d1e2f271fb
Cycle=Fre SyncdWW Rfe SyncsRR DpdR Fre Rfe SyncsRR
Relax acssrr003 No ACSyncsRR
Safe=Fre SyncdWW DpdR
Time acssrr003 98.40
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr004
"Fre SyncdWW Wse SyncdWW Rfe SyncsRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r2) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: lwz 4,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test acssrr004 Allowed
Histogram (18 states)
28549 :>2:r1=0; 2:r3=1; x=2; y=1;
2822726:>2:r1=0; 2:r3=2; x=2; y=1;
646464:>2:r1=0; 2:r3=2; x=1; y=1;
799830:>2:r1=0; 2:r3=1; x=1; y=1;
685602:>2:r1=2; 2:r3=1; x=1; y=1;
4861543:>2:r1=0; 2:r3=2; x=1; y=2;
5270156:>2:r1=2; 2:r3=1; x=2; y=1;
4606477:>2:r1=2; 2:r3=2; x=1; y=1;
12387157:>2:r1=0; 2:r3=1; x=1; y=2;
2577543:>2:r1=1; 2:r3=2; x=1; y=2;
28222885:>2:r1=1; 2:r3=1; x=1; y=1;
44223505:>2:r1=2; 2:r3=2; x=1; y=2;
14010820:>2:r1=1; 2:r3=1; x=2; y=1;
28739013:>2:r1=1; 2:r3=1; x=1; y=2;
34374304:>2:r1=0; 2:r3=0; x=2; y=1;
57607777:>2:r1=0; 2:r3=0; x=1; y=1;
93674839:>2:r1=2; 2:r3=2; x=2; y=1;
64460810:>2:r1=0; 2:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=3491c251ad1f32fc2b43d52f52c46191
Cycle=Fre SyncdWW Wse SyncdWW Rfe SyncsRR
Relax acssrr004 No ACSyncsRR
Safe=Fre Wse SyncdWW
Time acssrr004 79.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr005
"DpdR Fre SyncdWW Wse SyncdWW Rfe SyncsRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r6=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r2) ;
li r3,1 | li r3,1 | xor r4,r3,r3 ;
stw r3,0(r4) | stw r3,0(r4) | lwzx r5,r4,r6 ;
exists (y=2 /\ 2:r1=1 /\ 2:r3=1 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 27,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(11)
_litmus_P2_3_: xor 8,30,30
_litmus_P2_4_: lwzx 10,8,9
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test acssrr005 Allowed
Histogram (10 states)
11300041:>2:r1=0; 2:r3=1; 2:r5=0; y=1;
9071924:>2:r1=1; 2:r3=1; 2:r5=1; y=2;
10376615:>2:r1=1; 2:r3=1; 2:r5=0; y=1;
4799159:>2:r1=0; 2:r3=0; 2:r5=1; y=1;
82560883:>2:r1=1; 2:r3=1; 2:r5=1; y=1;
6977970:>2:r1=0; 2:r3=1; 2:r5=1; y=2;
14297449:>2:r1=0; 2:r3=1; 2:r5=1; y=1;
34405010:>2:r1=0; 2:r3=0; 2:r5=0; y=2;
102580883:>2:r1=0; 2:r3=0; 2:r5=1; y=2;
123630066:>2:r1=0; 2:r3=0; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=1 /\ 2:r5=0) is NOT validated
Hash=6b68dfe7e74c244d24f6a42341ecdcea
Cycle=DpdR Fre SyncdWW Wse SyncdWW Rfe SyncsRR
Relax acssrr005 No ACSyncsRR
Safe=Fre Wse SyncdWW DpdR
Time acssrr005 78.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr006
"Fre SyncdWW Rfe SyncsRR Fre SyncdWW Rfe SyncsRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 5,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 6,2
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 11,0(9)
_litmus_P0_0_: li 6,2
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acssrr006 Allowed
Histogram (108 states)
439 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
398 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
1378 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1675 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1243 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1868 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
2330 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
3830 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
23165 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
8320 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
82065 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
18345 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
6672 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
32785 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
8035 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
648927:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
23953 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
11254 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
13074 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
50756 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
17770 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
84971 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
25446 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
295436:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
613747:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
124157:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
66370 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
301540:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
123585:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
28083 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
156889:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
393349:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
33939 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
58314 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
214181:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
82844 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
202529:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
470734:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
630699:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
481819:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
121475:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
642215:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
300004:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
641789:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
1316890:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
484173:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1066 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
491955:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
486276:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
118889:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
136236:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
749810:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
832885:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1184455:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
1182380:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
2015974:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
80904 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
472347:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
2160705:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
2059707:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
3129474:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
2212261:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
3354601:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
4138477:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
6153025:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
2151109:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1293581:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
120098:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1355132:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
2123602:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
412531:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1843651:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
8441753:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
220889:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1085163:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
831059:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
3092941:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
677505:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
418974:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
842003:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
673828:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
646211:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
3368040:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3411033:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
10343 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
5815592:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
3478311:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
409667:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
19880846:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1199957:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
4064934:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
20234846:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1016590:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
18831219:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
1991857:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
19685408:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
6523382:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
19221303:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
1182554:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
628090:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
6140085:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
8432471:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
20016368:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
6410301:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
22733792:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
33607656:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
23420784:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
2239654:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=1749371cc26417072606d04b91651c05
Cycle=Fre SyncdWW Rfe SyncsRR Fre SyncdWW Rfe SyncsRR
Relax acssrr006 No ACSyncsRR
Safe=Fre SyncdWW
Time acssrr006 111.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/acssrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
acssrr007
"DpdR Fre SyncdWW Rfe SyncsRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) ;
li r3,1 | xor r4,r3,r3 ;
stw r3,0(r4) | lwzx r5,r4,r6 ;
exists (1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 31,0(11)
_litmus_P1_3_: xor 8,31,31
_litmus_P1_4_: lwzx 10,8,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test acssrr007 Allowed
Histogram (4 states)
91704352:>1:r1=0; 1:r3=1; 1:r5=1;
26075362:>1:r1=0; 1:r3=0; 1:r5=1;
307266203:>1:r1=0; 1:r3=0; 1:r5=0;
214954083:>1:r1=1; 1:r3=1; 1:r5=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=6c6ef868cbfa8678099a4f4472b504db
Cycle=DpdR Fre SyncdWW Rfe SyncsRR
Relax acssrr007 No ACSyncsRR
Safe=Fre SyncdWW DpdR
Time acssrr007 75.80
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Thu Dec 24 10:06:04 GMT 2009