Thu Dec 24 11:41:52 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr000
"Fre SyncdWW Rfe PodRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) ;
sync | ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwz r8,0(r2)
Test podrr000 Allowed
Histogram (4 states)
12 :>1:r1=1; 1:r3=0;
907067:>1:r1=0; 1:r3=1;
914289:>1:r1=0; 1:r3=0;
178632:>1:r1=1; 1:r3=1;
Ok
Witnesses
Positive: 12, Negative: 1999988
Condition exists (1:r1=1 /\ 1:r3=0) is validated
Hash=78d7a77bf8b1a9bd43cfddf06e35d5d3
Cycle=Fre SyncdWW Rfe PodRR
Relax podrr000 Ok PodRR
Safe=Fre BCSyncdWW
Time podrr000 1.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr001
"Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
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_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: sync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr001 Allowed
Histogram (15 states)
133 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
713 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
137 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1513 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
11399 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
19954 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
43152 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
79625 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
167987:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
41701 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
89857 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
282215:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
131944:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
42966 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
86704 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=2e6b2a124722ed948c8f7dc35dc4b80f
Cycle=Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr001 No PodRR
Safe=Fre BCSyncdWW
Time podrr001 2.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr002
"Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwz r8,0(r2)
_litmus_P2_0_: li r11,1
_litmus_P2_1_: stw r11,0(r9)
_litmus_P2_2_: sync
_litmus_P2_3_: li r10,1
_litmus_P2_4_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr002 Allowed
Histogram (33 states)
7 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
12 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
13 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
764 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
209 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
186 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
457 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
389 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
17623 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2660 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1044 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
57877 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
9954 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
7777 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
9766 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
36953 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
851 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
82117 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
32435 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
40354 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
31099 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
28578 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
6768 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
95901 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
92575 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
4591 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
12285 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
5144 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
97862 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
273468:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
35106 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
15174 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c594109cf9f75c58c9eec5a696ceb0a0
Cycle=Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR
Relax podrr002 No PodRR
Safe=Fre BCSyncsWW BCSyncdWW
Time podrr002 2.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr003
"Fre SyncdWW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,1 | stw r3,0(r4) | ;
stw r3,0(r4) | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r10,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stw r8,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwz r8,0(r2)
Test podrr003 Allowed
Histogram (7 states)
13116 :>1:r1=0; 2:r1=1; 2:r3=0;
262559:>1:r1=0; 2:r1=0; 2:r3=1;
162359:>1:r1=1; 2:r1=0; 2:r3=1;
361405:>1:r1=0; 2:r1=0; 2:r3=0;
197687:>1:r1=0; 2:r1=1; 2:r3=1;
691 :>1:r1=1; 2:r1=1; 2:r3=1;
2183 :>1:r1=1; 2:r1=0; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=3d48b5b0d8516d3d909b0a4f66959c71
Cycle=Fre SyncdWW Rfe SyncdRW Rfe PodRR
Relax podrr003 No PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr003 1.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr004
"Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: lwz r8,0(r9)
_litmus_P2_1_: sync
_litmus_P2_2_: li r10,1
_litmus_P2_3_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr004 Allowed
Histogram (15 states)
1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0;
116 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0;
347 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0;
209 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1;
487 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1;
303 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1;
4414 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0;
30379 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1;
124958:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1;
314727:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0;
126784:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1;
188057:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0;
113220:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1;
16316 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1;
79682 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=b2067185c885838837d33372d57790fb
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr004 No PodRR
Safe=Fre BCSyncdWW BCSyncdRW
Time podrr004 2.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr005
"Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,1 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r2) | | | ;
exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: lwz r8,0(r9)
_litmus_P2_1_: sync
_litmus_P2_2_: li r10,1
_litmus_P2_3_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr005 Allowed
Histogram (31 states)
2 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
5 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
7 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2;
22 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
184 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
2 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
35 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
265 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
486 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
533 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
736 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
10352 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
37872 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2;
7469 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
46930 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
9478 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
8501 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
26498 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
7716 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
28860 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
22790 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
25612 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
40525 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
196621:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
39265 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
128036:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
51574 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
149647:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
22848 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
117124:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
20005 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=1a4d6f8ada041391fb8c242b28f54910
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR
Relax podrr005 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr005 2.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr006
"Fre SyncsWW Rfe SyncdRW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,1 | ;
li r3,2 | stw r3,0(r4) | ;
stw r3,0(r2) | | ;
exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r10,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: li r8,1
_litmus_P1_3_: stw r8,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwz r8,0(r2)
Test podrr006 Allowed
Histogram (17 states)
1 :>1:r1=1; 2:r1=1; 2:r3=1; y=2;
3 :>1:r1=2; 2:r1=1; 2:r3=1; y=2;
2 :>1:r1=1; 2:r1=1; 2:r3=0; y=2;
19 :>1:r1=1; 2:r1=0; 2:r3=1; y=2;
2612 :>1:r1=0; 2:r1=0; 2:r3=2; y=2;
8596 :>1:r1=2; 2:r1=0; 2:r3=0; y=2;
45433 :>1:r1=2; 2:r1=0; 2:r3=1; y=2;
13402 :>1:r1=1; 2:r1=1; 2:r3=2; y=2;
29935 :>1:r1=0; 2:r1=1; 2:r3=0; y=2;
99624 :>1:r1=1; 2:r1=0; 2:r3=2; y=2;
37281 :>1:r1=0; 2:r1=0; 2:r3=1; y=2;
154835:>1:r1=1; 2:r1=0; 2:r3=0; y=2;
189601:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
162598:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
45632 :>1:r1=0; 2:r1=1; 2:r3=2; y=2;
11564 :>1:r1=2; 2:r1=1; 2:r3=2; y=2;
198862:>1:r1=2; 2:r1=0; 2:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=f5e5097c67500c52603a1c0158bb8551
Cycle=Fre SyncsWW Rfe SyncdRW Rfe PodRR
Relax podrr006 No PodRR
Safe=Fre BCSyncsWW BCSyncdRW
Time podrr006 1.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr007
"Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,2 | li r3,1 | ;
li r3,1 | stw r3,0(r2) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r10,0(r2)
_litmus_P1_1_: sync
_litmus_P1_2_: li r9,2
_litmus_P1_3_: stw r9,0(r2)
_litmus_P2_0_: lwz r8,0(r9)
_litmus_P2_1_: sync
_litmus_P2_2_: li r10,1
_litmus_P2_3_: stw r10,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr007 Allowed
Histogram (30 states)
1 :>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
185 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
20 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2;
94 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1;
68 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
259 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
1314 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2;
333 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2;
626 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2;
1761 :>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
1057 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1;
9221 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
7769 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1;
4869 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1;
20937 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
12926 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2;
34483 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1;
33892 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
61525 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2;
10291 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1;
81814 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2;
79074 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1;
63480 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
133001:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1;
192477:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1;
29752 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2;
68763 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1;
87967 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2;
41970 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1;
20071 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c22fcb545cb7b0f7f27c11adc702bd5e
Cycle=Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR
Relax podrr007 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr007 2.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr008
"Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ;
sync | | sync | ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P2_2_: sync
_litmus_P2_3_: li r11,2
_litmus_P2_4_: stw r11,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr008 Allowed
Histogram (75 states)
1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
5 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
4 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
10 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
21 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
81 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
20 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
4 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
15 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
6 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
9 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
29 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
87 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
230 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
141 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
29 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
57 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
295 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
997 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
380 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2490 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
290 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2369 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
274 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2613 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
9498 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1791 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2341 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1631 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4078 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5063 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
7313 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
15675 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
8388 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3681 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
45447 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
32721 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
20639 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
3777 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4270 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
21354 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
19320 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
3936 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
13470 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
10430 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
31609 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
12553 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16729 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
19599 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
12502 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
48511 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
9909 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
18556 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
40730 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3579 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
10172 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
53451 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
137571:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
30129 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
53172 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
8918 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
34217 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
11876 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3142 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
31124 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
19533 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
62029 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
85093 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=58c192e74d841e0ccb20b3014a58a473
Cycle=Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR
Relax podrr008 No PodRR
Safe=Fre BCSyncsWW
Time podrr008 4.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr009
"Fre SyncdWW Rfe SyncsRW Rfe PodRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r4) ;
sync | li r3,2 | ;
li r3,1 | stw r3,0(r2) | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r10,0(r2)
_litmus_P1_1_: sync
_litmus_P1_2_: li r9,2
_litmus_P1_3_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwz r8,0(r2)
Test podrr009 Allowed
Histogram (16 states)
6 :>1:r1=0; 2:r1=2; 2:r3=0; x=2;
12 :>1:r1=0; 2:r1=1; 2:r3=0; x=2;
28 :>1:r1=0; 2:r1=1; 2:r3=0; x=1;
677 :>1:r1=1; 2:r1=0; 2:r3=0; x=2;
61430 :>1:r1=0; 2:r1=2; 2:r3=1; x=2;
72568 :>1:r1=0; 2:r1=2; 2:r3=0; x=1;
67621 :>1:r1=1; 2:r1=1; 2:r3=1; x=2;
287404:>1:r1=0; 2:r1=0; 2:r3=0; x=1;
59545 :>1:r1=0; 2:r1=1; 2:r3=1; x=2;
19152 :>1:r1=0; 2:r1=0; 2:r3=1; x=1;
221090:>1:r1=0; 2:r1=2; 2:r3=1; x=1;
31986 :>1:r1=1; 2:r1=0; 2:r3=1; x=2;
45422 :>1:r1=0; 2:r1=0; 2:r3=0; x=2;
39979 :>1:r1=0; 2:r1=1; 2:r3=1; x=1;
4105 :>1:r1=1; 2:r1=2; 2:r3=1; x=2;
88975 :>1:r1=0; 2:r1=0; 2:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=d6249053a9b844d8e7a3045b38500a3a
Cycle=Fre SyncdWW Rfe SyncsRW Rfe PodRR
Relax podrr009 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW
Time podrr009 1.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr010
"Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r4) | | | ;
exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: lwz r10,0(r2)
_litmus_P2_1_: sync
_litmus_P2_2_: li r9,2
_litmus_P2_3_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr010 Allowed
Histogram (30 states)
1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
24 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
56 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
211 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
399 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
147 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
6830 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
1011 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
665 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
6006 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2;
31443 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
11112 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2;
105124:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
17496 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
36964 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2;
8995 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2;
6460 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2;
1789 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2;
17612 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2;
13636 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2;
2695 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1;
113965:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1;
118049:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2;
78954 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2;
104930:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1;
41521 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2;
53618 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2;
179926:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1;
24013 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1;
16348 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=fcb68021656d7cbdb455ef5bd2648d65
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr010 No PodRR
Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW
Time podrr010 2.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/podrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
podrr011
"Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r4) ;
sync | li r3,1 | li r3,2 | ;
li r3,2 | stw r3,0(r4) | stw r3,0(r2) | ;
stw r3,0(r2) | | | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r8,0(r9)
_litmus_P1_1_: sync
_litmus_P1_2_: li r10,1
_litmus_P1_3_: stw r10,0(r2)
_litmus_P2_0_: lwz r10,0(r2)
_litmus_P2_1_: sync
_litmus_P2_2_: li r9,2
_litmus_P2_3_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwz r8,0(r2)
Test podrr011 Allowed
Histogram (67 states)
1 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
2 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
1 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
30 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
8 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
40 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
12 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
78 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
3 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
89 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
18 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
420 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
401 :>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
222 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
81 :>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
355 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2;
2509 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2;
137 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
6833 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2;
1060 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2;
1390 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
2315 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
10132 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2;
6505 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
303 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
624 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
13387 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
17860 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2;
5231 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
1224 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2;
9758 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2;
7153 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2;
2348 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2;
1095 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
6305 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2;
2026 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
5565 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2;
385 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
30264 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
82388 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2;
17707 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
21091 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2;
4043 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2;
8494 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2;
3915 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
6376 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2;
10459 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2;
15580 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
69709 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
83596 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2;
1020 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
12042 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
42009 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2;
52914 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2;
55712 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
42476 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
2539 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2;
109907:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2;
109679:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2;
83898 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2;
3390 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
2256 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2;
22624 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 1000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=a463a88f960487eded38b9c473eec1b5
Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR
Relax podrr011 No PodRR
Safe=Fre BCSyncsWW BCSyncsRW BCSyncdRW
Time podrr011 3.81
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=
Thu Dec 24 11:42:20 CET 2009