Tue Dec 29 09:18:10 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 3,0(11)
_litmus_P3_1_: xor 10,3,3
_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 7,0(9)
_litmus_P2_1_: sync
_litmus_P2_2_: li 11,2
_litmus_P2_3_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_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 7,0(9)
_litmus_P0_1_: sync
_litmus_P0_2_: li 11,2
_litmus_P0_3_: stw 11,0(9)
Test bcssrw000 Allowed
Histogram (79 states)
1 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
1 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
1 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
18 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
1 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
19 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
17 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
2 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
35 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
22 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
13 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
709 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
177 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=2;
24 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=2;
15 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
35 :>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
146 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
309 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
202 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
33 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
96 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
56 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
161 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=2;
162 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
3150 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
2340 :>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
136 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
107 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=2;
998 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
1960 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=1; y=2;
2354 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
29684 :>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=1; y=1;
4550 :>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
375 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
1684 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
24 :>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
23 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1089 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=1; y=2;
384 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
712920:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
4884 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=1; y=1;
3249 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=2;
17641 :>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
1796664:>0:r1=1; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=0; x=2; y=1;
93536 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
1679166:>0:r1=0; 1:r1=0; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
4072 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
80028 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=0; x=2; y=2;
46478 :>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
151295:>0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=0; x=2; y=2;
23218 :>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
1565 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
3137 :>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=2;
303880:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
2656 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
18968 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=2;
21137 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
20591 :>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
106183:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
61856 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
44135 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=2;
1277599:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
312514:>0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 3:r1=2; 3:r4=2; x=1; y=2;
181296:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=1; y=1;
1988526:>0:r1=1; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
2799869:>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=0; x=2; y=1;
63829 :>0:r1=1; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=0; x=2; y=1;
141039512:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=1; 3:r4=2; x=1; y=1;
12890364:>0:r1=0; 1:r1=2; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
148456431:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=2; 3:r4=2; x=1; y=1;
1415595:>0:r1=0; 1:r1=1; 1:r4=2; 2:r1=0; 3:r1=0; 3:r4=2; x=1; y=1;
2025601:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=1; 3:r4=2; x=1; y=2;
239932:>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
1811988:>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=2; x=1; y=2;
19732 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=1; y=2;
145677:>0:r1=1; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
7 :>0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
15503 :>0:r1=0; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; y=2;
67653 :>0:r1=1; 1:r1=2; 1:r4=0; 2:r1=1; 3:r1=0; 3:r4=0; x=2; 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 65.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 30,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw001 Allowed
Histogram (17 states)
677 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
178 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
312 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1045 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2555 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
2824972:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
27693 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
54902 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
4742856:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
5059701:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
172197:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
147117:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
3740010:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
2921128:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
28616347:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
148524319:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
203163991:>0:r1=1; 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 34.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 29,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(11)
_litmus_P2_3_: xor 8,30,30
_litmus_P2_4_: lwzx 10,8,9
_litmus_P2_5_: sync
_litmus_P2_6_: li 7,1
_litmus_P2_7_: stw 7,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw002 Allowed
Histogram (28 states)
4 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
3 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
20 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
27 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
2 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
5 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
8 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
36 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
23362 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
9044 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
24 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
2 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
4 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; y=1;
25926 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
10931 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
10737 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
1721720:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
1121 :>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
851157:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
59298 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
2860705:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
402 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
2719651:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
119045110:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
1263695:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
571234:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
270825771:>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 37.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 29,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(11)
_litmus_P2_3_: xor 8,30,30
_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 7,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw003 Allowed
Histogram (27 states)
5 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
5 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
4 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
1 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=2;
1 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
58 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
767 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
142 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
112 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
2 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
403 :>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
1735 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=1; 2:r5=0; y=2;
56291 :>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=1; 2:r5=0; y=1;
881 :>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=2; 2:r5=0; y=2;
4298235:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 2:r3=1; 2:r5=0; y=2;
515363:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
245161:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
209478:>0:r1=0; 0:r4=0; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
4452310:>0:r1=0; 0:r4=0; 1:r1=1; 2:r1=2; 2:r3=2; 2:r5=0; y=2;
189 :>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=2; 2:r5=0; y=1;
252131557:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; y=1;
13392650:>0:r1=0; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 2:r5=0; y=1;
1399562:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
10956 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=1;
20866 :>0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
1644501:>0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; y=2;
121618765:>0:r1=1; 0:r4=2; 1:r1=0; 2:r1=2; 2:r3=2; 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=f0d60999a697d3eb825e725dab825965
Cycle=LwSyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw003 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw003 35.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P2_1_: xor 5,4,4
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,5,9
_litmus_P1_0_: lwz 7,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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw004 Allowed
Histogram (22 states)
4 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
7 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
4 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
11 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
12 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
13 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
11 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
72 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
276 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
408 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
3317 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
154 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
58418 :>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
67264 :>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
3644187:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
1958 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
3928212:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
1837 :>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
381817853:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
2691 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
64022 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
10409269:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; 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 36.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 6,1
_litmus_P2_3_: stw 6,0(9)
_litmus_P1_0_: lwz 7,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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw005 Allowed
Histogram (22 states)
26 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
12 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
49 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
74 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
35 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
92 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
81 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
317 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
46506 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
503403:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
1633327:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
11501032:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
690 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
4869 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
90307 :>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
2658 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
48416 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
9176591:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
148194:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
232677:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
331451971:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
45158673:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
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 39.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssrw006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssrw006
"LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe SyncsRW Rfe"
{0:r2=x; 0:r6=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwsync ;
sync | li r3,2 | li r3,1 ;
lwz r3,0(r2) | stw r3,0(r2) | stw r3,0(r4) ;
xor r4,r3,r3 | | ;
lwzx r5,r4,r6 | | ;
sync | | ;
li r7,1 | | ;
stw r7,0(r6) | | ;
exists (x=2 /\ y=2 /\ 0:r3=2 /\ 0:r5=0 /\ 1:r1=1 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 5,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 6,1
_litmus_P2_3_: stw 6,0(9)
_litmus_P1_0_: lwz 7,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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw006 Allowed
Histogram (22 states)
17 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
37 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
39 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=1;
5 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=1;
42 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
383 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=1; y=2;
7903 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
130 :>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=1; y=1;
97570 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
259633435:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=2; y=1;
341619:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=2; x=1; y=1;
634 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=1;
3952 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=2; x=1; y=2;
135201:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=2; x=1; y=2;
123732270:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=0; x=2; y=1;
2297 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=1;
64413 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=0; x=2; y=2;
9114195:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=2; y=2;
48377 :>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=0; x=1; y=2;
114762:>0:r3=2; 0:r5=0; 1:r1=1; 2:r1=1; x=1; y=2;
32 :>0:r3=2; 0:r5=0; 1:r1=0; 2:r1=1; x=1; y=2;
6702687:>0:r3=2; 0:r5=2; 1:r1=0; 2:r1=1; x=1; y=1;
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 37.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 4,10,9
_litmus_P1_0_: lwz 7,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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw007 Allowed
Histogram (17 states)
2 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
15 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
14 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=2;
18 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=1; y=1;
62 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=1; y=2;
1530 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=1; y=2;
389726:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=1; y=2;
7138967:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
2256 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=1; y=1;
6190086:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
499 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=1; y=1;
3142 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=1; y=2;
336366:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=1; y=2;
374294680:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2792 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
26719 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
11613126:>0:r3=1; 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: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 31.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 5,0(9)
_litmus_P1_0_: lwz 7,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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw008 Allowed
Histogram (17 states)
2 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
78 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
46 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
56 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
123 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
65553152:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
20137 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
2025 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
7632974:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
75421 :>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
163122:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
312758329:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; y=1;
2235979:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
11171754:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
683 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
6187 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
379932:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=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: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 33.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 5,0(9)
_litmus_P1_0_: lwz 7,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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw009 Allowed
Histogram (17 states)
125 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=2;
69 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
296 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=1; y=2;
2677692:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
12181468:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
721 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=1; 2:r3=1; y=1;
1507 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
26217 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r3=0; y=2;
8871659:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=0; y=2;
141732:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r3=1; y=2;
76552425:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=0; y=1;
39 :>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r3=1; y=1;
9 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=1;
6963 :>0:r3=1; 0:r5=0; 1:r1=0; 2:r1=2; 2:r3=1; y=2;
474702:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=2; 2:r3=1; y=2;
247087:>0:r3=1; 0:r5=0; 1:r1=1; 2:r1=1; 2:r3=1; y=2;
298817289:>0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r3=0; 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 33.76
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 30,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 29,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 bcssrw010 Allowed
Histogram (22 states)
150 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
20 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
11 :>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
46 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
18 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
52 :>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
22 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
124 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
105799:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
324997:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
19673 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
4657097:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
947 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
4829414:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
303813102:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
1019071:>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
3240080:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
79871487:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
2422 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
39378 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
866393:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
1209697:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
No
Witnesses
Positive: 0, Negative: 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 34.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 30,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 7,0(9)
_litmus_P1_1_: sync
_litmus_P1_2_: li 11,2
_litmus_P1_3_: stw 11,0(9)
_litmus_P0_0_: lwz 29,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 bcssrw011 Allowed
Histogram (22 states)
6 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
8 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
7 :>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
8102 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
2463 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
124 :>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
188 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
254 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=2;
1077 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
2990859:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
21067 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=2;
74346 :>0:r1=0; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
11098 :>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
6238734:>0:r1=1; 0:r3=1; 0:r5=0; 1:r1=1; 2:r1=0; 2:r4=0; y=2;
6613649:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=0; 2:r4=0; y=1;
30147 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=1; 2:r4=0; y=1;
50002 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 2:r1=2; 2:r4=0; y=2;
1660613:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=2; 2:r4=0; y=2;
1906218:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 2:r1=1; 2:r4=0; y=2;
270969037:>0:r1=1; 0:r3=1; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
18642340:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=2; 2:r4=0; y=1;
90779661:>0:r1=0; 0:r3=0; 0:r5=2; 1:r1=0; 2:r1=1; 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=ae75e3d1140839ad4046415fb4f32715
Cycle=DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe SyncsRW Rfe
Relax bcssrw011 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw011 34.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 4,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 4,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)
311862063:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0;
11646149:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0;
316491788:>0:r1=0; 0:r4=0; 1:r1=1; 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 21.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P2_1_: xor 10,3,3
_litmus_P2_2_: lwzx 4,10,9
_litmus_P2_3_: sync
_litmus_P2_4_: li 8,1
_litmus_P2_5_: stw 8,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 4,10,9
_litmus_P1_3_: sync
_litmus_P1_4_: li 8,1
_litmus_P1_5_: stw 8,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_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)
161295:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
57883725:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=0;
60906423:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
67445544:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=0;
71012179:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0;
76453370:>0:r1=1; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0;
66137464:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 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 33.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(9)
_litmus_P2_1_: xor 10,4,4
_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 3,0(11)
_litmus_P1_1_: xor 10,3,3
_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 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 30,10,9
_litmus_P0_3_: sync
_litmus_P0_4_: li 8,1
_litmus_P0_5_: stw 8,0(9)
Test bcssrw014 Allowed
Histogram (21 states)
19 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
6 :>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
1610 :>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
5985 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
1192 :>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
502 :>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
12 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=1; y=2;
10367 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
9952 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
302006:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
338544:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
6102953:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
8186363:>0:r1=2; 0:r4=0; 1:r1=0; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
199819665:>0:r1=2; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
4884216:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=2; 2:r1=0; 2:r4=0; y=1;
27718 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=1;
25833 :>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r4=0; y=2;
4467196:>0:r1=0; 0:r4=0; 1:r1=1; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
4273472:>0:r1=0; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
4613534:>0:r1=1; 0:r4=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r4=1; y=2;
166928855:>0:r1=1; 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 35.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 4,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)
597684:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
468487929:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
516894:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
170397493:>0:r1=1; 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=15f52564e04daa74ee8b809a62b31ce5
Cycle=SyncsRR DpdR SyncsRW Rfe DpdR SyncsRW Rfe
Relax bcssrw015 No BCSyncsRW
Safe=SyncsRR DpdR
Time bcssrw015 21.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_P1_5_: sync
_litmus_P1_6_: li 7,1
_litmus_P1_7_: stw 7,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: xor 10,3,3
_litmus_P0_2_: lwzx 4,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)
38994 :>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=1; 1:r5=0;
435086431:>0:r1=0; 0:r4=0; 1:r1=1; 1:r3=1; 1:r5=0;
16831833:>0:r1=0; 0:r4=0; 1:r1=0; 1:r3=0; 1:r5=0;
188042742:>0:r1=1; 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 21.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P1_1_: xor 5,4,4
_litmus_P1_2_: li 10,1
_litmus_P1_3_: stwx 10,5,9
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw017 Allowed
Histogram (4 states)
604 :>0:r3=1; 0:r5=0; 1:r1=0; x=1;
6023 :>0:r3=2; 0:r5=0; 1:r1=0; x=1;
12018201:>0:r3=2; 0:r5=0; 1:r1=1; x=1;
627975172:>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=97b40d67b76129b3ab3e1a6a5f6305eb
Cycle=DpdW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw017 No BCSyncsRW
Safe=Wse SyncsWR DpdW DpdR
Time bcssrw017 20.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 6,1
_litmus_P1_3_: stw 6,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw018 Allowed
Histogram (4 states)
3994 :>0:r3=1; 0:r5=0; 1:r1=0; x=1;
94303 :>0:r3=2; 0:r5=0; 1:r1=0; x=1;
616431257:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
23470446:>0:r3=2; 0:r5=0; 1:r1=1; 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 24.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: xor 10,3,3
_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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw019 Allowed
Histogram (6 states)
377688345:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
525739:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
80031 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
553450:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
1261119:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
259891316:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
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 25.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: li 6,1
_litmus_P1_3_: stw 6,0(9)
_litmus_P0_0_: li 10,2
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw020 Allowed
Histogram (4 states)
621762436:>0:r3=2; 0:r5=0; 1:r1=0; x=2;
1754 :>0:r3=1; 0:r5=0; 1:r1=0; x=1;
58863 :>0:r3=2; 0:r5=0; 1:r1=0; x=1;
18176947:>0:r3=2; 0:r5=0; 1:r1=1; 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=7f2323c0dd7502796856c97da172b168
Cycle=LwSyncdRW Wse SyncsWR DpdR SyncsRW Rfe
Relax bcssrw020 No BCSyncsRW
Safe=Wse SyncsWR LwSyncdRW DpdR
Time bcssrw020 23.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: xor 10,3,3
_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 29,0(11)
_litmus_P0_4_: xor 8,29,29
_litmus_P0_5_: lwzx 30,8,9
_litmus_P0_6_: sync
_litmus_P0_7_: li 7,1
_litmus_P0_8_: stw 7,0(9)
Test bcssrw021 Allowed
Histogram (6 states)
359903565:>0:r3=2; 0:r5=0; 1:r1=1; 1:r4=2; x=1;
51250 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
119234:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=2; x=1;
293817:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
627150:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=1;
279004984:>0:r3=2; 0:r5=0; 1:r1=0; 1:r4=0; x=2;
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 24.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 4,0(11)
_litmus_P1_1_: xor 10,4,4
_litmus_P1_2_: lwzx 5,10,9
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_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)
6265 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1;
11111846:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1;
628881889:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0;
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 18.97
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,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 3,0(11)
_litmus_P0_4_: xor 8,3,3
_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)
73571 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
608641060:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
89874 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
31195495:>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=c2c9c0359658b64e4185d23d932ca70a
Cycle=SyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw023 No BCSyncsRW
Safe=Fre SyncsWR SyncsRR DpdR
Time bcssrw023 20.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,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 3,0(11)
_litmus_P0_4_: xor 8,3,3
_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)
18520 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=1;
16260 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=1;
30553894:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=1;
609411326:>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=dcde740d5eace2726b3b99bfd0448c43
Cycle=LwSyncsRR DpdR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw024 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw024 20.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 6,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_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)
618499754:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
18156 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
21482090:>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=8047871ef7343012976d8a83d92f5d9f
Cycle=SyncdRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw025 No BCSyncsRW
Safe=Fre SyncsWR SyncdRR DpdR
Time bcssrw025 20.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: xor 8,3,3
_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 3,0(11)
_litmus_P0_4_: xor 8,3,3
_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)
806943:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
1041452:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
318406694:>0:r3=1; 0:r5=0; 1:r1=1; 1:r4=1; 1:r6=1;
319744911:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
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 21.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 5,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 6,0(9)
_litmus_P0_0_: li 10,1
_litmus_P0_1_: stw 10,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(11)
_litmus_P0_4_: xor 8,3,3
_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)
13520 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=1;
26741272:>0:r3=1; 0:r5=0; 1:r1=1; 1:r3=1;
613245208:>0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0;
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 19.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 3,0(11)
_litmus_P1_1_: xor 8,3,3
_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 3,0(11)
_litmus_P0_4_: xor 8,3,3
_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)
23338 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=1;
316845626:>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=0; 1:r6=0;
75021 :>0:r3=1; 0:r5=0; 1:r1=0; 1:r4=1; 1:r6=1;
323056015:>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=f96ce8a4017924c7511ae42d30af7292
Cycle=DpdR LwSyncsRR Fre SyncsWR DpdR SyncsRW Rfe
Relax bcssrw028 No BCSyncsRW
Safe=Fre SyncsWR LwSyncsRR DpdR
Time bcssrw028 22.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_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_: sync
_litmus_P0_2_: lwz 31,0(11)
_litmus_P0_3_: xor 8,31,31
_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)
2017988:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
1895779:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
7944012:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
290847272:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
337294949:>0:r1=1; 0:r3=1; 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 23.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_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_: sync
_litmus_P0_2_: lwz 31,0(11)
_litmus_P0_3_: xor 8,31,31
_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)
3177 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
266628166:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
1660117:>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
3406760:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
368301780:>0:r1=1; 0:r3=1; 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 23.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 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_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_: lwsync
_litmus_P0_2_: lwz 31,0(11)
_litmus_P0_3_: xor 8,31,31
_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)
23568 :>0:r1=0; 0:r3=1; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
16370 :>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=1; 1:r5=0;
297368207:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=1; 1:r3=1; 1:r5=0;
18795587:>0:r1=0; 0:r3=0; 0:r5=0; 1:r1=0; 1:r3=0; 1:r5=0;
323796268:>0:r1=1; 0:r3=1; 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=ae803005916745f384198d670ee29f6c
Cycle=LwSyncsRR DpdR SyncsRW Rfe LwSyncsRR DpdR SyncsRW Rfe
Relax bcssrw031 No BCSyncsRW
Safe=LwSyncsRR DpdR
Time bcssrw031 23.40
$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: none */
/* 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=-s 100000 -r 400
Tue Dec 29 09:33:35 GMT 2009