Wed Dec 23 13:38:58 NFT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr000
"Fre SyncdWW Rfe PosRR DpdR PosRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r6=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r2) ;
sync | xor r4,r3,r3 ;
li r3,1 | lwzx r5,r4,r6 ;
stw r3,0(r4) | lwz r7,0(r6) ;
exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0 /\ 1:r7=0)
Generated assembler
_litmus_P1_0_: lwz 25,0(11)
_litmus_P1_1_: lwz 29,0(11)
_litmus_P1_2_: xor 6,29,29
_litmus_P1_3_: lwzx 8,6,9
_litmus_P1_4_: lwz 7,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 posrr000 Allowed
Histogram (5 states)
220 :>1:r1=0; 1:r3=0; 1:r5=0; 1:r7=1;
1101 :>1:r1=0; 1:r3=1; 1:r5=1; 1:r7=1;
10659589:>1:r1=1; 1:r3=1; 1:r5=1; 1:r7=1;
7264598:>1:r1=0; 1:r3=0; 1:r5=1; 1:r7=1;
14074492:>1:r1=0; 1:r3=0; 1:r5=0; 1:r7=0;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0 /\ 1:r7=0) is NOT validated
Hash=dca4403d3afb34d355df5cfe6b045e45
Cycle=Fre SyncdWW Rfe PosRR DpdR PosRR
Relax posrr000 No PosRR
Safe=Fre DpdR BCSyncdWW
Time posrr000 7.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr001
"Fre SyncdWW Rfe SyncdRW Rfe PosRR DpdR PosRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r6=z;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r2) ;
sync | li r3,1 | xor r4,r3,r3 ;
li r3,1 | stw r3,0(r4) | lwzx r5,r4,r6 ;
stw r3,0(r4) | | lwz r7,0(r6) ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0 /\ 2:r7=0)
Generated assembler
_litmus_P2_0_: lwz 24,0(11)
_litmus_P2_1_: lwz 29,0(11)
_litmus_P2_2_: xor 6,29,29
_litmus_P2_3_: lwzx 8,6,9
_litmus_P2_4_: lwz 7,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,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 posrr001 Allowed
Histogram (13 states)
23 :>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=1;
47 :>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; 2:r7=1;
112 :>1:r1=1; 2:r1=0; 2:r3=1; 2:r5=1; 2:r7=1;
184 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; 2:r7=0;
91 :>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=1;
406 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=1; 2:r7=1;
1786266:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; 2:r7=0;
1069547:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=1; 2:r7=1;
5971152:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=0;
1065376:>1:r1=1; 2:r1=1; 2:r3=1; 2:r5=1; 2:r7=1;
1645415:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=0;
4710639:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=1; 2:r7=1;
4750742:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=1; 2:r7=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0 /\ 2:r7=0) is NOT validated
Hash=bda3ebc8e325ea91e8b0f345967e27a9
Cycle=Fre SyncdWW Rfe SyncdRW Rfe PosRR DpdR PosRR
Relax posrr001 No PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr001 7.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr002
"Fre SyncdWW Rfe DpdR PosRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r5=y;}
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 | lwz r6,0(r5) ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r4=0 /\ 1:r6=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: xor 7,27,27
_litmus_P1_2_: lwzx 29,7,9
_litmus_P1_3_: lwz 8,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 posrr002 Allowed
Histogram (4 states)
256 :>1:r1=0; 1:r4=0; 1:r6=1;
5612275:>1:r1=0; 1:r4=1; 1:r6=1;
11572487:>1:r1=1; 1:r4=1; 1:r6=1;
14814982:>1:r1=0; 1:r4=0; 1:r6=0;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated
Hash=aa763fab21553ece116fd280efdc92e3
Cycle=Fre SyncdWW Rfe DpdR PosRR
Relax posrr002 No PosRR
Safe=Fre DpdR BCSyncdWW
Time posrr002 7.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr003
"DpdR Fre SyncdWW Rfe DpdR PosRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 1:r9=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 | lwz r6,0(r5) ;
stw r3,0(r4) | xor r7,r6,r6 ;
| lwzx r8,r7,r9 ;
exists (1:r1=1 /\ 1:r8=0)
Generated assembler
_litmus_P1_0_: lwz 24,0(10)
_litmus_P1_1_: xor 29,24,24
_litmus_P1_2_: lwzx 7,29,11
_litmus_P1_3_: lwz 6,0(11)
_litmus_P1_4_: xor 5,6,6
_litmus_P1_5_: lwzx 25,5,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 posrr003 Allowed
Histogram (3 states)
6490295:>1:r1=0; 1:r8=1;
14196303:>1:r1=0; 1:r8=0;
11313402:>1:r1=1; 1:r8=1;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (1:r1=1 /\ 1:r8=0) is NOT validated
Hash=b660291ec0b800081e710e7f87d96ef9
Cycle=DpdR Fre SyncdWW Rfe DpdR PosRR
Relax posrr003 No PosRR
Safe=Fre DpdR BCSyncdWW
Time posrr003 4.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr004
"Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z;}
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,1 | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | lwz r6,0(r5) ;
stw r3,0(r4) | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r4=0 /\ 2:r6=0)
Generated assembler
_litmus_P2_0_: lwz 26,0(11)
_litmus_P2_1_: xor 7,26,26
_litmus_P2_2_: lwzx 29,7,9
_litmus_P2_3_: lwz 8,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,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 posrr004 Allowed
Histogram (10 states)
33 :>1:r1=0; 2:r1=1; 2:r4=0; 2:r6=1;
110 :>1:r1=0; 2:r1=0; 2:r4=0; 2:r6=1;
22 :>1:r1=1; 2:r1=0; 2:r4=0; 2:r6=1;
992458:>1:r1=0; 2:r1=0; 2:r4=1; 2:r6=1;
6268961:>1:r1=0; 2:r1=0; 2:r4=0; 2:r6=0;
1069714:>1:r1=1; 2:r1=1; 2:r4=1; 2:r6=1;
1911453:>1:r1=0; 2:r1=1; 2:r4=0; 2:r6=0;
4488550:>1:r1=1; 2:r1=0; 2:r4=1; 2:r6=1;
1609930:>1:r1=1; 2:r1=0; 2:r4=0; 2:r6=0;
4658769:>1:r1=0; 2:r1=1; 2:r4=1; 2:r6=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r4=0 /\ 2:r6=0) is NOT validated
Hash=dc1e41e1ec2673d57c366537084bc1c4
Cycle=Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR
Relax posrr004 No PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr004 8.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr005
"DpdR Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=a; 2:r9=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,1 | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | lwz r6,0(r5) ;
stw r3,0(r4) | | xor r7,r6,r6 ;
| | lwzx r8,r7,r9 ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r8=0)
Generated assembler
_litmus_P2_0_: lwz 23,0(10)
_litmus_P2_1_: xor 25,23,23
_litmus_P2_2_: lwzx 7,25,11
_litmus_P2_3_: lwz 6,0(11)
_litmus_P2_4_: xor 5,6,6
_litmus_P2_5_: lwzx 24,5,9
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test posrr005 Allowed
Histogram (7 states)
1663682:>1:r1=1; 2:r1=0; 2:r8=0;
1026428:>1:r1=0; 2:r1=0; 2:r8=1;
1739481:>1:r1=0; 2:r1=1; 2:r8=0;
6011298:>1:r1=0; 2:r1=0; 2:r8=0;
4330559:>1:r1=1; 2:r1=0; 2:r8=1;
5070361:>1:r1=0; 2:r1=1; 2:r8=1;
1158191:>1:r1=1; 2:r1=1; 2:r8=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r8=0) is NOT validated
Hash=8d0831339733254b3c8a1735bb7650c7
Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR
Relax posrr005 No PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr005 5.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr006
"Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe DpdR PosRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=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 | xor r3,r1,r1 ;
sync | li r3,1 | li r3,1 | lwzx r4,r3,r5 ;
li r3,1 | stw r3,0(r4) | stw r3,0(r4) | lwz r6,0(r5) ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r4=0 /\ 3:r6=0)
Generated assembler
_litmus_P3_0_: lwz 27,0(11)
_litmus_P3_1_: xor 7,27,27
_litmus_P3_2_: lwzx 29,7,9
_litmus_P3_3_: lwz 8,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,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 posrr006 Allowed
Histogram (22 states)
10 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=1;
14 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=1;
11 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r4=0; 3:r6=1;
31 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=1;
44 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=1;
23 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=1;
71 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=1;
280202:>1:r1=0; 2:r1=0; 3:r1=0; 3:r4=1; 3:r6=1;
1925800:>1:r1=1; 2:r1=0; 3:r1=1; 3:r4=1; 3:r6=1;
1050975:>1:r1=1; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=0;
1550050:>1:r1=1; 2:r1=0; 3:r1=0; 3:r4=1; 3:r6=1;
101680:>1:r1=1; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=0;
673167:>1:r1=0; 2:r1=1; 3:r1=1; 3:r4=1; 3:r6=1;
1674378:>1:r1=0; 2:r1=1; 3:r1=0; 3:r4=1; 3:r6=1;
1898229:>1:r1=0; 2:r1=0; 3:r1=1; 3:r4=1; 3:r6=1;
89765 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r4=0; 3:r6=0;
49385 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r4=1; 3:r6=1;
1111572:>1:r1=0; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=0;
2214249:>1:r1=0; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=0;
83092 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=0;
704454:>1:r1=1; 2:r1=1; 3:r1=0; 3:r4=1; 3:r6=1;
2592798:>1:r1=0; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=0;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r4=0 /\ 3:r6=0) is NOT validated
Hash=2669164f7a2ad6879aaa11955c600dc5
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe DpdR PosRR
Relax posrr006 No PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr006 18.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr007
"Fre SyncdWW Rfe PosRR Fre SyncdWW Rfe PosRR"
{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) | lwz r3,0(r2) | stw r1,0(r2) | lwz r3,0(r2) ;
sync | | sync | ;
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 31,0(9)
_litmus_P3_1_: 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 31,0(9)
_litmus_P1_1_: 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 posrr007 Allowed
Histogram (83 states)
3 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1;
1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
2 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1;
2 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
1 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
1 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2;
3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
6 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1;
5 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
4 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
13 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1;
2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
8 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
4 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
3 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1;
6 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
10 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
8 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
6 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1;
6 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
1 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
5 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
5 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
10 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
20 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
3 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
10 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2;
10 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
28 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
12 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1;
25 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
20 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
19 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
12 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
38 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
32 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
19 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
9 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
14 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
11 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2;
8 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
40 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
32 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1;
20 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
13 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1;
23 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1;
56 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
8 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
44 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1;
200005:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2;
348392:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2;
218063:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
374991:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1;
384679:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1;
120874:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1140845:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1;
298687:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1;
916515:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2;
1325538:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1;
313512:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1224110:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
957263:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2;
67084 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1;
170899:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2;
1183700:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
456168:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
360600:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1;
281927:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1;
1799165:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1;
292831:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1;
292174:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
310858:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1;
424434:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
603455:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1033718:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
898864:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=dd5096b6f2bf4363a180ba8c94b71b97
Cycle=Fre SyncdWW Rfe PosRR Fre SyncdWW Rfe PosRR
Relax posrr007 No PosRR
Safe=Fre BCSyncdWW
Time posrr007 18.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr008
"DpdR Fre SyncdWW Rfe PosRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r6=x;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwz r3,0(r2) ;
sync | xor r4,r3,r3 ;
li r3,1 | lwzx r5,r4,r6 ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0)
Generated assembler
_litmus_P1_0_: lwz 27,0(11)
_litmus_P1_1_: lwz 29,0(11)
_litmus_P1_2_: xor 7,29,29
_litmus_P1_3_: lwzx 8,7,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 posrr008 Allowed
Histogram (4 states)
639 :>1:r1=0; 1:r3=1; 1:r5=1;
11298103:>1:r1=1; 1:r3=1; 1:r5=1;
4968686:>1:r1=0; 1:r3=0; 1:r5=1;
15732572:>1:r1=0; 1:r3=0; 1:r5=0;
No
Witnesses
Positive: 0, Negative: 32000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0) is NOT validated
Hash=2ca85242fec82e5b95f9a9a93b21e48a
Cycle=DpdR Fre SyncdWW Rfe PosRR
Relax posrr008 No PosRR
Safe=Fre DpdR BCSyncdWW
Time posrr008 1.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr009
"Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PosRR"
{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) | lwz r3,0(r2) ;
sync | lwzx r4,r3,r5 | sync | ;
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 31,0(9)
_litmus_P3_1_: 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 30,0(11)
_litmus_P1_1_: xor 8,30,30
_litmus_P1_2_: lwzx 31,8,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 posrr009 Allowed
Histogram (41 states)
2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
4 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=2;
16 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2;
3 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1;
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
2 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
51 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1;
11 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
11 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
2 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1;
18 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2;
2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
16 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2;
35 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
74 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1;
9 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
67 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2;
20 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2;
41 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1;
5 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1;
100591:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
175515:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
67637 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
185600:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
310287:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2;
277544:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2;
227687:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1055944:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1315883:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2;
2381247:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1;
473676:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2;
1092092:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2;
1031187:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
869063:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
1070698:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1;
1294692:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1323906:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1;
351056:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1;
730077:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1;
217459:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2;
1447768:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=b445d37d77e5c3f9fac5d5dce20158ec
Cycle=Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PosRR
Relax posrr009 No PosRR
Safe=Fre DpdR BCSyncdWW
Time posrr009 2.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr010
"Fre SyncdWW Rfe SyncdRW Rfe PosRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;}
P0 | P1 | P2 ;
li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r2) ;
sync | li r3,1 | ;
li r3,1 | stw r3,0(r4) | ;
stw r3,0(r4) | | ;
exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r3=1)
Generated assembler
_litmus_P2_0_: lwz 31,0(9)
_litmus_P2_1_: lwz 11,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,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 posrr010 Allowed
Histogram (18 states)
3 :>1:r1=0; 2:r1=0; 2:r3=2; y=1;
4 :>1:r1=1; 2:r1=0; 2:r3=2; y=1;
18 :>1:r1=1; 2:r1=0; 2:r3=1; y=1;
70 :>1:r1=0; 2:r1=0; 2:r3=2; y=2;
24 :>1:r1=0; 2:r1=2; 2:r3=1; y=1;
127 :>1:r1=0; 2:r1=0; 2:r3=1; y=2;
167 :>1:r1=1; 2:r1=2; 2:r3=1; y=1;
140 :>1:r1=0; 2:r1=1; 2:r3=2; y=2;
78 :>1:r1=0; 2:r1=0; 2:r3=1; y=1;
456836:>1:r1=0; 2:r1=2; 2:r3=2; y=1;
1183790:>1:r1=1; 2:r1=1; 2:r3=1; y=1;
1597830:>1:r1=0; 2:r1=1; 2:r3=1; y=1;
2244391:>1:r1=0; 2:r1=0; 2:r3=0; y=1;
2595096:>1:r1=0; 2:r1=1; 2:r3=1; y=2;
2689002:>1:r1=0; 2:r1=2; 2:r3=2; y=2;
1674981:>1:r1=1; 2:r1=0; 2:r3=0; y=1;
4316018:>1:r1=1; 2:r1=2; 2:r3=2; y=1;
4241425:>1:r1=0; 2:r1=0; 2:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r3=1) is NOT validated
Hash=5b3cfa45c2982145969071c6dab1a9d9
Cycle=Fre SyncdWW Rfe SyncdRW Rfe PosRR
Relax posrr010 No PosRR
Safe=Fre BCSyncdWW BCSyncdRW
Time posrr010 1.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr011
"DpdR Fre SyncdWW Rfe SyncdRW Rfe PosRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r6=x;}
P0 | P1 | P2 ;
li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | lwz r3,0(r2) ;
sync | li r3,1 | xor r4,r3,r3 ;
li r3,1 | stw r3,0(r4) | lwzx r5,r4,r6 ;
stw r3,0(r4) | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0)
Generated assembler
_litmus_P2_0_: lwz 26,0(11)
_litmus_P2_1_: lwz 29,0(11)
_litmus_P2_2_: xor 7,29,29
_litmus_P2_3_: lwzx 8,7,9
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,0(9)
_litmus_P0_0_: li 31,1
_litmus_P0_1_: stw 31,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 3,1
_litmus_P0_4_: stw 3,0(9)
Test posrr011 Allowed
Histogram (10 states)
104 :>1:r1=1; 2:r1=0; 2:r3=1; 2:r5=1;
32 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0;
145 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=1;
1115762:>1:r1=1; 2:r1=1; 2:r3=1; 2:r5=1;
4662268:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=1;
1769619:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0;
537543:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=1;
1926246:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0;
6007720:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0;
4980561:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=1;
No
Witnesses
Positive: 0, Negative: 21000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0) is NOT validated
Hash=8b1358e772205e1d07c702e088c475e5
Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe PosRR
Relax posrr011 No PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr011 2.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr012
"Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR"
{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) | lwz r1,0(r2) | lwz r1,0(r2) ;
stw r1,0(r2) | sync | sync | lwz r3,0(r2) ;
sync | li r3,1 | li r3,1 | ;
li r3,1 | stw r3,0(r4) | stw r3,0(r4) | ;
stw r3,0(r4) | | | ;
exists (z=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=1)
Generated assembler
_litmus_P3_0_: lwz 31,0(9)
_litmus_P3_1_: lwz 11,0(9)
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,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 posrr012 Allowed
Histogram (40 states)
1 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=1;
3 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
5 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=1;
4 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
2 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=1;
8 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
6 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; z=1;
6 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2;
18 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2;
10 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=1;
29 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2;
17 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2;
78 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2;
1 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2;
9 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=1;
57 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; z=1;
57 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; z=1;
31 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; z=1;
25 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=1;
91996 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=1;
77756 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=1;
209242:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2;
199692:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
95684 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; z=1;
192891:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; z=2;
992000:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2;
734431:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; z=1;
321880:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1693486:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2;
1602583:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2;
285065:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=1;
655109:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=1;
408690:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=1;
1288564:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; z=1;
2075255:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=1;
1195429:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; z=2;
1178264:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; z=1;
1469639:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=1;
764355:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=1;
467622:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (z=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated
Hash=2707402f3cf9f20b1f649906e5dcb239
Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR
Relax posrr012 No PosRR
Safe=Fre BCSyncdWW BCSyncdRW
Time posrr012 2.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/posrr013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
posrr013
"DpdR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR"
{0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r6=x;}
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(r2) ;
sync | li r3,1 | li r3,1 | xor r4,r3,r3 ;
li r3,1 | stw r3,0(r4) | stw r3,0(r4) | lwzx r5,r4,r6 ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0 /\ 3:r5=0)
Generated assembler
_litmus_P3_0_: lwz 27,0(11)
_litmus_P3_1_: lwz 29,0(11)
_litmus_P3_2_: xor 7,29,29
_litmus_P3_3_: lwzx 8,7,9
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 31,1
_litmus_P2_3_: stw 31,0(9)
_litmus_P1_0_: lwz 30,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: li 31,1
_litmus_P1_3_: stw 31,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 posrr013 Allowed
Histogram (21 states)
3 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=0;
12 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=0;
17 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; 3:r5=1;
28 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=1;
46 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=1;
48 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; 3:r5=1;
134167:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; 3:r5=0;
67979 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; 3:r5=1;
102258:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=0;
115807:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=0;
837588:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=1;
804769:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; 3:r5=1;
1415230:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=1;
1088887:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=0;
2982006:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=0;
2193113:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=1;
1331868:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=1;
135500:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=1;
1576894:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=1;
1897219:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=0;
1316561:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=0;
No
Witnesses
Positive: 0, Negative: 16000000
Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0 /\ 3:r5=0) is NOT validated
Hash=c740edf890395d3b09045a9e97a8f79e
Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR
Relax posrr013 No PosRR
Safe=Fre DpdR BCSyncdWW BCSyncdRW
Time posrr013 2.59
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 100000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 10
#endif
#ifndef N_EXE
#define N_EXE (64 < N ? 1 : 64 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread -maix64 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 64 */
GCCOPTS="-Wall -std=gnu99 -O -pthread -maix64"
LITMUSOPTS=
Wed Dec 23 13:40:33 NFT 2009