Mon Dec 28 13:27:49 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw000
"DpdR SyncsRW Rfe SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r5=x;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
sync | xor r3,r1,r1 | sync | xor r3,r1,r1 ;
li r3,2 | lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
stw r3,0(r2) | sync | stw r3,0(r2) | sync ;
| li r6,1 | | li r6,1 ;
| stw r6,0(r5) | | stw r6,0(r5) ;
exists (x=2 /\ y=2 /\ 0:r1=1 /\ 1:r1=2 /\ 1:r4=0 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 30,0(11)
_litmus_P3_1_: xor 10,30,30
_litmus_P3_2_: lwzx 31,10,9
_litmus_P3_3_: sync
_litmus_P3_4_: li 8,1
_litmus_P3_5_: stw 8,0(9)
_litmus_P2_0_: lwz 6,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 5,0(9)
_litmus_P0_1_: sync
_litmus_P0_2_: li 11,2
_litmus_P0_3_: stw 11,0(9)
Test bcssrw000 Allowed
Histogram (95 states)
173319:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
125702:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
48286 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
163451:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
36327 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
451498:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
847504:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
159738:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
34299 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
49542 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
162213:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
193138:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
25334 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
213848:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
613033:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
74802 :>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
326105:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
671054:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
137103:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
44390 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
98001 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
169058:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
75134 :>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
229286:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
430974:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
163127:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
150283:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
487025:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
1992747:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
433110:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
44782 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
2183882:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
122363:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
33087 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
167187:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
390702:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1982272:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
169362:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
934534:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
724271:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
2405078:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1926357:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2092273:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
187372:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
449991:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
642403:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
863847:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
436173:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
146430:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
2172800:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
2315377:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
2929486:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
2511832:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
1890540:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
2667405:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
1010950:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
1587256:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
508770:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
4038437:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
168617:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
4583670:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2531319:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
2173055:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
2715117:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1405303:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
2477408:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
2996382:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
8900935:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
3081888:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
5714595:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
5845567:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3077070:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
1304782:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
659225:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
833474:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
5613686:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
5645442:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
859812:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
905813:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
5567807:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
563448:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
7798313:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2320004:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2149325:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
4520373:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
4601025:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2928966:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1114297:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
5497856:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1029822:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
3238950:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
2458457:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
1992594:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
573071:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
5837882:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 160000000
Condition exists (x=2 /\ y=2 /\ 0:r1=1 /\ 1:r1=2 /\ 1:r4=0 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r4=0) is NOT validated
Hash=b7e6e6df4355fb418bf475952119efba
Cycle=DpdR SyncsRW Rfe SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw000 No BCSyncsRW
Safe=DpdR
Time bcssrw000 94.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw001
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync | xor r3,r1,r1 ;
lwzx r4,r3,r5 | li r3,2 | lwzx r4,r3,r5 ;
sync | stw r3,0(r2) | sync ;
li r6,1 | | li r6,1 ;
stw r6,0(r5) | | stw r6,0(r5) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw001 Allowed
Histogram (17 states)
2489491:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
4753468:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
11244471:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2656462:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
15553150:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
3281258:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
5162799:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
22412025:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
9124791:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
13472092:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
4288291:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
19090048:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
26051225:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
4132894:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
38910308:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
714892:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
16662335:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=0b5e63c8ef234eb2e941f5c51f0aef20
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw001 No BCSyncsRW
Safe=DpdR
Time bcssrw001 50.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw002
"SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync | sync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
sync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | sync ;
| | li r7,1 ;
| | stw r7,0(r6) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 26,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 27,0(11)
_litmus_P2_3_: xor 8,27,27
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: sync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw002 Allowed
Histogram (30 states)
187250:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
453121:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
157813:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
308310:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
227421:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
458593:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
271236:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
380555:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
63754 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
335295:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
2542464:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
45713 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
528251:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
4568183:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3985903:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
2597771:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
5156947:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
14481140:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
4748105:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
1806147:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
13210040:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
12890104:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
23423526:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
1649469:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
25395219:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
7314552:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
19199551:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
2234710:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
38325424:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
13053433:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=11796ca5759756e415169a54d5d677e2
Cycle=SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw002 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw002 59.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw003
"LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 2:r2=y; 2:r6=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync | lwsync ;
lwzx r4,r3,r5 | li r3,2 | lwz r3,0(r2) ;
sync | stw r3,0(r2) | xor r4,r3,r3 ;
li r6,1 | | lwzx r5,r4,r6 ;
stw r6,0(r5) | | sync ;
| | li r7,1 ;
| | stw r7,0(r6) ;
exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 26,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 27,0(11)
_litmus_P2_3_: xor 8,27,27
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: sync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw003 Allowed
Histogram (31 states)
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
3383 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
46294 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
87187 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
23314 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
106718:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
56589 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
98068 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
20038 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
3083766:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
185884:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
2969 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
106831:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
726474:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
4857429:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
168220:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
10973062:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
610729:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
6468139:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
5667294:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
13438777:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
8288982:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
2359797:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
23388842:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
3312926:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
38595113:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
26771707:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
6726227:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
18787689:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
13504157:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
11533394:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=2 /\ 2:r5=0) is NOT validated
Hash=f0d60999a697d3eb825e725dab825965
Cycle=LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw003 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw003 56.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw004
"DpdW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | xor r3,r1,r1 ;
sync | li r3,2 | li r4,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stwx r4,r3,r5 ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw004 Allowed
Histogram (22 states)
536348:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
188099:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
356795:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
548231:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
5947539:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1510502:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
12667830:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
4668576:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
10846591:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
3478112:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
7903787:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
2101238:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
13542372:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
2602887:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
9068402:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
37908882:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
15694436:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
17251326:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
12639300:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
35686444:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
3029701:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
1822602:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=2b45cfbf06c32c061b1ef2291b80e3a8
Cycle=DpdW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw004 No BCSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bcssrw004 56.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw005
"SyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync ;
sync | li r3,2 | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw005 Allowed
Histogram (22 states)
287588:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
605787:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
245265:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
13622074:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
9768595:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
8062602:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
1218163:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
530974:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
1288321:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
2487533:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
4301576:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
6309747:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
7578639:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
19312542:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
2968767:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
2332254:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
8366036:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
7355470:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
12030409:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
12247539:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
37357748:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
41722371:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=921da9ec68c9cae42224f4aee8da9e15
Cycle=SyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw005 No BCSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bcssrw005 55.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw006
"LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwsync ;
sync | li r3,2 | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw006 Allowed
Histogram (24 states)
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=2;
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
295494:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
566017:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
282442:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
1168111:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
4679072:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
1208795:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
8922476:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
13193989:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
2338125:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
3342064:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
7572445:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
9060756:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
1298662:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
5519616:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
8079014:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
2373267:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
11482391:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
15600628:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
41359102:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
34009306:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
9920671:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
17727555:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2) is NOT validated
Hash=ec356be30e18f54ebeedc96f10f9b03d
Cycle=LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw006 No BCSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bcssrw006 55.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw007
"DpdR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | xor r3,r1,r1 ;
sync | li r3,2 | lwzx r4,r3,r5 ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw007 Allowed
Histogram (17 states)
3045389:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
1103767:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
12978374:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
9444360:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
8239340:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
35450366:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
4518011:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
2535324:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
11105116:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
9211640:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
12065319:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
3272886:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
6687252:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
13778777:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
19348885:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
44956545:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2258649:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=befe5b0646d37c624367af2f5d68102e
Cycle=DpdR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw007 No BCSyncsRW
Safe=Fre SyncsWR DpdR
Time bcssrw007 52.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw008
"SyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync ;
sync | li r3,2 | lwz r3,0(r4) ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw008 Allowed
Histogram (18 states)
1 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
11594181:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
5319708:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
9882387:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
2461471:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
15513460:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
6848142:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
3847425:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
35722953:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
9992656:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
9301244:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
47662576:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
2783967:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
4362927:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
10235262:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
5107176:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
18602329:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
762135:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=a20320b515d5d6be92359c592ff3a749
Cycle=SyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw008 No BCSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bcssrw008 53.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw009
"LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwsync ;
sync | li r3,2 | lwz r3,0(r4) ;
lwz r3,0(r2) | stw r3,0(r2) | ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw009 Allowed
Histogram (19 states)
3 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
1 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
12075849:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
7009030:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
2375986:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
10500331:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
1150178:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
5429405:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
4890023:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
2775826:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
9868786:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
4008237:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
8133141:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
36191203:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
9569738:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
3515306:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
19317776:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
47493430:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
15695751:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=b007f90666b53b8e1b409ebed80da9b2
Cycle=LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw009 No BCSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bcssrw009 51.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw010
"DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
sync | sync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | sync ;
lwzx r5,r4,r6 | | li r6,1 ;
sync | | stw r6,0(r5) ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 26,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 27,0(11)
_litmus_P0_3_: xor 8,27,27
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw010 Allowed
Histogram (22 states)
498291:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
428934:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
2984988:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
396230:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
26183522:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4101062:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3322237:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
560238:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
18534493:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
6505909:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
13122046:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3112943:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
7296832:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
17073564:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2506539:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3255829:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
4704932:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
641031:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
26982825:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
39901505:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9588107:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
8297943:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=2770695d9c722f87a04175621ac51ca6
Cycle=DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw010 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw010 52.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw011
"DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync | sync | xor r3,r1,r1 ;
lwz r3,0(r2) | li r3,2 | lwzx r4,r3,r5 ;
xor r4,r3,r3 | stw r3,0(r2) | sync ;
lwzx r5,r4,r6 | | li r6,1 ;
sync | | stw r6,0(r5) ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 5,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 26,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 27,0(11)
_litmus_P0_3_: xor 8,27,27
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Test bcssrw011 Allowed
Histogram (22 states)
86597 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
31411 :>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
607245:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
104356:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
107829:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
707841:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3354134:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
4456409:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
6943474:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
19593505:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
4616699:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3407223:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
12260978:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
3455787:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
12488719:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
4200046:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
14549543:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
12936903:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
6579439:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
35820665:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
28811526:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
24879671:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=ae75e3d1140839ad4046415fb4f32715
Cycle=DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw011 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw011 53.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw012
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 ;
sync | sync ;
li r6,1 | li r6,1 ;
stw r6,0(r5) | stw r6,0(r5) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw013
"DpdR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 | lwzx r4,r3,r5 ;
sync | sync | sync ;
li r6,1 | li r6,1 | li r6,1 ;
stw r6,0(r5) | stw r6,0(r5) | stw r6,0(r5) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw014
"DpsR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=y; 0:r5=x; 1:r2=x; 1:r5=y; 2:r2=y;}
P0 | P1 | P2 ;
lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | xor r3,r1,r1 | xor r3,r1,r1 ;
lwzx r4,r3,r5 | lwzx r4,r3,r5 | lwzx r4,r3,r2 ;
sync | sync | sync ;
li r6,1 | li r6,1 | li r5,2 ;
stw r6,0(r5) | stw r6,0(r5) | stw r5,0(r2) ;
exists (y=2 /\ 0:r1=2 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=1)
Generated assembler
_litmus_P2_0_: lwz 31,0(9)
_litmus_P2_1_: xor 10,31,31
_litmus_P2_2_: lwzx 11,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,2
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw014 Allowed
Histogram (21 states)
4784 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
80586 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
115143:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
152008:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
5390946:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
17197480:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
6236639:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
4364312:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
4955196:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
11661929:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
8781683:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
23066352:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
7125909:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
15270897:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
38261582:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
970776:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
4191910:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
3754222:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
26345571:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
12645842:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
9426233:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 200000000
Condition exists (y=2 /\ 0:r1=2 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=7bfa463f7adb7b5e7778fa7badd28f31
Cycle=DpsR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw014 No BCSyncsRW
Safe=DpsR DpdR
Time bcssrw014 51.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw015
"SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | sync ;
lwzx r4,r3,r5 | lwz r3,0(r2) ;
sync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | sync ;
| li r7,1 ;
| stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw016
"LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe"
{0:r2=x; 0:r5=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
xor r3,r1,r1 | lwsync ;
lwzx r4,r3,r5 | lwz r3,0(r2) ;
sync | xor r4,r3,r3 ;
li r6,1 | lwzx r5,r4,r6 ;
stw r6,0(r5) | sync ;
| li r7,1 ;
| stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 30,0(11)
_litmus_P0_1_: xor 10,30,30
_litmus_P0_2_: lwzx 31,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Failure: malloc
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw017
"DpdW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 ;
lwz r3,0(r2) | stwx r4,r3,r5 ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 4,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,4,9
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw018
"SyncdRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw019
"DpdR SyncsRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | sync ;
xor r4,r3,r3 | li r6,1 ;
lwzx r5,r4,r6 | stw r6,0(r5) ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw020
"LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1)
Generated assembler
_litmus_P1_0_: lwz 4,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 5,1
_litmus_P1_3_: stw 5,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw021
"DpdR LwSyncsRW Wse SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | lwsync ;
xor r4,r3,r3 | li r6,1 ;
lwzx r5,r4,r6 | stw r6,0(r5) ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 10,30,30
_litmus_P1_2_: lwzx 31,10,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw022
"DpdR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw023
"SyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=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) ;
lwz r3,0(r2) | xor r4,r3,r3 ;
xor r4,r3,r3 | lwzx r5,r4,r6 ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 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 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw024
"LwSyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r2) ;
lwz r3,0(r2) | xor r4,r3,r3 ;
xor r4,r3,r3 | lwzx r5,r4,r6 ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: lwsync
_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 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw025
"SyncdRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw026
"DpdR SyncsRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | sync ;
xor r4,r3,r3 | lwz r6,0(r5) ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P1_3_: sync
_litmus_P1_4_: lwz 10,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw027
"LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r4=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) ;
lwz r3,0(r2) | ;
xor r4,r3,r3 | ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw028
"DpdR LwSyncsRR Fre SyncsWR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r5=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | lwsync ;
xor r4,r3,r3 | lwz r6,0(r5) ;
lwzx r5,r4,r6 | ;
sync | ;
li r7,1 | ;
stw r7,0(r6) | ;
exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0)
Generated assembler
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,9
_litmus_P1_3_: lwsync
_litmus_P1_4_: lwz 10,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 30,0(11)
_litmus_P0_4_: xor 8,30,30
_litmus_P0_5_: lwzx 31,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Failure: malloc
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw029
"SyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
sync | sync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
sync | sync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw030
"LwSyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
sync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
sync | sync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Failure: malloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw031
"LwSyncsRR DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
lwz r1,0(r2) | lwz r1,0(r2) ;
lwsync | lwsync ;
lwz r3,0(r2) | lwz r3,0(r2) ;
xor r4,r3,r3 | xor r4,r3,r3 ;
lwzx r5,r4,r6 | lwzx r5,r4,r6 ;
sync | sync ;
li r7,1 | li r7,1 ;
stw r7,0(r6) | stw r7,0(r6) ;
exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 30,0(11)
_litmus_P1_3_: xor 8,30,30
_litmus_P1_4_: lwzx 10,8,9
_litmus_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 30,0(11)
_litmus_P0_3_: xor 8,30,30
_litmus_P0_4_: lwzx 10,8,9
_litmus_P0_5_: sync
_litmus_P0_6_: li 7,1
_litmus_P0_7_: stw 7,0(9)
Failure: malloc
Failure: malloc
Failure: malloc
$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 (16 < N ? 1 : 16 / 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: 16 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=-s 1000000 -r 40
Mon Dec 28 13:40:18 GMT 2009