Wed Dec 30 15:09:54 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww000
"DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=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 ;
li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | ;
exists (x=2 /\ 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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww000 Allowed
Histogram (3 states)
82338747:>1:r1=0; x=1;
244559604:>1:r1=1; x=1;
313101649:>1:r1=0; x=2;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=262d40103ab036ada7c4d5ede4cb5840
Cycle=DpdW Wse SyncdWW Rfe
Relax bcsdww000 No BCSyncdWW
Safe=Wse DpdW
Time bcsdww000 64.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww001
"DpdW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 | sync | li r4,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: xor 30,3,3
_litmus_P3_2_: li 10,1
_litmus_P3_3_: stwx 10,30,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww001 Allowed
Histogram (15 states)
644424:>1:r1=1; 3:r1=1; x=1; z=2;
686051:>1:r1=1; 3:r1=1; x=2; z=1;
13595343:>1:r1=1; 3:r1=0; x=2; z=1;
16759694:>1:r1=0; 3:r1=1; x=1; z=2;
27846622:>1:r1=1; 3:r1=1; x=1; z=1;
3038864:>1:r1=0; 3:r1=0; x=1; z=1;
42618707:>1:r1=0; 3:r1=0; x=2; z=1;
44013990:>1:r1=0; 3:r1=0; x=1; z=2;
31814905:>1:r1=1; 3:r1=0; x=1; z=1;
35034326:>1:r1=0; 3:r1=1; x=1; z=1;
1197444:>1:r1=1; 3:r1=0; x=2; z=2;
16539864:>1:r1=0; 3:r1=1; x=2; z=1;
70346145:>1:r1=0; 3:r1=0; x=2; z=2;
14270894:>1:r1=1; 3:r1=0; x=1; z=2;
1592727:>1:r1=0; 3:r1=1; x=2; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=96b3ad5ef3552835e91cfb053b388e47
Cycle=DpdW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww001 No BCSyncdWW
Safe=Wse DpdW
Time bcsdww001 92.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww002
"SyncdRW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | li r4,1 | sync | li r3,1 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: li 4,1
_litmus_P3_3_: stw 4,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww002 Allowed
Histogram (15 states)
4481525:>1:r1=0; 3:r1=0; x=1; z=1;
369599:>1:r1=1; 3:r1=1; x=2; z=1;
836328:>1:r1=0; 3:r1=1; x=2; z=2;
741963:>1:r1=1; 3:r1=1; x=1; z=2;
995986:>1:r1=1; 3:r1=0; x=2; z=2;
13544962:>1:r1=1; 3:r1=0; x=2; z=1;
33645732:>1:r1=0; 3:r1=1; x=1; z=1;
49044028:>1:r1=0; 3:r1=0; x=1; z=2;
16176916:>1:r1=1; 3:r1=0; x=1; z=2;
38379703:>1:r1=1; 3:r1=0; x=1; z=1;
65695577:>1:r1=0; 3:r1=0; x=2; z=2;
11590921:>1:r1=0; 3:r1=1; x=2; z=1;
43210955:>1:r1=0; 3:r1=0; x=2; z=1;
26483851:>1:r1=1; 3:r1=1; x=1; z=1;
14801954:>1:r1=0; 3:r1=1; x=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=af33a9d4f6f79386d356cbbdb0662698
Cycle=SyncdRW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww002 No BCSyncdWW
Safe=Wse SyncdRW DpdW
Time bcsdww002 94.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww003
"DpdR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 | sync | lwzx r4,r3,r5 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 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_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww003 Allowed
Histogram (15 states)
2949712:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
673342:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
1838216:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
409481:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
807158:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
24723178:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
46579918:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
17279273:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
12591439:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
36203624:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
43265906:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
10256581:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
17766529:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
74420393:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
30235250:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=6c72af0e6695d87de072985a4977a496
Cycle=DpdR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww003 No BCSyncdWW
Safe=Fre Wse DpdW DpdR
Time bcsdww003 90.93
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww004
"DpsR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r4,1 | sync | lwzx r4,r3,r2 ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww004 Allowed
Histogram (42 states)
15 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
23516 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
3372 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
131796:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
4587 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
1843 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
4845 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
9007 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
31161 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
106645:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
50410 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
44514 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
74890 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
38447 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
24114 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
128599:>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
33817 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
17017 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
545812:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
73033 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
483046:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
1013505:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1633932:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
6648350:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
1838453:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
3231523:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
4259839:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
3684560:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
4642001:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
27361717:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
9778113:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
20319657:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
25967217:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
33377996:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
21495805:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
54391184:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
16149357:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
31705821:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
13644304:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
971622:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
11849534:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
24205024:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=26d413fc2e2cdadfa9e0f1aeb3ab365b
Cycle=DpsR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww004 No BCSyncdWW
Safe=Fre Wse DpsR DpdW
Time bcsdww004 97.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww005
"SyncdRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | li r4,1 | sync | lwz r3,0(r4) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww005 Allowed
Histogram (15 states)
3329805:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
735566:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
1304431:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
1012771:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
1189074:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
17101882:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
67957395:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
30643925:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
43909071:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
35348773:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
41914687:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
14674127:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
16920739:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
28593614:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
15364140:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=9d8e29c8c4e565bae4fdb78aec0db9b5
Cycle=SyncdRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww005 No BCSyncdWW
Safe=Fre Wse SyncdRR DpdW
Time bcsdww005 90.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww006
"SyncsRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | li r4,1 | sync | lwz r3,0(r2) ;
li r3,1 | stwx r4,r3,r5 | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww006 Allowed
Histogram (42 states)
1573 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
314955:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
240596:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
274512:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
346674:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
1209006:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
433009:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
253790:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
717441:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
219346:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
2578607:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
1095590:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
1749925:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
869852:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
4743393:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
1416864:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
893127:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
1587255:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
1183315:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
2736585:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
679586:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
414542:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
5181606:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
1402160:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
3529105:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
1314615:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
10111838:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
5997342:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
3631639:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
22578370:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
2416276:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
18246668:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
7545065:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
50678002:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
26356178:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
11376790:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
27575173:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
20032921:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
12620820:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
15485169:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
19789813:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
30170907:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=62faf55c9e7916888e6ae088e9375bff
Cycle=SyncsRR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe
Relax bcsdww006 No BCSyncdWW
Safe=Fre Wse SyncsRR DpdW
Time bcsdww006 95.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww007
"DpdW Wse SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | li r4,1 ;
li r3,1 | li r3,1 | stwx r4,r3,r5 ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
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_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww007 Allowed
Histogram (7 states)
34918747:>2:r1=0; x=2; y=2;
10266173:>2:r1=0; x=1; y=1;
13359258:>2:r1=1; x=1; y=2;
90730712:>2:r1=1; x=1; y=1;
124111771:>2:r1=0; x=2; y=1;
20904932:>2:r1=1; x=2; y=1;
105708407:>2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=7c2462ff041c713f8de949f757a40d53
Cycle=DpdW Wse SyncdWW Wse SyncdWW Rfe
Relax bcsdww007 No BCSyncdWW
Safe=Wse SyncdWW DpdW
Time bcsdww007 63.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww008
"SyncdRW Wse SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | li r3,1 ;
li r3,1 | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1)
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_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww008 Allowed
Histogram (7 states)
11276185:>2:r1=1; x=1; y=2;
26671573:>2:r1=0; x=2; y=2;
88376295:>2:r1=1; x=1; y=1;
16792783:>2:r1=0; x=1; y=1;
116897121:>2:r1=0; x=1; y=2;
13600746:>2:r1=1; x=2; y=1;
126385297:>2:r1=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated
Hash=e6b1c1a0023ee13d1ea18feb286c6d13
Cycle=SyncdRW Wse SyncdWW Wse SyncdWW Rfe
Relax bcsdww008 No BCSyncdWW
Safe=Wse SyncdWW SyncdRW
Time bcsdww008 65.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww009
"DpdR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 2:r1=1 /\ 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_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww009 Allowed
Histogram (7 states)
8573092:>2:r1=1; 2:r4=1; y=2;
36358383:>2:r1=0; 2:r4=0; y=2;
12378032:>2:r1=0; 2:r4=1; y=1;
79841740:>2:r1=1; 2:r4=1; y=1;
106290762:>2:r1=0; 2:r4=1; y=2;
143140869:>2:r1=0; 2:r4=0; y=1;
13417122:>2:r1=1; 2:r4=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=9d7f07ce6da224ac7eca2af4a5915a72
Cycle=DpdR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww009 No BCSyncdWW
Safe=Fre Wse SyncdWW DpdR
Time bcsdww009 62.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww010
"DpsR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r2 ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 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_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww010 Allowed
Histogram (18 states)
622 :>2:r1=0; 2:r4=1; x=2; y=1;
4600 :>2:r1=2; 2:r4=1; x=1; y=1;
7337 :>2:r1=1; 2:r4=2; x=1; y=2;
23588 :>2:r1=0; 2:r4=2; x=2; y=1;
127356:>2:r1=2; 2:r4=1; x=2; y=1;
63043 :>2:r1=0; 2:r4=2; x=1; y=1;
79024 :>2:r1=0; 2:r4=1; x=1; y=1;
237533:>2:r1=0; 2:r4=2; x=1; y=2;
893028:>2:r1=0; 2:r4=1; x=1; y=2;
13658885:>2:r1=1; 2:r4=1; x=2; y=1;
56233944:>2:r1=0; 2:r4=0; x=1; y=1;
41596726:>2:r1=1; 2:r4=1; x=1; y=2;
5480493:>2:r1=2; 2:r4=2; x=1; y=1;
36826503:>2:r1=0; 2:r4=0; x=2; y=1;
46106763:>2:r1=2; 2:r4=2; x=1; y=2;
29037324:>2:r1=1; 2:r4=1; x=1; y=1;
99292764:>2:r1=2; 2:r4=2; x=2; y=1;
70330467:>2:r1=0; 2:r4=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=3bd35505ff4c5dbff1bb92ff33d7496b
Cycle=DpsR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww010 No BCSyncdWW
Safe=Fre Wse SyncdWW DpsR
Time bcsdww010 66.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww011
"SyncdRR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (y=2 /\ 2:r1=1 /\ 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_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww011 Allowed
Histogram (7 states)
8739070:>2:r1=1; 2:r3=1; y=2;
13521266:>2:r1=0; 2:r3=1; y=1;
34514287:>2:r1=0; 2:r3=0; y=2;
12199221:>2:r1=1; 2:r3=0; y=1;
139533554:>2:r1=0; 2:r3=0; y=1;
109576629:>2:r1=0; 2:r3=1; y=2;
81915973:>2:r1=1; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=d6dadb697329282571a4979eadd035fd
Cycle=SyncdRR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww011 No BCSyncdWW
Safe=Fre Wse SyncdWW SyncdRR
Time bcsdww011 62.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww012
"SyncsRR Fre SyncdWW Wse SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r2) ;
li r3,1 | li r3,1 | ;
stw r3,0(r4) | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test bcsdww012 Allowed
Histogram (18 states)
25022 :>2:r1=0; 2:r3=1; x=2; y=1;
614427:>2:r1=2; 2:r3=1; x=1; y=1;
2182559:>2:r1=0; 2:r3=2; x=2; y=1;
4793474:>2:r1=2; 2:r3=1; x=2; y=1;
490983:>2:r1=0; 2:r3=2; x=1; y=1;
11852006:>2:r1=0; 2:r3=1; x=1; y=2;
4324047:>2:r1=0; 2:r3=2; x=1; y=2;
2483138:>2:r1=1; 2:r3=2; x=1; y=2;
34552457:>2:r1=0; 2:r3=0; x=2; y=1;
650017:>2:r1=0; 2:r3=1; x=1; y=1;
13508090:>2:r1=1; 2:r3=1; x=2; y=1;
29490512:>2:r1=1; 2:r3=1; x=1; y=2;
5116540:>2:r1=2; 2:r3=2; x=1; y=1;
66197637:>2:r1=0; 2:r3=0; x=1; y=2;
28761816:>2:r1=1; 2:r3=1; x=1; y=1;
94077046:>2:r1=2; 2:r3=2; x=2; y=1;
56961429:>2:r1=0; 2:r3=0; x=1; y=1;
43918800:>2:r1=2; 2:r3=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=3491c251ad1f32fc2b43d52f52c46191
Cycle=SyncsRR Fre SyncdWW Wse SyncdWW Rfe
Relax bcsdww012 No BCSyncdWW
Safe=Fre Wse SyncsRR SyncdWW
Time bcsdww012 66.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww013
"SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=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 ;
li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | ;
exists (x=2 /\ 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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww013 Allowed
Histogram (3 states)
138837838:>1:r1=0; x=1;
294580435:>1:r1=0; x=2;
206581727:>1:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (x=2 /\ 1:r1=1) is NOT validated
Hash=3bacaa46622528b0ef100acb0d326a4f
Cycle=SyncdRW Wse SyncdWW Rfe
Relax bcsdww013 No BCSyncdWW
Safe=Wse SyncdRW
Time bcsdww013 61.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww014
"SyncdRW Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | li r3,1 | sync | li r3,1 ;
li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: li 4,1
_litmus_P3_3_: stw 4,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww014 Allowed
Histogram (15 states)
357817:>1:r1=1; 3:r1=1; x=2; z=1;
572889:>1:r1=1; 3:r1=0; x=2; z=2;
541451:>1:r1=0; 3:r1=1; x=2; z=2;
11407913:>1:r1=0; 3:r1=1; x=2; z=1;
8077237:>1:r1=0; 3:r1=0; x=1; z=1;
50894353:>1:r1=0; 3:r1=0; x=2; z=1;
11510577:>1:r1=1; 3:r1=0; x=1; z=2;
384468:>1:r1=1; 3:r1=1; x=1; z=2;
39526713:>1:r1=0; 3:r1=1; x=1; z=1;
60539674:>1:r1=0; 3:r1=0; x=2; z=2;
11560405:>1:r1=0; 3:r1=1; x=1; z=2;
23088290:>1:r1=1; 3:r1=1; x=1; z=1;
39714183:>1:r1=1; 3:r1=0; x=1; z=1;
12095791:>1:r1=1; 3:r1=0; x=2; z=1;
49728239:>1:r1=0; 3:r1=0; x=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated
Hash=ee6d6ba63625d467fac397c863618ff2
Cycle=SyncdRW Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww014 No BCSyncdWW
Safe=Wse SyncdRW
Time bcsdww014 91.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww015
"DpdR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r3,1 | sync | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 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_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww015 Allowed
Histogram (15 states)
671556:>1:r1=1; 3:r1=0; 3:r4=0; z=2;
1253166:>1:r1=0; 3:r1=1; 3:r4=0; z=2;
851862:>1:r1=1; 3:r1=1; 3:r4=0; z=1;
333282:>1:r1=1; 3:r1=1; 3:r4=1; z=2;
4827061:>1:r1=0; 3:r1=0; 3:r4=1; z=1;
14216518:>1:r1=0; 3:r1=1; 3:r4=1; z=2;
9560193:>1:r1=1; 3:r1=0; 3:r4=1; z=2;
18770828:>1:r1=0; 3:r1=1; 3:r4=0; z=1;
40071523:>1:r1=0; 3:r1=1; 3:r4=1; z=1;
43652074:>1:r1=0; 3:r1=0; 3:r4=1; z=2;
49485047:>1:r1=0; 3:r1=0; 3:r4=0; z=1;
25090484:>1:r1=1; 3:r1=1; 3:r4=1; z=1;
31913022:>1:r1=1; 3:r1=0; 3:r4=1; z=1;
66011738:>1:r1=0; 3:r1=0; 3:r4=0; z=2;
13291646:>1:r1=1; 3:r1=0; 3:r4=0; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=17704085d61983610ea6761b47264366
Cycle=DpdR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww015 No BCSyncdWW
Safe=Fre Wse SyncdRW DpdR
Time bcsdww015 89.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww016
"DpsR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ;
sync | li r3,1 | sync | lwzx r4,r3,r2 ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww016 Allowed
Histogram (42 states)
17 :>1:r1=1; 3:r1=0; 3:r4=1; y=2; z=1;
2173 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2;
15103 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1;
11141 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1;
115401:>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1;
19806 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1;
4027 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1;
11728 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2;
2641 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2;
21538 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2;
163583:>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1;
32106 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2;
53355 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1;
63883 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1;
474657:>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1;
94913 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2;
26235 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1;
42566 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1;
43021 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=2;
94117 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=2;
8297755:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1;
537866:>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2;
388496:>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1;
28004464:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1;
3348082:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2;
2789958:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2;
898821:>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1;
17930881:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2;
5056125:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2;
13904511:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1;
18912646:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1;
35653866:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2;
53763848:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1;
2696056:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2;
11190624:>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1;
26957062:>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2;
35519837:>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1;
26945870:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2;
11478445:>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1;
10260237:>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1;
2583350:>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1;
1589189:>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=afd72f686b99433de47ab6d5cad91134
Cycle=DpsR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww016 No BCSyncdWW
Safe=Fre Wse SyncdRW DpsR
Time bcsdww016 95.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww017
"SyncdRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | li r3,1 | sync | lwz r3,0(r4) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww017 Allowed
Histogram (15 states)
7082552:>1:r1=0; 3:r1=0; 3:r3=1; z=1;
580706:>1:r1=1; 3:r1=0; 3:r3=0; z=2;
23126819:>1:r1=1; 3:r1=1; 3:r3=1; z=1;
605327:>1:r1=1; 3:r1=1; 3:r3=0; z=1;
13174457:>1:r1=1; 3:r1=0; 3:r3=0; z=1;
12582489:>1:r1=0; 3:r1=1; 3:r3=1; z=2;
14496631:>1:r1=0; 3:r1=1; 3:r3=0; z=1;
46046843:>1:r1=0; 3:r1=0; 3:r3=1; z=2;
408647:>1:r1=1; 3:r1=1; 3:r3=1; z=2;
36120157:>1:r1=1; 3:r1=0; 3:r3=1; z=1;
51912302:>1:r1=0; 3:r1=0; 3:r3=0; z=1;
37964716:>1:r1=0; 3:r1=1; 3:r3=1; z=1;
10701434:>1:r1=1; 3:r1=0; 3:r3=1; z=2;
64401693:>1:r1=0; 3:r1=0; 3:r3=0; z=2;
795227:>1:r1=0; 3:r1=1; 3:r3=0; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c13f8ec23ce3b9ee95f51b18bda82021
Cycle=SyncdRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww017 No BCSyncdWW
Safe=Fre Wse SyncdRW SyncdRR
Time bcsdww017 89.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww018
"SyncsRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | li r3,1 | sync | lwz r3,0(r2) ;
li r3,1 | stw r3,0(r4) | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_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 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww018 Allowed
Histogram (42 states)
967 :>1:r1=1; 3:r1=0; 3:r3=1; y=2; z=1;
307849:>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1;
154132:>1:r1=0; 3:r1=1; 3:r3=2; y=2; z=2;
150076:>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1;
327798:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1;
194700:>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2;
480716:>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1;
1156004:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1;
300732:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1;
1446481:>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1;
486500:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1;
1713838:>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2;
539150:>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2;
1444764:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1;
719367:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2;
2598891:>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2;
557692:>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2;
3358184:>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1;
370244:>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1;
7693641:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1;
1108961:>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2;
24581707:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2;
5386847:>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1;
2691604:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2;
2307046:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2;
1111939:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2;
10562416:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1;
1828579:>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2;
10512593:>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1;
16629247:>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1;
4016861:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2;
2298004:>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1;
635441:>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1;
13086708:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1;
26746230:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1;
21429507:>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2;
31611008:>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1;
32685306:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2;
50800102:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1;
10456941:>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1;
17867967:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2;
7643260:>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=df82d53ff13c1c0132bc81937f5ecf56
Cycle=SyncsRR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe
Relax bcsdww018 No BCSyncdWW
Safe=Fre Wse SyncsRR SyncdRW
Time bcsdww018 96.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww019
"DpdR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=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 ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (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 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww019 Allowed
Histogram (3 states)
205039039:>1:r1=1; 1:r4=1;
319936024:>1:r1=0; 1:r4=0;
115024937:>1:r1=0; 1:r4=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r4=0) is NOT validated
Hash=abe769d43585052eb6bd1199546b3603
Cycle=DpdR Fre SyncdWW Rfe
Relax bcsdww019 No BCSyncdWW
Safe=Fre DpdR
Time bcsdww019 77.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww020
"DpdR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r5 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 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_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww020 Allowed
Histogram (15 states)
1801560:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1;
1014144:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1;
1508613:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0;
1064643:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0;
16858743:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1;
28549503:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1;
32061053:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1;
41147512:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0;
71465988:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0;
15874833:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1;
42566945:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1;
17214881:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0;
15864420:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0;
31343514:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1;
1663648:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated
Hash=ff6729203383abc4a32d53a80bd77acb
Cycle=DpdR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww020 No BCSyncdWW
Safe=Fre DpdR
Time bcsdww020 91.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww021
"DpsR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww021 Allowed
Histogram (42 states)
34 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
4711 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
4873 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
3357 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; z=2;
9661 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
175693:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
37708 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=2;
2908 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; z=2;
30311 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
25370 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1;
62149 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
62284 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1;
670939:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2;
51484 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
149197:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=2;
100858:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2;
77106 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
46957 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1;
131746:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1;
1907188:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
38438 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1;
636039:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1;
3301034:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
1638794:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
1119853:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
4658962:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
13608005:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
3335385:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2;
9896585:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1;
4216154:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2;
6464860:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
12618225:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1;
33447741:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2;
23689911:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2;
20532982:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2;
20335532:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1;
16883148:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
909944:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
24155641:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2;
55203544:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1;
32755111:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1;
26999578:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=26085f29b1357e5e8f0e159288ddd725
Cycle=DpsR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww021 No BCSyncdWW
Safe=Fre DpsR DpdR
Time bcsdww021 97.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww022
"SyncdRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww022 Allowed
Histogram (15 states)
1482827:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0;
687755:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0;
16416313:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0;
1019788:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1;
25834116:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1;
3717445:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1;
36068204:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1;
43508954:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0;
17734398:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1;
30564332:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1;
14585721:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1;
13096615:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0;
44555087:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1;
69549192:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0;
1179253:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=52b75bc6c8456215cdaad6fb3a5164ee
Cycle=SyncdRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww022 No BCSyncdWW
Safe=Fre SyncdRR DpdR
Time bcsdww022 93.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww023
"SyncsRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,10,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww023 Allowed
Histogram (42 states)
1851 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
174934:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
238183:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
527791:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
862855:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
1388244:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1496394:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
412671:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
951880:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
306535:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
1749709:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
883429:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
256781:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
2159488:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
1377838:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
1093063:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
3197056:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
443263:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
1549615:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
888693:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
3529333:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
8148159:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
2693926:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
20199206:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
5955013:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
16748598:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
377414:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
28651171:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
12624982:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
1443436:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
29994297:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
2745428:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
723682:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
4548910:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
18279870:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
21261225:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
9654425:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
26077786:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
5166087:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
51976094:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
11870380:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
17370305:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=ef69b708c957de42a04a8b5ca4d81078
Cycle=SyncsRR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe
Relax bcsdww023 No BCSyncdWW
Safe=Fre SyncsRR DpdR
Time bcsdww023 97.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww024
"DpsR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r2 | sync | lwzx r4,r3,r2 ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1)
Generated assembler
_litmus_P3_0_: lwz 3,0(9)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 11,10,9
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww024 Allowed
Histogram (103 states)
1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
18 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
6 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
34 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
31 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
55 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
41 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
100 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
53 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
98 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
10 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
161 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
93 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
88 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
68 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
50 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=1;
265 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
47 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
202 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
72 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
3 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
824 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
81 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
847 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
6656 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
20 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
4118 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
12865 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
75885 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
5167 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
8147 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2;
61829 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
6610 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=1; y=2;
5021 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=1; y=2;
8557 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1;
8482 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1;
4119 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1;
71797 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=1;
12811 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1;
61698 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=1; y=1;
8251 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
51276 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=1;
60929 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
76836 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2;
52193 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
264 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=1;
15755 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1;
68758 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=2;
67735 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
59181 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=1;
8617 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
94 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=1;
8459 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
36461 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
15773 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
13416 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
92888 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1;
181448:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1;
45399 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1;
26109 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
36045 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1;
45655 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
126643:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2;
77123 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
36654 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=2;
94289 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
180748:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
26141 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2;
13732 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1;
337246:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1;
458066:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
37236 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
124215:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
340798:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
1778866:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2;
4074541:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1;
458203:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2;
1773872:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1;
743001:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1;
4623017:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2;
3137765:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1;
2630620:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1;
21647082:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2;
4089121:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2;
6490587:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1;
3145345:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1;
7745372:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1;
2637026:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2;
21653503:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1;
7559657:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1;
9270611:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1;
27567263:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1;
22366084:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2;
27514597:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2;
36644133:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1;
24538542:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1;
7564543:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1;
24489441:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2;
9287444:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1;
22280198:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1;
4605326:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1;
6502775:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated
Hash=6e01edb2061b004b7156eefd80367964
Cycle=DpsR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe
Relax bcsdww024 No BCSyncdWW
Safe=Fre DpsR
Time bcsdww024 118.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww025
"SyncdRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r2 | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 30,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww025 Allowed
Histogram (42 states)
22 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
3713 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
13012 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
3433 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
23959 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
203149:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
5441 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
23687 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
23472 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
73080 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
54514 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
41748 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
108047:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
13252 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
51873 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
146039:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
39994 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
26938 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
123565:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
542730:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
505585:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
1555580:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2;
3962123:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2;
3250717:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2;
5062406:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2;
2578777:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2;
655301:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1;
2196600:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1;
7095357:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1;
12550073:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1;
36499964:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1;
33290099:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2;
1293645:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1;
19257426:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2;
12697344:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1;
26490243:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1;
12474875:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1;
25869736:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2;
18656086:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1;
25798441:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2;
55191356:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1;
11546598:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=f58b58e77c065c1d7e45eddd6a49ef4b
Cycle=SyncdRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe
Relax bcsdww025 No BCSyncdWW
Safe=Fre SyncdRR DpsR
Time bcsdww025 93.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww026
"SyncsRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r2 | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(9)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 11,10,9
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww026 Allowed
Histogram (108 states)
14 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
5 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
7 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
66 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
20 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
111 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
444 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
603 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
16 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
492 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
1024 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
338 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
591 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
270 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
4564 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
5790 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
505 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
971 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
175 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
873 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
2223 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
5621 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
1954 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
3154 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
4764 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
11519 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
15843 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
3634 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
4635 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
2762 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
46061 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
7977 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
83373 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
64 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=1;
12514 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
2082 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
18348 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
8330 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
1223 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
17342 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
9880 :>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
26944 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
13005 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
804065:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1;
293015:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2;
53919 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
34622 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
42074 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
80947 :>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
87758 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1;
196950:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
55883 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
135339:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1;
308168:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1;
32776 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1;
32014 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
817094:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1;
10054 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1;
125449:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
1438843:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1;
653433:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1;
682716:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1;
840676:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2;
2277937:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1;
104126:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
83160 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
1276173:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2;
2840750:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2;
1462570:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2;
4024277:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1;
631678:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1;
2211714:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1;
487839:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1;
1620334:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1;
546815:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2;
193574:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2;
441862:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
3712883:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2;
1515567:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1;
527170:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1;
8607697:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1;
3642649:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1;
340796:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
796138:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1;
831617:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1;
3062631:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1;
3320914:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1;
1118499:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2;
2184431:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2;
24021511:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1;
8896158:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1;
5289093:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1;
2185358:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2;
6522170:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2;
743471:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2;
21764334:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1;
19956037:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1;
6520272:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1;
7683964:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1;
4909109:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2;
3439874:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1;
25217858:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2;
20815998:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2;
7087114:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1;
20904914:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2;
18931891:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2;
24437231:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1;
35763916:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=494bdd377023c801c91266ccd04985a6
Cycle=SyncsRR Fre SyncdWW Rfe DpsR Fre SyncdWW Rfe
Relax bcsdww026 No BCSyncdWW
Safe=Fre SyncsRR DpsR
Time bcsdww026 118.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww027
"DpdW Wse SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | li r4,1 ;
lwz r3,0(r4) | li r3,1 | stwx r4,r3,r5 ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=1)
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_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww027 Allowed
Histogram (7 states)
7616131:>0:r3=1; 2:r1=0; x=1;
19925183:>0:r3=1; 2:r1=1; x=2;
52870175:>0:r3=0; 2:r1=0; x=2;
18999965:>0:r3=0; 2:r1=1; x=1;
112469684:>0:r3=0; 2:r1=0; x=1;
107400764:>0:r3=1; 2:r1=0; x=2;
80718098:>0:r3=1; 2:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated
Hash=a3cc59f896bd23424085486bc047f237
Cycle=DpdW Wse SyncdWR Fre SyncdWW Rfe
Relax bcsdww027 No BCSyncdWW
Safe=Fre Wse SyncdWR DpdW
Time bcsdww027 60.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww028
"SyncdRW Wse SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | li r3,1 ;
lwz r3,0(r4) | li r3,1 | stw r3,0(r4) ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=1)
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_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww028 Allowed
Histogram (7 states)
12358604:>0:r3=1; 2:r1=0; x=1;
41185888:>0:r3=0; 2:r1=0; x=2;
12961913:>0:r3=1; 2:r1=1; x=2;
126599880:>0:r3=0; 2:r1=0; x=1;
112267282:>0:r3=1; 2:r1=0; x=2;
78507632:>0:r3=1; 2:r1=1; x=1;
16118801:>0:r3=0; 2:r1=1; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated
Hash=e4e07528cdbf9272fd50b0cf6708ccaa
Cycle=SyncdRW Wse SyncdWR Fre SyncdWW Rfe
Relax bcsdww028 No BCSyncdWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcsdww028 62.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww029
"DpdR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (0:r3=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_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww029 Allowed
Histogram (7 states)
22930395:>0:r3=0; 2:r1=1; 2:r4=1;
3828288:>0:r3=1; 2:r1=0; 2:r4=1;
24703588:>0:r3=1; 2:r1=1; 2:r4=0;
106360597:>0:r3=1; 2:r1=0; 2:r4=0;
78841510:>0:r3=1; 2:r1=1; 2:r4=1;
108465309:>0:r3=0; 2:r1=0; 2:r4=1;
54870313:>0:r3=0; 2:r1=0; 2:r4=0;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=1052dfbfb336d023eeffaaf6c00324c1
Cycle=DpdR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww029 No BCSyncdWW
Safe=Fre SyncdWR DpdR
Time bcsdww029 73.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww030
"DpsR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r2 ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=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_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww030 Allowed
Histogram (18 states)
3371 :>0:r3=1; 2:r1=2; 2:r4=1; y=1;
1411 :>0:r3=0; 2:r1=0; 2:r4=1; y=1;
5690 :>0:r3=1; 2:r1=1; 2:r4=2; y=2;
21293 :>0:r3=0; 2:r1=0; 2:r4=2; y=1;
219962:>0:r3=1; 2:r1=0; 2:r4=1; y=1;
141198:>0:r3=1; 2:r1=0; 2:r4=2; y=1;
1558291:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
3747144:>0:r3=1; 2:r1=2; 2:r4=2; y=1;
53494311:>0:r3=0; 2:r1=0; 2:r4=0; y=1;
329764:>0:r3=0; 2:r1=2; 2:r4=1; y=1;
25527648:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
86295433:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
815934:>0:r3=1; 2:r1=0; 2:r4=2; y=2;
15741430:>0:r3=1; 2:r1=1; 2:r4=1; y=1;
102932873:>0:r3=0; 2:r1=2; 2:r4=2; y=1;
41411124:>0:r3=1; 2:r1=2; 2:r4=2; y=2;
43058042:>0:r3=1; 2:r1=0; 2:r4=0; y=1;
24695081:>0:r3=0; 2:r1=1; 2:r4=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r4=1) is NOT validated
Hash=762db7307d35c050ae02494154891df7
Cycle=DpsR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww030 No BCSyncdWW
Safe=Fre SyncdWR DpsR
Time bcsdww030 62.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww031
"SyncdRR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (0:r3=0 /\ 2:r1=1 /\ 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_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww031 Allowed
Histogram (7 states)
16711745:>0:r3=0; 2:r1=1; 2:r3=1;
15653252:>0:r3=1; 2:r1=1; 2:r3=0;
6932585:>0:r3=1; 2:r1=0; 2:r3=1;
52817084:>0:r3=0; 2:r1=0; 2:r3=0;
115552456:>0:r3=1; 2:r1=0; 2:r3=0;
75951767:>0:r3=1; 2:r1=1; 2:r3=1;
116381111:>0:r3=0; 2:r1=0; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=d99b2c9fcd24d521255a6c4ef185df57
Cycle=SyncdRR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww031 No BCSyncdWW
Safe=Fre SyncdWR SyncdRR
Time bcsdww031 76.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww032.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww032
"SyncsRR Fre SyncdWR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r2) ;
lwz r3,0(r4) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: lwz 3,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 11,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcsdww032 Allowed
Histogram (18 states)
302586:>0:r3=1; 2:r1=2; 2:r3=1; y=1;
49490 :>0:r3=0; 2:r1=0; 2:r3=1; y=1;
636273:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
452378:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
2223801:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
4710197:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
2131129:>0:r3=0; 2:r1=0; 2:r3=2; y=1;
5079027:>0:r3=0; 2:r1=2; 2:r3=1; y=1;
3643321:>0:r3=1; 2:r1=2; 2:r3=2; y=1;
14127936:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
13894035:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
20902133:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
104069489:>0:r3=0; 2:r1=2; 2:r3=2; y=1;
54637614:>0:r3=0; 2:r1=0; 2:r3=0; y=1;
75188158:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
37105529:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
20837038:>0:r3=0; 2:r1=1; 2:r3=1; y=1;
40009866:>0:r3=1; 2:r1=2; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=6ef8013c1a65c6c1574ee921baad8f97
Cycle=SyncsRR Fre SyncdWR Fre SyncdWW Rfe
Relax bcsdww032 No BCSyncdWW
Safe=Fre SyncsRR SyncdWR
Time bcsdww032 67.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww033.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww033
"SyncdRR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=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) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (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 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test bcsdww033 Allowed
Histogram (3 states)
200569859:>1:r1=1; 1:r3=1;
129574098:>1:r1=0; 1:r3=1;
309856043:>1:r1=0; 1:r3=0;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=6fa2fc8a03a8948f9262ae5fd1e47a19
Cycle=SyncdRR Fre SyncdWW Rfe
Relax bcsdww033 No BCSyncdWW
Safe=Fre SyncdRR
Time bcsdww033 75.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww034.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww034
"SyncdRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 31,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww034 Allowed
Histogram (15 states)
5764906:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
596984:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
629659:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
843664:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
48028636:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
13498392:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
22833065:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
34628868:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
47574294:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
13818860:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
13539979:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
13341049:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
69006661:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
35100371:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
794612:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=3dd9d4fff43138f32cd2819c7a65cdb3
Cycle=SyncdRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe
Relax bcsdww034 No BCSyncdWW
Safe=Fre SyncdRR
Time bcsdww034 92.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww035.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww035
"SyncsRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 30,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww035 Allowed
Histogram (42 states)
1208 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
470786:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
381523:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
249813:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
189559:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
352110:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
491486:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1;
381714:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
1446187:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1;
2761151:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
607966:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
722115:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1782391:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
280839:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; z=1;
546057:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
1868261:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1391764:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1;
2313558:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
8442966:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
12024615:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
1912258:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
6726551:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
924312:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
950139:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
31117219:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
3033025:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2;
1409654:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
3330390:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1;
914522:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
2189305:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
6056548:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1;
32272181:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
22869983:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
10671686:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1;
25682407:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1;
3848890:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2;
15614868:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1;
19148213:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
52398243:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1;
12409322:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1;
11271373:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1;
18542842:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=f0c1b6d32c1c64645b39ad490ac97524
Cycle=SyncsRR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe
Relax bcsdww035 No BCSyncdWW
Safe=Fre SyncsRR SyncdRR
Time bcsdww035 96.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww036.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww036
"DpdR Fre SyncsWR Fre SyncdWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 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_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test bcsdww036 Allowed
Histogram (13 states)
1161051:>0:r3=2; 2:r1=0; 2:r4=2; x=2;
189633:>0:r3=2; 2:r1=0; 2:r4=1; x=2;
2037625:>0:r3=2; 2:r1=1; 2:r4=2; x=2;
7264699:>0:r3=2; 2:r1=0; 2:r4=0; x=2;
62039033:>0:r3=1; 2:r1=0; 2:r4=1; x=2;
64977539:>0:r3=1; 2:r1=0; 2:r4=0; x=1;
5743615:>0:r3=1; 2:r1=0; 2:r4=1; x=1;
48101588:>0:r3=1; 2:r1=0; 2:r4=2; x=2;
74918590:>0:r3=1; 2:r1=1; 2:r4=1; x=1;
30674611:>0:r3=1; 2:r1=0; 2:r4=2; x=1;
22827813:>0:r3=1; 2:r1=1; 2:r4=2; x=1;
58810186:>0:r3=1; 2:r1=0; 2:r4=0; x=2;
21254017:>0:r3=1; 2:r1=1; 2:r4=2; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated
Hash=b5668ea36c70858ef8634a895265c398
Cycle=DpdR Fre SyncsWR Fre SyncdWW Rfe
Relax bcsdww036 No BCSyncdWW
Safe=Fre SyncsWR DpdR
Time bcsdww036 60.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww037.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww037
"SyncdRR Fre SyncsWR Fre SyncdWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 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_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test bcsdww037 Allowed
Histogram (13 states)
1730672:>0:r3=2; 2:r1=1; 2:r3=2; x=2;
746120:>0:r3=2; 2:r1=0; 2:r3=2; x=2;
110103:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
7408644:>0:r3=1; 2:r1=0; 2:r3=1; x=1;
17829389:>0:r3=1; 2:r1=1; 2:r3=2; x=2;
16441926:>0:r3=1; 2:r1=1; 2:r3=2; x=1;
6203722:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
51326239:>0:r3=1; 2:r1=0; 2:r3=2; x=2;
71231638:>0:r3=1; 2:r1=1; 2:r3=1; x=1;
58415687:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
64127125:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
40341829:>0:r3=1; 2:r1=0; 2:r3=2; x=1;
64086906:>0:r3=1; 2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=c99d291fc8d3f66519c556e43131cb0b
Cycle=SyncdRR Fre SyncsWR Fre SyncdWW Rfe
Relax bcsdww037 No BCSyncdWW
Safe=Fre SyncsWR SyncdRR
Time bcsdww037 60.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcsdww038.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcsdww038
"SyncsRR Fre SyncdWW Rfe SyncsRR Fre SyncdWW Rfe"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r2) | sync | lwz r3,0(r2) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 4,0(9)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 11,0(9)
_litmus_P2_0_: li 5,2
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 4,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 11,0(9)
_litmus_P0_0_: li 5,2
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test bcsdww038 Allowed
Histogram (108 states)
334 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1071 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1024 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1551 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
10798 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
23554 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
7264 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1981 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
301 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
23841 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
3959 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
24232 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
11492 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
708089:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
86640 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
10134 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
67289 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
1663 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
30778 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
17164 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
227254:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
30959 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
84107 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
11912 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
73224 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
706652:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
720118:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
229547:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
120425:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
73979 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
7245 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
150222:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
86136 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
216398:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
24360 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
17447 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
608002:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
137165:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
67408 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
302803:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
148832:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
553809:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
214855:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
133904:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
85494 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
121898:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1;
480086:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
502135:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
741690:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
449717:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
596117:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
484525:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
301017:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
442861:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
743591:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
682881:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1430013:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
1440675:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
559802:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
417554:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
488098:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
422444:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1243069:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
821415:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
1961 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
998404:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
831520:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
1299696:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1247021:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
2022026:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1297059:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
2133236:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
8319301:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
678724:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
3367003:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
2148018:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
6443875:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
2144373:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
3366299:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
718539:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
3136768:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
2236065:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
1253940:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
784673:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
6175258:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
997428:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
2228970:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
4038908:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
3446454:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
1246278:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
19585351:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
6309306:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
8297784:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
20204214:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
2135966:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
3466763:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
6449770:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
22913091:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
4058396:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
6184811:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
19579231:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
18746901:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
18679914:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
22928026:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
34054136:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
20238188:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
2030754:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
3140597:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=1749371cc26417072606d04b91651c05
Cycle=SyncsRR Fre SyncdWW Rfe SyncsRR Fre SyncdWW Rfe
Relax bcsdww038 No BCSyncdWW
Safe=Fre SyncsRR
Time bcsdww038 120.88
$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 16:03:51 GMT 2009