Wed Dec 30 17:34:00 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 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P3_3_: sync
_litmus_P3_4_: li 8,1
_litmus_P3_5_: stw 8,0(9)
_litmus_P2_0_: lwz 5,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,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 (97 states)
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
1 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
228585:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
203738:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
311233:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
890576:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
481118:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=2;
560732:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
149374:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
213038:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
229796:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
169310:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
188545:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
379548:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
1256127:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
670285:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
420846:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
2316191:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
777127:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
285932:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
364636:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
477241:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
2311461:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
623352:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
1835660:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
490711:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
1041921:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
755848:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
453252:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
340188:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
355545:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
272902:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
269764:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
3087899:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
1959036:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
417884:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
1398639:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
581269:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
397684:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
360738:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
6546756:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
14514846:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
3682635:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
219994:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
246736:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
231644:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
7163198:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
3292670:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
6612022:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
3058792:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
1126306:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
311202:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
6828375:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
7718662:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
597512:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3877646:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3085041:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
2150230:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
4738031:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
4264628:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
7346932:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
1304957:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
6767595:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
6708064:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
4103000:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
7296911:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
2727312:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
6982139:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
3928000:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
6887785:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
426775:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
3172795:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
5058169:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
10515042:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
15635834:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3075417:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
286839:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
243739:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
2403034:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
11848868:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
13371302:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
8687076:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
2530983:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
2005284:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
5065767:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
13100584:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
18302212:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
502895:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
7440696:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
486991:>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
3909598:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
605362:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
1459989:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
9038812:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1031798:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
13970486:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
3976299:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
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 114.67
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw001 Allowed
Histogram (18 states)
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
4598453:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9666842:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
35749072:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
18209177:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
12865664:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
3598753:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
7242384:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
36758101:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
13845613:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
43078196:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
22830716:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
66814853:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
9591764:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
19794465:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
3940024:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
36303659:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
55112263:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
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 64.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 25,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 26,0(11)
_litmus_P2_3_: xor 8,26,26
_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 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw002 Allowed
Histogram (33 states)
2 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
1 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
392896:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
416677:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
1613640:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
2410481:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
1769433:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1824340:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
12864829:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
1833358:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
5360121:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1738433:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
1103029:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1860758:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
2929103:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
12332597:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
14568800:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
3493041:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
4051843:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
46521609:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
5576482:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
2597618:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
40066711:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
17013242:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
30035414:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
30387841:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
9946028:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
9444545:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
56199259:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
32760058:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
14795282:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
34092528:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
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 73.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 25,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 26,0(11)
_litmus_P2_3_: xor 8,26,26
_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 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,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=0; 2:r3=2; 2:r5=0; y=1;
25830 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
54342 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
303573:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
601788:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1080905:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
2043282:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
2291054:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
749202:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1293809:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
800946:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
1158248:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
3875998:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
142593:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
7166418:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
4263630:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
14067911:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
3338347:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
4648957:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
18508642:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
27941667:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
15522823:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
40342992:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
3863034:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
10041512:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
11757937:>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
58430540:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
57483138:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
34115038:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
33431921:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
40653922:>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: 400000000
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 71.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 30,28,28
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,30,9
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw004 Allowed
Histogram (24 states)
7 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
2 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=2;
1124211:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
1630567:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
726200:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
659963:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
1593526:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
13357406:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
27898982:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
5033886:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
9507025:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
5911450:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
98798493:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
3273340:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
15774155:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
27584982:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
24777196:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
4137535:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
51450116:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
13908464:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
21277306:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
30330256:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
31858800:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
9386132:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
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 72.14
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw005 Allowed
Histogram (23 states)
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
572995:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
786743:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
878174:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
1555795:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
4981924:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
6366279:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
3830729:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
3019345:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
5986857:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
14276199:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
14178912:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
670619:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
23472139:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
24067869:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
24479414:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
55646551:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
16860409:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
99097445:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
25828783:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
34672315:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
12149790:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
26620713:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
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 72.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw006 Allowed
Histogram (23 states)
1 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=2; y=1;
698917:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
799966:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
1315693:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
1961574:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
17246653:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
3201687:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
1904232:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
25200436:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
4709946:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
24211805:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
6294769:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
12716522:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
4739904:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
5096318:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
15101235:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
26259185:>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
54637403:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
103503867:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
23715049:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
22526213:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
31706123:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
12452502:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
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 70.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 10,28,28
_litmus_P2_2_: lwzx 30,10,9
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw007 Allowed
Histogram (19 states)
18 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
15651283:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
25198664:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
6241090:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
50452748:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
10441562:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
3803684:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
25888575:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
9127559:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
18695313:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
32438406:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
6113028:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
31970705:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
4835756:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
22438665:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
101848897:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
13798913:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
21055131:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
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 67.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,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;
5283749:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
15877075:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
27253481:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
9972801:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
8319480:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
22195247:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
18337432:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
5884465:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
13111762:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
27583508:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
3149273:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
5981697:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
50465399:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
105263200:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
34255810:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
22559431:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
24506189:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
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 67.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: lwz 4,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 26,0(11)
_litmus_P0_4_: xor 8,26,26
_litmus_P0_5_: lwzx 27,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)
11 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=2;
16 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
24342681:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
17853494:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
5244142:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
5264134:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
16359309:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
27209886:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
5735692:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
9539504:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
7793987:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
27461461:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
3754360:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
24666602:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
13818304:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
106875971:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
33333618:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
21741478:>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
49005350:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
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 68.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 25,0(11)
_litmus_P0_1_: sync
_litmus_P0_2_: lwz 26,0(11)
_litmus_P0_3_: xor 8,26,26
_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)
40453569:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
6241832:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
7383244:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
4453361:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
24410628:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
3339513:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
64983835:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2186171:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
9041130:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
40652618:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
12967621:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
16693952:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
5720967:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
22189231:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
5296883:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
4319906:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1249274:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
14834670:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
56474502:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
39257014:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
4071437:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
13778642:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
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 67.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 27,0(11)
_litmus_P2_1_: xor 10,27,27
_litmus_P2_2_: lwzx 28,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 25,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 26,0(11)
_litmus_P0_3_: xor 8,26,26
_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)
765074:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
1416626:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
7652737:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
799790:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1985366:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4692994:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
42183862:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
13856364:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
6876944:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
39814027:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
19558022:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4322596:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
16348665:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
64123317:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
3908925:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
24437979:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
9027493:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
5522282:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
30479011:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
57839906:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1242835:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
43145185:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
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 68.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw012 Allowed
Histogram (3 states)
276526380:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0;
192114358:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0;
171359262:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=e494be0d2836eabb8ed392ae5713400a
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw012 No BCSyncsRW
Safe=DpdR
Time bcssrw012 75.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw013 Allowed
Histogram (7 states)
3283230:>0:r1=1; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
3428441:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=0;
4937372:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
106511578:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
84950437:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
96856836:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
100032106:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=873592e9aeb4eb41aabdf201c7c3fd2d
Cycle=DpdR SyncsRW Rfe DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw013 No BCSyncsRW
Safe=DpdR
Time bcssrw013 78.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_1_: xor 10,30,30
_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 27,0(11)
_litmus_P1_1_: xor 10,27,27
_litmus_P1_2_: lwzx 28,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 27,0(11)
_litmus_P0_1_: xor 10,27,27
_litmus_P0_2_: lwzx 28,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw014 Allowed
Histogram (22 states)
2 :>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
120777:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
1249697:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
338362:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
3723398:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
14101658:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
4396590:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
7743984:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
14432328:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
3828231:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
22590126:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
525977:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
9938583:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
35055370:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
38883741:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
57196474:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
39635939:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
68060263:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
9553313:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
33920424:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
19201009:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
15503754:>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: 400000000
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 68.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw015 Allowed
Histogram (4 states)
257038125:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
72463169:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
129437340:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
181061366:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=15f52564e04daa74ee8b809a62b31ce5
Cycle=SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw015 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw015 75.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw016 Allowed
Histogram (4 states)
24039184:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
172169899:>0:r1=1; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
192579278:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
251211639:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=da74259e4b84d84fe8b12e45af381e8e
Cycle=LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw016 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw016 74.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,3,3
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,30,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 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw017 Allowed
Histogram (4 states)
135644853:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
193681565:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
297176241:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
13497341:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=97b40d67b76129b3ab3e1a6a5f6305eb
Cycle=DpdW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw017 No BCSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bcssrw017 67.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,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 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw018 Allowed
Histogram (4 states)
13272388:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
85560875:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
275482456:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
265684281:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=059b61899a92329ffeaf348803309697
Cycle=SyncdRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw018 No BCSyncsRW
Safe=Wse SyncsWR SyncdRW DpdR
Time bcssrw018 65.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw019 Allowed
Histogram (6 states)
9574755:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
2496474:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
8380243:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
127844467:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
300959184:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
190744877:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=ef298b82541a3b112e43ae882acb50a5
Cycle=DpdR SyncsRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw019 No BCSyncsRW
Safe=Wse SyncsWR SyncsRW DpdR
Time bcssrw019 66.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 4,1
_litmus_P1_3_: stw 4,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 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw020 Allowed
Histogram (4 states)
7721190:>0:r3=1; 0:r5=0; 1:r1=0; x=1;
266028611:>0:r3=2; 0:r5=0; 1:r1=0; x=1;
80449518:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
285800681:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1) is NOT validated
Hash=7f2323c0dd7502796856c97da172b168
Cycle=LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw020 No BCSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bcssrw020 66.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,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 27,0(11)
_litmus_P0_4_: xor 8,27,27
_litmus_P0_5_: lwzx 28,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw021 Allowed
Histogram (6 states)
739079:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
3606417:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
4905857:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
193873363:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
313059089:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
123816195:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=3ac226fd1be7f310c6194b6c73f3c232
Cycle=DpdR LwSyncsRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw021 No BCSyncsRW
Safe=Wse SyncsWR LwSyncsRW DpdR
Time bcssrw021 66.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw022 Allowed
Histogram (3 states)
177908041:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1;
319985460:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0;
142106499:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0) is NOT validated
Hash=7ac3fafaae301cc73390972bbdd5c0f4
Cycle=DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw022 No BCSyncsRW
Safe=Fre SyncsWR DpdR
Time bcssrw022 73.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw023 Allowed
Histogram (4 states)
76008832:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
130913064:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
124812795:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
308265309:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=c2c9c0359658b64e4185d23d932ca70a
Cycle=SyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw023 No BCSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bcssrw023 74.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw024 Allowed
Histogram (4 states)
21330242:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
168267531:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
319243720:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
131158507:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=dcde740d5eace2726b3b99bfd0448c43
Cycle=LwSyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw024 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw024 74.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw025 Allowed
Histogram (3 states)
133389907:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
311633358:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
194976735:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=8047871ef7343012976d8a83d92f5d9f
Cycle=SyncdRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw025 No BCSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bcssrw025 71.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw026 Allowed
Histogram (4 states)
11688419:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
199423295:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
307546479:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
121341807:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=e601791e1656e598fa3a9bacd4c2c5b2
Cycle=DpdR SyncsRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw026 No BCSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bcssrw026 75.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw027 Allowed
Histogram (3 states)
192222895:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
319034022:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
128743083:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=0) is NOT validated
Hash=a9989a08ab5b3cfd8006a16e6ef9efd7
Cycle=LwSyncdRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw027 No BCSyncsRW
Safe=Fre SyncsWR LwSyncdRR DpdR
Time bcssrw027 76.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw028 Allowed
Histogram (4 states)
376864:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
123544709:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
318659006:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
197419421:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=f96ce8a4017924c7511ae42d30af7292
Cycle=DpdR LwSyncsRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw028 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw028 75.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw029 Allowed
Histogram (5 states)
79024735:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
116778119:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
114333654:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
85532412:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
244331080:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=69e45967a3fe794a66d57ca3e640a326
Cycle=SyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe
Relax bcssrw029 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw029 75.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw030 Allowed
Histogram (5 states)
18969561:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
75399727:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
168287063:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
128772135:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
248571514:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=ce33b1e1ca4525573eb6199b87f1a3d7
Cycle=LwSyncsRR DpdR SyncsRW Rfe SyncsRR DpdR SyncsRW Rfe
Relax bcssrw030 No BCSyncsRW
Safe=SyncsRR LwSyncsRR DpdR
Time bcssrw030 78.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
Test bcssrw031 Allowed
Histogram (5 states)
24495375:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
27703811:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
178886511:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
237830865:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
171083438:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (0:r1=1 /\ 0:r3=1 /\ 0:r5=0 /\ 1:r1=1 /\ 1:r3=1 /\ 1:r5=0) is NOT validated
Hash=ae803005916745f384198d670ee29f6c
Cycle=LwSyncsRR DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe
Relax bcssrw031 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw031 75.19
$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: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Wed Dec 30 18:12:55 GMT 2009