#master command line: ppcmaster -m 4000 -nagain 0 -host chianti.inria.fr:1111 -auto @all ####################### # Version information # ####################### #Model: #Path: . #URL: svn+ssh://secsvn@svn-sem.cl.cam.ac.uk/WeakMemory/ppc-abstract-machine #Repository Root: svn+ssh://secsvn@svn-sem.cl.cam.ac.uk #Repository UUID: 0227817e-5e02-0410-83b2-89653b220fac #Revision: 8411 #Node Kind: directory #Schedule: normal #Last Changed Author: ss726 #Last Changed Rev: 8397 #Last Changed Date: 2011-08-31 10:48:11 +0100 (Wed, 31 Aug 2011) # #Name: MachineDefUtils.lem #Revision: 8411 #Last Changed Author: so294 #Last Changed Rev: 8345 #Last Changed Date: 2011-08-05 12:52:50 +0100 (Fri, 05 Aug 2011) #Text Last Updated: 2011-08-08 10:55:55 +0100 (Mon, 08 Aug 2011) #Checksum: 093f06a9a327d1379cf23078896b7b72 # #Name: MachineDefFreshIds.lem #Revision: 8411 #Last Changed Author: pes20 #Last Changed Rev: 8251 #Last Changed Date: 2011-07-01 16:14:46 +0100 (Fri, 01 Jul 2011) #Text Last Updated: 2011-07-27 16:22:49 +0100 (Wed, 27 Jul 2011) #Checksum: 987ca7ba14acfe76c1ab8236371977f8 # #Name: MachineDefValue.lem #Revision: 8411 #Last Changed Author: so294 #Last Changed Rev: 8345 #Last Changed Date: 2011-08-05 12:52:50 +0100 (Fri, 05 Aug 2011) #Text Last Updated: 2011-08-08 10:55:55 +0100 (Mon, 08 Aug 2011) #Checksum: 3f0dc34931d5785c77ca202b8a0bcab1 # #Name: MachineDefTypes.lem #Revision: 8411 #Last Changed Author: so294 #Last Changed Rev: 8345 #Last Changed Date: 2011-08-05 12:52:50 +0100 (Fri, 05 Aug 2011) #Text Last Updated: 2011-08-08 10:55:55 +0100 (Mon, 08 Aug 2011) #Checksum: 3d40959b14b5ff94fcb4a13e1379aa85 # #Name: MachineDefInstructionSemantics.lem #Revision: 8412 #Last Changed Author: ss726 #Last Changed Rev: 8412 #Last Changed Date: 2011-09-15 14:03:19 +0100 (Thu, 15 Sep 2011) #Text Last Updated: 2011-09-15 12:34:39 +0100 (Thu, 15 Sep 2011) #Checksum: 6d820d871a8010494a69514bc274f5af # #Name: MachineDefStorageSubsystem.lem #Revision: 8411 #Last Changed Author: so294 #Last Changed Rev: 8345 #Last Changed Date: 2011-08-05 12:52:50 +0100 (Fri, 05 Aug 2011) #Text Last Updated: 2011-08-08 10:55:55 +0100 (Mon, 08 Aug 2011) #Checksum: c8480067b8ba12f5380ce0555c5ec977 # #Name: MachineDefThreadSubsystem.lem #Revision: 8411 #Last Changed Author: ss726 #Last Changed Rev: 8397 #Last Changed Date: 2011-08-31 10:48:11 +0100 (Wed, 31 Aug 2011) #Text Last Updated: 2011-08-30 14:53:24 +0100 (Tue, 30 Aug 2011) #Checksum: 2bf0a3b13315c2e3f7f218f9f7338915 # #Name: MachineDefSystem.lem #Revision: 8411 #Last Changed Author: pes20 #Last Changed Rev: 8327 #Last Changed Date: 2011-07-27 16:07:13 +0100 (Wed, 27 Jul 2011) #Text Last Updated: 2011-07-27 16:22:49 +0100 (Wed, 27 Jul 2011) #Checksum: ad42f8a98a3f80280c150024fecee268 # #M MachineDefTypes.lem #M MachineDefInstructionSemantics.lem #M MachineDefThreadSubsystem.lem #Lem run: #Thu Sep 15 17:07:04 BST 2011 # #Revision: 6 #Last Changed Author: ss726 #Last Changed Rev: 6 #Last Changed Date: 2011-05-12 15:02:21 +0200 (Thu, 12 May 2011) # #M src/version.ml #Build: #Thu May 19 11:29:12 CEST 2011 #-e # #-e ** Result for A000.litmus ** Test A000 Allowed States 3 0:r1=0; 1:r1=0; 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1) Hash=731b259b57382df5f9d906e0a8ec0dab Cycle=Rfe SyncdRW Rfe SyncdRW Relax A000 No Safe=ACSyncdRW Prefetch= Com=Rf Rf Orig=Rfe SyncdRW Rfe SyncdRW Observation A000 Never 0 3 status: 0 real: 0.05 user: 0.05 sys: 0.00 ** Result for A006.litmus ** Test A006 Allowed States 3 0:r1=0; 1:r1=0; 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1) Hash=ed1c512b6f38e2119bada8df32953c21 Cycle=Rfe SyncdRW Rfe LwSyncdRW Relax A006 No Safe=ACSyncdRW ACLwSyncdRW Prefetch= Com=Rf Rf Orig=Rfe LwSyncdRW Rfe SyncdRW Observation A006 Never 0 3 status: 0 real: 0.05 user: 0.04 sys: 0.00 ** Result for A067.litmus ** Test A067 Allowed States 3 0:r1=0; 1:r1=0; 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1) Hash=f41cfe96f8031533d08177efba625b88 Cycle=Rfe SyncdRW Rfe DpDatadW Relax A067 No Safe=ABCSyncdRW DpDatadW Prefetch= Com=Rf Rf Orig=DpDatadW Rfe SyncdRW Rfe Observation A067 Never 0 3 status: 0 real: 0.02 user: 0.01 sys: 0.00 ** Result for A061.litmus ** Test A061 Allowed States 3 0:r1=0; 1:r1=0; 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1) Hash=12e0c3979643f5433f4bd97649aa5f2d Cycle=Rfe SyncdRW Rfe DpAddrdW Relax A061 No Safe=ABCSyncdRW DpAddrdW Prefetch= Com=Rf Rf Orig=DpAddrdW Rfe SyncdRW Rfe Observation A061 Never 0 3 status: 0 real: 0.02 user: 0.02 sys: 0.00 ** Result for A069.litmus ** Test A069 Allowed States 3 0:r1=0; 1:r1=0; 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1) Hash=623693a2939e115f5989439152efa467 Cycle=Rfe SyncdRW Rfe DpCtrldW Relax A069 No Safe=ABCSyncdRW DpCtrldW Prefetch= Com=Rf Rf Orig=DpCtrldW Rfe SyncdRW Rfe Observation A069 Never 0 3 status: 0 real: 0.02 user: 0.02 sys: 0.00 ** Result for A065.litmus ** Test A065 Allowed States 3 0:r1=0; 0:r4=0; 1:r1=0; 0:r1=0; 0:r4=0; 1:r1=1; 0:r1=1; 0:r4=0; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1) Hash=2c4e90d582f91e794b1ea0e37c065fdc Cycle=Rfe SyncdRW Rfe DpAddrdR Fri Relax A065 No Safe=ABCSyncdRW [DpAddrdR,Fri] Prefetch= Com=Rf Rf Orig=DpAddrdR Fri Rfe SyncdRW Rfe Observation A065 Never 0 3 status: 0 real: 0.04 user: 0.04 sys: 0.00 ** Result for A090.litmus ** Test A090 Allowed States 3 0:r1=0; 1:r1=0; 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1) Hash=70ac7132cbaacd38cf3b50a32bc97f11 Cycle=Rfe LwSyncdRW Rfe LwSyncdRW Relax A090 No Safe=ACLwSyncdRW Prefetch= Com=Rf Rf Orig=Rfe LwSyncdRW Rfe LwSyncdRW Observation A090 Never 0 3 status: 0 real: 0.04 user: 0.04 sys: 0.00 ** Result for A131.litmus ** Test A131 Allowed States 3 1:r1=0; 1:r4=0; 1:r1=0; 1:r4=1; 1:r1=1; 1:r4=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r4=0) Hash=abe769d43585052eb6bd1199546b3603 Cycle=Rfe DpAddrdR Fre SyncdWW Relax A131 No Safe=Fre BCSyncdWW DpAddrdR Prefetch=1:x=T Com=Rf Fr Orig=SyncdWW Rfe DpAddrdR Fre Observation A131 Never 0 3 status: 0 real: 0.03 user: 0.03 sys: 0.00 ** Result for A135.litmus ** Test A135 Allowed States 3 1:r1=0; 1:r3=0; 1:r1=0; 1:r3=1; 1:r1=1; 1:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r3=0) Hash=c707ee488a6fe9cdd4f7e5c2c4ab0723 Cycle=Rfe DpCtrlIsyncdR Fre SyncdWW Relax A135 No Safe=Fre BCSyncdWW DpCtrlIsyncdR Prefetch=1:x=T Com=Rf Fr Orig=SyncdWW Rfe DpCtrlIsyncdR Fre Observation A135 Never 0 3 status: 0 real: 0.03 user: 0.03 sys: 0.00 ** Result for A077.litmus ** Test A077 Allowed States 3 1:r1=0; 1:r3=0; 1:r1=0; 1:r3=1; 1:r1=1; 1:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r3=0) Hash=6fa2fc8a03a8948f9262ae5fd1e47a19 Cycle=Rfe SyncdRR Fre SyncdWW Relax A077 No Safe=ACSyncdRR Fre SyncdWW Prefetch=1:x=T Com=Rf Fr Orig=Fre SyncdWW Rfe SyncdRR Observation A077 Never 0 3 status: 0 real: 0.07 user: 0.07 sys: 0.00 ** Result for A081.litmus ** Test A081 Allowed States 3 1:r1=0; 1:r3=0; 1:r1=0; 1:r3=1; 1:r1=1; 1:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r3=0) Hash=f2fb4f705b4ae377d74d86f86bde91ee Cycle=Rfe SyncdRR Fre LwSyncdWW Relax A081 No Safe=ACSyncdRR Fre LwSyncdWW Prefetch=1:x=T Com=Rf Fr Orig=Fre LwSyncdWW Rfe SyncdRR Observation A081 Never 0 3 status: 0 real: 0.08 user: 0.07 sys: 0.00 ** Result for A154.litmus ** Test A154 Allowed States 3 1:r1=0; [x]=1; 1:r1=0; [x]=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1) Hash=af9998d4ff45b06d631d9a94eefc4e67 Cycle=Rfe DpDatadW Wse SyncdWW Relax A154 No Safe=Wse BCSyncdWW DpDatadW Prefetch=0:x=F,1:x=W Com=Rf Ws Orig=SyncdWW Rfe DpDatadW Wse Observation A154 Never 0 3 status: 0 real: 0.04 user: 0.04 sys: 0.00 ** Result for A156.litmus ** Test A156 Allowed States 3 1:r1=0; [x]=1; 1:r1=0; [x]=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1) Hash=38ce13154a7e8ca56fa82e0689c225f9 Cycle=Rfe DpCtrldW Wse SyncdWW Relax A156 No Safe=Wse BCSyncdWW DpCtrldW Prefetch=0:x=F,1:x=W Com=Rf Ws Orig=SyncdWW Rfe DpCtrldW Wse Observation A156 Never 0 3 status: 0 real: 0.05 user: 0.04 sys: 0.00 ** Result for A152.litmus ** Test A152 Allowed States 3 1:r1=0; [x]=1; 1:r1=0; [x]=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1) Hash=262d40103ab036ada7c4d5ede4cb5840 Cycle=Rfe DpAddrdW Wse SyncdWW Relax A152 No Safe=Wse BCSyncdWW DpAddrdW Prefetch=0:x=F,1:x=W Com=Rf Ws Orig=SyncdWW Rfe DpAddrdW Wse Observation A152 Never 0 3 status: 0 real: 0.05 user: 0.05 sys: 0.00 ** Result for A063.litmus ** Test A063 Allowed States 4 0:r1=0; 1:r1=0; [y]=2; 0:r1=0; 1:r1=1; [y]=2; 0:r1=0; 1:r1=2; [y]=2; 0:r1=1; 1:r1=0; [y]=2; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 1:r1=2) Hash=a06e69510f90a49c5796fa69e99e0f83 Cycle=Rfe SyncdRW Rfe DpAddrdW Wsi Relax A063 No Safe=ABCSyncdRW [DpAddrdW,Wsi] Prefetch= Com=Rf Rf Orig=DpAddrdW Wsi Rfe SyncdRW Rfe Observation A063 Never 0 4 status: 0 real: 0.13 user: 0.13 sys: 0.00 ** Result for A127.litmus ** Test A127 Allowed States 3 1:r1=0; 1:r3=0; 1:r1=0; 1:r3=1; 1:r1=1; 1:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r3=0) Hash=99037ea093e4b022e3b61a8c09253659 Cycle=Rfe LwSyncdRR Fre SyncdWW Relax A127 No Safe=Fre BCSyncdWW LwSyncdRR Prefetch=1:x=T Com=Rf Fr Orig=SyncdWW Rfe LwSyncdRR Fre Observation A127 Never 0 3 status: 0 real: 0.13 user: 0.13 sys: 0.00 ** Result for A018.litmus ** Test A018 Allowed States 3 1:r1=0; [x]=1; 1:r1=0; [x]=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1) Hash=3bacaa46622528b0ef100acb0d326a4f Cycle=Rfe SyncdRW Wse SyncdWW Relax A018 No Safe=ACSyncdRW Wse SyncdWW Prefetch=0:x=F,1:x=W Com=Rf Ws Orig=Wse SyncdWW Rfe SyncdRW Observation A018 Never 0 3 status: 0 real: 0.21 user: 0.21 sys: 0.00 ** Result for A111.litmus ** Test A111 Allowed States 3 0:r3=0; 1:r3=1; 0:r3=1; 1:r3=0; 0:r3=1; 1:r3=1; No (allowed not found) Condition exists (0:r3=0 /\ 1:r3=0) Hash=5db67b28ae44dfb0497cda13c245c4e4 Cycle=Fre SyncdWR Fre SyncdWR Relax A111 No Safe=Fre SyncdWR Prefetch=0:y=T,1:x=T Com=Fr Fr Orig=SyncdWR Fre SyncdWR Fre Observation A111 Never 0 3 status: 0 real: 0.16 user: 0.16 sys: 0.00 ** Result for A024.litmus ** Test A024 Allowed States 3 1:r1=0; [x]=1; 1:r1=0; [x]=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1) Hash=e61df4fe295080500f7ed8b320f8afee Cycle=Rfe SyncdRW Wse LwSyncdWW Relax A024 No Safe=ACSyncdRW Wse LwSyncdWW Prefetch=0:x=F,1:x=W Com=Rf Ws Orig=Wse LwSyncdWW Rfe SyncdRW Observation A024 Never 0 3 status: 0 real: 0.23 user: 0.23 sys: 0.00 ** Result for A099.litmus ** Test A099 Allowed States 3 1:r1=0; [x]=1; 1:r1=0; [x]=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1) Hash=f2059b3317352037db1a67aebcfbd257 Cycle=Rfe LwSyncdRW Wse SyncdWW Relax A099 No Safe=ACLwSyncdRW Wse SyncdWW Prefetch=0:x=F,1:x=W Com=Rf Ws Orig=Wse SyncdWW Rfe LwSyncdRW Observation A099 Never 0 3 status: 0 real: 0.22 user: 0.21 sys: 0.00 ** Result for A103.litmus ** Test A103 Allowed States 3 1:r1=0; [x]=1; 1:r1=0; [x]=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1) Hash=4d1c1648955365c08b4c97b22a8d5408 Cycle=Rfe LwSyncdRW Wse LwSyncdWW Relax A103 No Safe=ACLwSyncdRW Wse LwSyncdWW Prefetch=0:x=F,1:x=W Com=Rf Ws Orig=Wse LwSyncdWW Rfe LwSyncdRW Observation A103 Never 0 3 status: 0 real: 0.22 user: 0.22 sys: 0.00 ** Result for A118.litmus ** Test A118 Allowed States 3 1:r3=0; [y]=1; 1:r3=1; [y]=1; 1:r3=1; [y]=2; No (allowed not found) Condition exists ([y]=2 /\ 1:r3=0) Hash=7da20a2ab953c9d18488d3f4e7841bb2 Cycle=Fre SyncdWW Wse SyncdWR Relax A118 No Safe=Fre Wse SyncdWW SyncdWR Prefetch=0:y=W,1:y=F,1:x=T Com=Ws Fr Orig=SyncdWW Wse SyncdWR Fre Observation A118 Never 0 3 status: 0 real: 0.46 user: 0.45 sys: 0.00 ** Result for A121.litmus ** Test A121 Allowed States 4 1:r3=0; [y]=1; 1:r3=0; [y]=2; 1:r3=1; [y]=1; 1:r3=1; [y]=2; Ok Condition exists ([y]=2 /\ 1:r3=0) Hash=178cdf8fa414f9851e5cbee2c97136b0 Cycle=Fre LwSyncdWW Wse SyncdWR Relax A121 Ok Safe=Fre Wse SyncdWR LwSyncdWW Prefetch=0:y=W,1:y=F,1:x=T Com=Ws Fr Orig=LwSyncdWW Wse SyncdWR Fre Observation A121 Sometimes 1 3 status: 0 real: 0.52 user: 0.52 sys: 0.00 ** Result for A045.litmus ** Test A045 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=ce53b75865f5d12c7fed8b9677ad6694 Cycle=Rfe SyncdRW Rfe DpCtrlIsyncdR Fre Relax A045 No Safe=ABCSyncdRW Fre DpCtrlIsyncdR Prefetch=0:y=T,1:y=T Com=Fr Rf Rf Orig=DpCtrlIsyncdR Fre Rfe SyncdRW Rfe Observation A045 Never 0 7 status: 0 real: 0.60 user: 0.59 sys: 0.00 ** Result for A044.litmus ** Test A044 Allowed States 7 0:r1=0; 0:r4=0; 2:r1=0; 0:r1=0; 0:r4=0; 2:r1=1; 0:r1=0; 0:r4=1; 2:r1=0; 0:r1=0; 0:r4=1; 2:r1=1; 0:r1=1; 0:r4=0; 2:r1=0; 0:r1=1; 0:r4=1; 2:r1=0; 0:r1=1; 0:r4=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1) Hash=77b412df18b43b1217441576aeb493ca Cycle=Rfe SyncdRW Rfe DpAddrdR Fre Relax A044 No Safe=ABCSyncdRW Fre DpAddrdR Prefetch=0:y=T,1:y=T Com=Fr Rf Rf Orig=DpAddrdR Fre Rfe SyncdRW Rfe Observation A044 Never 0 7 status: 0 real: 0.60 user: 0.60 sys: 0.00 ** Result for A139.litmus ** Test A139 Allowed States 3 [x]=1; [y]=1; [x]=1; [y]=2; [x]=2; [y]=1; No (allowed not found) Condition exists ([x]=2 /\ [y]=2) Hash=b13e0c20b3a95ec28cc7a23efa1563b6 Cycle=Wse SyncdWW Wse SyncdWW Relax A139 No Safe=Wse SyncdWW Prefetch=0:x=F,0:y=W,1:y=F,1:x=W Com=Ws Ws Orig=SyncdWW Wse SyncdWW Wse Observation A139 Never 0 3 status: 0 real: 1.30 user: 1.29 sys: 0.00 ** Result for A142.litmus ** Test A142 Allowed States 3 [x]=1; [y]=1; [x]=1; [y]=2; [x]=2; [y]=1; No (allowed not found) Condition exists ([x]=2 /\ [y]=2) Hash=8448ba0b52ce20d00ef5f71a9150ac5a Cycle=Wse SyncdWW Wse LwSyncdWW Relax A142 No Safe=Wse SyncdWW LwSyncdWW Prefetch=0:x=F,0:y=W,1:y=F,1:x=W Com=Ws Ws Orig=LwSyncdWW Wse SyncdWW Wse Observation A142 Never 0 3 status: 0 real: 1.48 user: 1.48 sys: 0.00 ** Result for A147.litmus ** Test A147 Allowed States 3 [x]=1; [y]=1; [x]=1; [y]=2; [x]=2; [y]=1; No (allowed not found) Condition exists ([x]=2 /\ [y]=2) Hash=829af8195a1482485057a881cab011a8 Cycle=Wse LwSyncdWW Wse LwSyncdWW Relax A147 No Safe=Wse LwSyncdWW Prefetch=0:x=F,0:y=W,1:y=F,1:x=W Com=Ws Ws Orig=LwSyncdWW Wse LwSyncdWW Wse Observation A147 Never 0 3 status: 0 real: 1.55 user: 1.55 sys: 0.00 ** Result for A047.litmus ** Test A047 Allowed States 9 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=0; 2:r1=2; [y]=1; 0:r1=0; 2:r1=2; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=2; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=2) Hash=6b47301dd2ed74e5b7d71a0c18a79309 Cycle=Rfe SyncdRW Rfe DpDatadW Wse Relax A047 No Safe=ABCSyncdRW Wse DpDatadW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpDatadW Wse Rfe SyncdRW Rfe Observation A047 Never 0 9 status: 0 real: 2.08 user: 2.08 sys: 0.00 ** Result for A048.litmus ** Test A048 Allowed States 9 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=0; 2:r1=2; [y]=1; 0:r1=0; 2:r1=2; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=2; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=2) Hash=03a09f22ddbd6af7fb2d89273b079d23 Cycle=Rfe SyncdRW Rfe DpCtrldW Wse Relax A048 No Safe=ABCSyncdRW Wse DpCtrldW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpCtrldW Wse Rfe SyncdRW Rfe Observation A048 Never 0 9 status: 0 real: 2.23 user: 2.23 sys: 0.00 ** Result for A046.litmus ** Test A046 Allowed States 9 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=0; 2:r1=2; [y]=1; 0:r1=0; 2:r1=2; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=2; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=2) Hash=dd5ef9c5a288f568730fa7e74b172310 Cycle=Rfe SyncdRW Rfe DpAddrdW Wse Relax A046 No Safe=ABCSyncdRW Wse DpAddrdW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpAddrdW Wse Rfe SyncdRW Rfe Observation A046 Never 0 9 status: 0 real: 2.34 user: 2.33 sys: 0.01 ** Result for A011.litmus ** Test A011 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=3149b48dab3ade0c05a8191aab581c51 Cycle=Rfe SyncdRW Rfe SyncdRR Fre Relax A011 No Safe=ACSyncdRW ACSyncdRR Fre Prefetch=0:y=T,1:y=T Com=Fr Rf Rf Orig=Rfe SyncdRR Fre Rfe SyncdRW Observation A011 Never 0 7 status: 0 real: 4.34 user: 4.32 sys: 0.01 ** Result for A071.litmus ** Test A071 Allowed States 7 0:r1=0; 1:r1=0; 1:r3=0; 0:r1=0; 1:r1=0; 1:r3=1; 0:r1=0; 1:r1=1; 1:r3=0; 0:r1=0; 1:r1=1; 1:r3=1; 0:r1=1; 1:r1=0; 1:r3=0; 0:r1=1; 1:r1=0; 1:r3=1; 0:r1=1; 1:r1=1; 1:r3=1; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 1:r3=0) Hash=ddac41d06441eb87ef18576dea412a93 Cycle=Rfe SyncdRR Fre Rfe LwSyncdRW Relax A071 No Safe=ACSyncdRR ACLwSyncdRW Fre Prefetch=1:x=T,2:x=T Com=Rf Fr Rf Orig=Fre Rfe LwSyncdRW Rfe SyncdRR Observation A071 Never 0 7 status: 0 real: 5.47 user: 5.46 sys: 0.01 ** Result for A043.litmus ** Test A043 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=b03cbe60214abde5539633cf0f7f04c2 Cycle=Rfe SyncdRW Rfe LwSyncdRR Fre Relax A043 No Safe=ABCSyncdRW Fre LwSyncdRR Prefetch=0:y=T,1:y=T Com=Fr Rf Rf Orig=LwSyncdRR Fre Rfe SyncdRW Rfe Observation A043 Never 0 7 status: 0 real: 8.42 user: 8.41 sys: 0.01 ** Result for A074.litmus ** Test A074 Allowed States 7 0:r3=0; 2:r1=0; 2:r3=0; 0:r3=0; 2:r1=0; 2:r3=1; 0:r3=0; 2:r1=1; 2:r3=1; 0:r3=1; 2:r1=0; 2:r3=0; 0:r3=1; 2:r1=0; 2:r3=1; 0:r3=1; 2:r1=1; 2:r3=0; 0:r3=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Hash=925286d16494ebf5ec288ca398714a02 Cycle=Rfe SyncdRR Fre SyncdWR Fre Relax A074 No Safe=ACSyncdRR Fre SyncdWR Prefetch=0:y=T,1:y=T,2:x=T Com=Fr Rf Fr Orig=Fre SyncdWR Fre Rfe SyncdRR Observation A074 Never 0 7 status: 0 real: 9.26 user: 9.24 sys: 0.02 ** Result for A003.litmus ** Test A003 Allowed States 9 0:r1=0; 1:r1=0; [x]=1; 0:r1=0; 1:r1=0; [x]=2; 0:r1=0; 1:r1=1; [x]=1; 0:r1=0; 1:r1=1; [x]=2; 0:r1=1; 1:r1=0; [x]=1; 0:r1=1; 1:r1=0; [x]=2; 0:r1=2; 1:r1=0; [x]=1; 0:r1=2; 1:r1=0; [x]=2; 0:r1=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 0:r1=2 /\ 1:r1=1) Hash=3b9c0a72f2426dfaaac8c7da27093b5c Cycle=Rfe SyncdRW Rfe SyncdRW Wse Relax A003 No Safe=ACSyncdRW Wse Prefetch=1:x=W,2:x=F Com=Rf Ws Rf Orig=Wse Rfe SyncdRW Rfe SyncdRW Observation A003 Never 0 9 status: 0 real: 24.21 user: 24.19 sys: 0.02 ** Result for A008.litmus ** Test A008 Allowed States 9 0:r1=0; 1:r1=0; [x]=1; 0:r1=0; 1:r1=0; [x]=2; 0:r1=0; 1:r1=1; [x]=1; 0:r1=0; 1:r1=1; [x]=2; 0:r1=1; 1:r1=0; [x]=1; 0:r1=1; 1:r1=0; [x]=2; 0:r1=2; 1:r1=0; [x]=1; 0:r1=2; 1:r1=0; [x]=2; 0:r1=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 0:r1=2 /\ 1:r1=1) Hash=d3b44e37fdc2b7c592683df843d536ea Cycle=Rfe SyncdRW Wse Rfe LwSyncdRW Relax A008 No Safe=ACSyncdRW ACLwSyncdRW Wse Prefetch=1:x=W,2:x=F Com=Rf Ws Rf Orig=Wse Rfe LwSyncdRW Rfe SyncdRW Observation A008 Never 0 9 status: 0 real: 30.18 user: 30.15 sys: 0.03 ** Result for A013.litmus ** Test A013 Allowed States 9 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=0; 2:r1=2; [y]=1; 0:r1=0; 2:r1=2; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=2; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=2) Hash=6f16f03feb0de899ad300292bc471411 Cycle=Rfe SyncdRW Rfe LwSyncdRW Wse Relax A013 No Safe=ACSyncdRW ACLwSyncdRW Wse Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=Rfe LwSyncdRW Wse Rfe SyncdRW Observation A013 Never 0 9 status: 0 real: 31.52 user: 31.50 sys: 0.02 ** Result for A075.litmus ** Test A075 Allowed States 9 2:r1=0; 2:r3=0; [y]=1; 2:r1=0; 2:r3=0; [y]=2; 2:r1=0; 2:r3=1; [y]=1; 2:r1=0; 2:r3=1; [y]=2; 2:r1=1; 2:r3=1; [y]=1; 2:r1=1; 2:r3=1; [y]=2; 2:r1=2; 2:r3=0; [y]=1; 2:r1=2; 2:r3=1; [y]=1; 2:r1=2; 2:r3=1; [y]=2; No (allowed not found) Condition exists ([y]=2 /\ 2:r1=2 /\ 2:r3=0) Hash=05eb02a8d4be19d3d1ec3a86128a016d Cycle=Rfe SyncdRR Fre SyncdWW Wse Relax A075 No Safe=ACSyncdRR Fre Wse SyncdWW Prefetch=0:y=W,1:y=F,2:x=T Com=Ws Rf Fr Orig=Fre SyncdWW Wse Rfe SyncdRR Observation A075 Never 0 9 status: 0 real: 34.43 user: 34.39 sys: 0.03 ** Result for A092.litmus ** Test A092 Allowed States 9 0:r1=0; 1:r1=0; [x]=1; 0:r1=0; 1:r1=0; [x]=2; 0:r1=0; 1:r1=1; [x]=1; 0:r1=0; 1:r1=1; [x]=2; 0:r1=1; 1:r1=0; [x]=1; 0:r1=1; 1:r1=0; [x]=2; 0:r1=2; 1:r1=0; [x]=1; 0:r1=2; 1:r1=0; [x]=2; 0:r1=2; 1:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 0:r1=2 /\ 1:r1=1) Hash=ee4e67f432fce6a5ac60d449c23ff188 Cycle=Rfe LwSyncdRW Rfe LwSyncdRW Wse Relax A092 No Safe=ACLwSyncdRW Wse Prefetch=1:x=W,2:x=F Com=Rf Ws Rf Orig=Wse Rfe LwSyncdRW Rfe LwSyncdRW Observation A092 Never 0 9 status: 0 real: 37.09 user: 37.05 sys: 0.03 ** Result for A051.litmus ** Test A051 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=0c074649ef22030402ff9646a0437f4a Cycle=Rfe SyncdRW Rfe DpCtrlIsyncdR Fre SyncdWW Relax A051 No Safe=ABCSyncdRW Fre SyncdWW DpCtrlIsyncdR Prefetch=0:y=T Com=Fr Rf Rf Orig=DpCtrlIsyncdR Fre SyncdWW Rfe SyncdRW Rfe Observation A051 Never 0 7 status: 0 real: 54.35 user: 54.32 sys: 0.03 ** Result for A034.litmus ** Test A034 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=291750bec5ec3ca0010417962ba9c149 Cycle=Rfe SyncdRW Rfe SyncdRW Rfe DpDatadW Relax A034 No Safe=ACSyncdRW ABCSyncdRW DpDatadW Prefetch= Com=Rf Rf Rf Orig=Rfe SyncdRW Rfe DpDatadW Rfe SyncdRW Observation A034 Never 0 7 status: 0 real: 56.55 user: 56.49 sys: 0.05 ** Result for A036.litmus ** Test A036 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=f9ce1acce75b5217763cdd5d853564e0 Cycle=Rfe SyncdRW Rfe SyncdRW Rfe DpCtrldW Relax A036 No Safe=ACSyncdRW ABCSyncdRW DpCtrldW Prefetch= Com=Rf Rf Rf Orig=Rfe SyncdRW Rfe DpCtrldW Rfe SyncdRW Observation A036 Never 0 7 status: 0 real: 58.17 user: 58.12 sys: 0.04 ** Result for A012.litmus ** Test A012 Allowed States 7 0:r3=0; 2:r1=0; [x]=1; 0:r3=0; 2:r1=0; [x]=2; 0:r3=0; 2:r1=1; [x]=1; 0:r3=1; 2:r1=0; [x]=1; 0:r3=1; 2:r1=0; [x]=2; 0:r3=1; 2:r1=1; [x]=1; 0:r3=1; 2:r1=1; [x]=2; No (allowed not found) Condition exists ([x]=2 /\ 0:r3=0 /\ 2:r1=1) Hash=24e207cbad5b0f5c7ad0edf8140e6fd1 Cycle=Rfe SyncdRW Wse SyncdWR Fre Relax A012 No Safe=ACSyncdRW Fre Wse SyncdWR Prefetch=0:x=F,0:y=T,1:y=T,2:x=W Com=Fr Rf Ws Orig=Wse SyncdWR Fre Rfe SyncdRW Observation A012 Never 0 7 status: 0 real: 58.43 user: 58.38 sys: 0.05 ** Result for A076.litmus ** Test A076 Allowed States 10 2:r1=0; 2:r3=0; [y]=1; 2:r1=0; 2:r3=0; [y]=2; 2:r1=0; 2:r3=1; [y]=1; 2:r1=0; 2:r3=1; [y]=2; 2:r1=1; 2:r3=1; [y]=1; 2:r1=1; 2:r3=1; [y]=2; 2:r1=2; 2:r3=0; [y]=1; 2:r1=2; 2:r3=0; [y]=2; 2:r1=2; 2:r3=1; [y]=1; 2:r1=2; 2:r3=1; [y]=2; Ok Condition exists ([y]=2 /\ 2:r1=2 /\ 2:r3=0) Hash=839d5d584082047b5e95d4f7663c3489 Cycle=Rfe SyncdRR Fre LwSyncdWW Wse Relax A076 Ok Safe=ACSyncdRR Fre Wse LwSyncdWW Prefetch=0:y=W,1:y=F,2:x=T Com=Ws Rf Fr Orig=Fre LwSyncdWW Wse Rfe SyncdRR Observation A076 Sometimes 1 9 status: 0 real: 59.47 user: 59.40 sys: 0.06 ** Result for A028.litmus ** Test A028 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=596ea5d9c903b1b5dc79ba66f9abaeaa Cycle=Rfe SyncdRW Rfe SyncdRW Rfe DpAddrdW Relax A028 No Safe=ACSyncdRW ABCSyncdRW DpAddrdW Prefetch= Com=Rf Rf Rf Orig=Rfe SyncdRW Rfe DpAddrdW Rfe SyncdRW Observation A028 Never 0 7 status: 0 real: 60.09 user: 60.03 sys: 0.04 ** Result for A050.litmus ** Test A050 Allowed States 7 0:r1=0; 0:r4=0; 2:r1=0; 0:r1=0; 0:r4=0; 2:r1=1; 0:r1=0; 0:r4=1; 2:r1=0; 0:r1=0; 0:r4=1; 2:r1=1; 0:r1=1; 0:r4=0; 2:r1=0; 0:r1=1; 0:r4=1; 2:r1=0; 0:r1=1; 0:r4=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1) Hash=e6872c41a85243ae41df6b460263377a Cycle=Rfe SyncdRW Rfe DpAddrdR Fre SyncdWW Relax A050 No Safe=ABCSyncdRW Fre SyncdWW DpAddrdR Prefetch=0:y=T Com=Fr Rf Rf Orig=DpAddrdR Fre SyncdWW Rfe SyncdRW Rfe Observation A050 Never 0 7 status: 0 real: 60.77 user: 60.71 sys: 0.06 ** Result for A088.litmus ** Test A088 Allowed States 7 1:r1=0; 2:r1=0; 2:r3=0; 1:r1=0; 2:r1=0; 2:r3=1; 1:r1=0; 2:r1=1; 2:r3=0; 1:r1=0; 2:r1=1; 2:r3=1; 1:r1=1; 2:r1=0; 2:r3=0; 1:r1=1; 2:r1=0; 2:r3=1; 1:r1=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Hash=e158d5d8489375088b1366132f69e984 Cycle=Rfe SyncdRR Fre SyncdWW Rfe DpDatadW Relax A088 No Safe=ACSyncdRR Fre BCSyncdWW DpDatadW Prefetch=2:x=T Com=Rf Rf Fr Orig=Fre SyncdWW Rfe DpDatadW Rfe SyncdRR Observation A088 Never 0 7 status: 0 real: 62.86 user: 62.81 sys: 0.04 ** Result for A089.litmus ** Test A089 Allowed States 7 1:r1=0; 2:r1=0; 2:r3=0; 1:r1=0; 2:r1=0; 2:r3=1; 1:r1=0; 2:r1=1; 2:r3=0; 1:r1=0; 2:r1=1; 2:r3=1; 1:r1=1; 2:r1=0; 2:r3=0; 1:r1=1; 2:r1=0; 2:r3=1; 1:r1=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Hash=bc223f9c707b0f8861e84bc635283402 Cycle=Rfe SyncdRR Fre SyncdWW Rfe DpCtrldW Relax A089 No Safe=ACSyncdRR Fre BCSyncdWW DpCtrldW Prefetch=2:x=T Com=Rf Rf Fr Orig=Fre SyncdWW Rfe DpCtrldW Rfe SyncdRR Observation A089 Never 0 7 status: 0 real: 64.79 user: 64.75 sys: 0.04 ** Result for A085.litmus ** Test A085 Allowed States 7 1:r1=0; 2:r1=0; 2:r3=0; 1:r1=0; 2:r1=0; 2:r3=1; 1:r1=0; 2:r1=1; 2:r3=0; 1:r1=0; 2:r1=1; 2:r3=1; 1:r1=1; 2:r1=0; 2:r3=0; 1:r1=1; 2:r1=0; 2:r3=1; 1:r1=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Hash=e42b358270b2a64ee8be047dc961070c Cycle=Rfe SyncdRR Fre SyncdWW Rfe DpAddrdW Relax A085 No Safe=ACSyncdRR Fre BCSyncdWW DpAddrdW Prefetch=2:x=T Com=Rf Rf Fr Orig=Fre SyncdWW Rfe DpAddrdW Rfe SyncdRR Observation A085 Never 0 7 status: 0 real: 67.05 user: 66.99 sys: 0.05 ** Result for A041.litmus ** Test A041 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=4ce5f2affbadc04594a16bcdf2300fe8 Cycle=Rfe SyncdRW Rfe DpDatadW Rfe LwSyncdRW Relax A041 No Safe=ABCSyncdRW ACLwSyncdRW DpDatadW Prefetch= Com=Rf Rf Rf Orig=DpDatadW Rfe LwSyncdRW Rfe SyncdRW Rfe Observation A041 Never 0 7 status: 0 real: 68.88 user: 68.82 sys: 0.04 ** Result for A068.litmus ** Test A068 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=40ff61a77cb4420d71f1701af8d193b3 Cycle=Rfe SyncdRW Rfe LwSyncdRW Rfe DpDatadW Relax A068 No Safe=ABCSyncdRW BCLwSyncdRW DpDatadW Prefetch= Com=Rf Rf Rf Orig=LwSyncdRW Rfe DpDatadW Rfe SyncdRW Rfe Observation A068 Never 0 7 status: 0 real: 68.93 user: 68.88 sys: 0.04 ** Result for A032.litmus ** Test A032 Allowed States 7 0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1) Hash=964dd7a675edb7a28b225b10ec88ec26 Cycle=Rfe SyncdRW Rfe SyncdRW Rfe DpAddrdR Fri Relax A032 No Safe=ACSyncdRW ABCSyncdRW [DpAddrdR,Fri] Prefetch= Com=Rf Rf Rf Orig=Rfe SyncdRW Rfe DpAddrdR Fri Rfe SyncdRW Observation A032 Never 0 7 status: 0 real: 70.48 user: 70.42 sys: 0.05 ** Result for A070.litmus ** Test A070 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=b87e2c737fc93d3dd4e86060a5298bd9 Cycle=Rfe SyncdRW Rfe LwSyncdRW Rfe DpCtrldW Relax A070 No Safe=ABCSyncdRW BCLwSyncdRW DpCtrldW Prefetch= Com=Rf Rf Rf Orig=LwSyncdRW Rfe DpCtrldW Rfe SyncdRW Rfe Observation A070 Never 0 7 status: 0 real: 71.08 user: 71.01 sys: 0.05 ** Result for A042.litmus ** Test A042 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=95fdd4446a43f5a720a1aff94603bc50 Cycle=Rfe SyncdRW Rfe DpCtrldW Rfe LwSyncdRW Relax A042 No Safe=ABCSyncdRW ACLwSyncdRW DpCtrldW Prefetch= Com=Rf Rf Rf Orig=DpCtrldW Rfe LwSyncdRW Rfe SyncdRW Rfe Observation A042 Never 0 7 status: 0 real: 71.27 user: 71.20 sys: 0.05 ** Result for A095.litmus ** Test A095 Allowed States 8 0:r3=0; 2:r1=0; [x]=1; 0:r3=0; 2:r1=0; [x]=2; 0:r3=0; 2:r1=1; [x]=1; 0:r3=0; 2:r1=1; [x]=2; 0:r3=1; 2:r1=0; [x]=1; 0:r3=1; 2:r1=0; [x]=2; 0:r3=1; 2:r1=1; [x]=1; 0:r3=1; 2:r1=1; [x]=2; Ok Condition exists ([x]=2 /\ 0:r3=0 /\ 2:r1=1) Hash=53ab4e36ca9bb350a797b2f120cf481f Cycle=Rfe LwSyncdRW Wse SyncdWR Fre Relax A095 Ok Safe=ACLwSyncdRW Fre Wse SyncdWR Prefetch=0:x=F,0:y=T,1:y=T,2:x=W Com=Fr Rf Ws Orig=Wse SyncdWR Fre Rfe LwSyncdRW Observation A095 Sometimes 1 7 status: 0 real: 72.04 user: 71.98 sys: 0.05 ** Result for A138.litmus ** Test A138 Allowed States 7 1:r1=0; 2:r1=0; 2:r3=0; 1:r1=0; 2:r1=0; 2:r3=1; 1:r1=0; 2:r1=1; 2:r3=0; 1:r1=0; 2:r1=1; 2:r3=1; 1:r1=1; 2:r1=0; 2:r3=0; 1:r1=1; 2:r1=0; 2:r3=1; 1:r1=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Hash=2345e543e884886cadb8dcd1ed477ab9 Cycle=Rfe LwSyncdRW Rfe DpCtrlIsyncdR Fre SyncdWW Relax A138 No Safe=Fre BCSyncdWW BCLwSyncdRW DpCtrlIsyncdR Prefetch=2:x=T Com=Rf Rf Fr Orig=SyncdWW Rfe LwSyncdRW Rfe DpCtrlIsyncdR Fre Observation A138 Never 0 7 status: 0 real: 72.65 user: 72.61 sys: 0.04 ** Result for A062.litmus ** Test A062 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=17a75b1b5e4c05c20c19297442b516a7 Cycle=Rfe SyncdRW Rfe LwSyncdRW Rfe DpAddrdW Relax A062 No Safe=ABCSyncdRW BCLwSyncdRW DpAddrdW Prefetch= Com=Rf Rf Rf Orig=LwSyncdRW Rfe DpAddrdW Rfe SyncdRW Rfe Observation A062 Never 0 7 status: 0 real: 73.76 user: 73.71 sys: 0.04 ** Result for A038.litmus ** Test A038 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=89f42e1666fd3aff514ee175b6516096 Cycle=Rfe SyncdRW Rfe DpAddrdW Rfe LwSyncdRW Relax A038 No Safe=ABCSyncdRW ACLwSyncdRW DpAddrdW Prefetch= Com=Rf Rf Rf Orig=DpAddrdW Rfe LwSyncdRW Rfe SyncdRW Rfe Observation A038 Never 0 7 status: 0 real: 74.61 user: 74.53 sys: 0.07 ** Result for A087.litmus ** Test A087 Allowed States 7 1:r1=0; 1:r4=0; 2:r1=0; 2:r3=0; 1:r1=0; 1:r4=0; 2:r1=0; 2:r3=1; 1:r1=0; 1:r4=0; 2:r1=1; 2:r3=0; 1:r1=0; 1:r4=0; 2:r1=1; 2:r3=1; 1:r1=1; 1:r4=0; 2:r1=0; 2:r3=0; 1:r1=1; 1:r4=0; 2:r1=0; 2:r3=1; 1:r1=1; 1:r4=0; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r4=0 /\ 2:r1=1 /\ 2:r3=0) Hash=faaa7843511388adf97297fc82baf35d Cycle=Rfe SyncdRR Fre SyncdWW Rfe DpAddrdR Fri Relax A087 No Safe=ACSyncdRR Fre BCSyncdWW [DpAddrdR,Fri] Prefetch=2:x=T Com=Rf Rf Fr Orig=Fre SyncdWW Rfe DpAddrdR Fri Rfe SyncdRR Observation A087 Never 0 7 status: 0 real: 77.24 user: 77.18 sys: 0.06 ** Result for A134.litmus ** Test A134 Allowed States 7 1:r1=0; 2:r1=0; 2:r4=0; 1:r1=0; 2:r1=0; 2:r4=1; 1:r1=0; 2:r1=1; 2:r4=0; 1:r1=0; 2:r1=1; 2:r4=1; 1:r1=1; 2:r1=0; 2:r4=0; 1:r1=1; 2:r1=0; 2:r4=1; 1:r1=1; 2:r1=1; 2:r4=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r4=0) Hash=333c43155be80e5ed4be95edc1631cd9 Cycle=Rfe LwSyncdRW Rfe DpAddrdR Fre SyncdWW Relax A134 No Safe=Fre BCSyncdWW BCLwSyncdRW DpAddrdR Prefetch=2:x=T Com=Rf Rf Fr Orig=SyncdWW Rfe LwSyncdRW Rfe DpAddrdR Fre Observation A134 Never 0 7 status: 0 real: 81.94 user: 81.87 sys: 0.06 ** Result for A057.litmus ** Test A057 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=9946fe80b09678c9621ddb4416e4d0b7 Cycle=Rfe SyncdRW Rfe DpCtrlIsyncdR Fre LwSyncdWW Relax A057 No Safe=ABCSyncdRW Fre LwSyncdWW DpCtrlIsyncdR Prefetch=0:y=T Com=Fr Rf Rf Orig=DpCtrlIsyncdR Fre LwSyncdWW Rfe SyncdRW Rfe Observation A057 Never 0 7 status: 0 real: 85.50 user: 85.43 sys: 0.06 ** Result for A040.litmus ** Test A040 Allowed States 7 0:r1=0; 0:r4=0; 1:r1=0; 2:r1=0; 0:r1=0; 0:r4=0; 1:r1=0; 2:r1=1; 0:r1=0; 0:r4=0; 1:r1=1; 2:r1=0; 0:r1=0; 0:r4=0; 1:r1=1; 2:r1=1; 0:r1=1; 0:r4=0; 1:r1=0; 2:r1=0; 0:r1=1; 0:r4=0; 1:r1=0; 2:r1=1; 0:r1=1; 0:r4=0; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r1=1 /\ 2:r1=1) Hash=3fd8925583b45ef44deef08cbb24fab4 Cycle=Rfe SyncdRW Rfe DpAddrdR Fri Rfe LwSyncdRW Relax A040 No Safe=ABCSyncdRW ACLwSyncdRW [DpAddrdR,Fri] Prefetch= Com=Rf Rf Rf Orig=DpAddrdR Fri Rfe LwSyncdRW Rfe SyncdRW Rfe Observation A040 Never 0 7 status: 0 real: 85.56 user: 85.48 sys: 0.06 ** Result for A066.litmus ** Test A066 Allowed States 7 0:r1=0; 1:r1=0; 1:r4=0; 2:r1=0; 0:r1=0; 1:r1=0; 1:r4=0; 2:r1=1; 0:r1=0; 1:r1=1; 1:r4=0; 2:r1=0; 0:r1=0; 1:r1=1; 1:r4=0; 2:r1=1; 0:r1=1; 1:r1=0; 1:r4=0; 2:r1=0; 0:r1=1; 1:r1=0; 1:r4=0; 2:r1=1; 0:r1=1; 1:r1=1; 1:r4=0; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1) Hash=f907fb041f6a5303539e2d1bce424230 Cycle=Rfe SyncdRW Rfe LwSyncdRW Rfe DpAddrdR Fri Relax A066 No Safe=ABCSyncdRW BCLwSyncdRW [DpAddrdR,Fri] Prefetch= Com=Rf Rf Rf Orig=LwSyncdRW Rfe DpAddrdR Fri Rfe SyncdRW Rfe Observation A066 Never 0 7 status: 0 real: 87.19 user: 87.12 sys: 0.05 ** Result for A056.litmus ** Test A056 Allowed States 7 0:r1=0; 0:r4=0; 2:r1=0; 0:r1=0; 0:r4=0; 2:r1=1; 0:r1=0; 0:r4=1; 2:r1=0; 0:r1=0; 0:r4=1; 2:r1=1; 0:r1=1; 0:r4=0; 2:r1=0; 0:r1=1; 0:r4=1; 2:r1=0; 0:r1=1; 0:r4=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1) Hash=e9dd57776b4ea89e30feeff9242b4697 Cycle=Rfe SyncdRW Rfe DpAddrdR Fre LwSyncdWW Relax A056 No Safe=ABCSyncdRW Fre LwSyncdWW DpAddrdR Prefetch=0:y=T Com=Fr Rf Rf Orig=DpAddrdR Fre LwSyncdWW Rfe SyncdRW Rfe Observation A056 Never 0 7 status: 0 real: 96.08 user: 96.01 sys: 0.06 ** Result for A117.litmus ** Test A117 Allowed States 7 1:r1=0; 1:r3=0; 2:r3=0; 1:r1=0; 1:r3=0; 2:r3=1; 1:r1=0; 1:r3=1; 2:r3=0; 1:r1=0; 1:r3=1; 2:r3=1; 1:r1=1; 1:r3=0; 2:r3=1; 1:r1=1; 1:r3=1; 2:r3=0; 1:r1=1; 1:r3=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r3=0 /\ 2:r3=0) Hash=d3e17dbbf4dbbb975e9771c9c76c8985 Cycle=Rfe DpCtrlIsyncdR Fre SyncdWR Fre SyncdWW Relax A117 No Safe=Fre BCSyncdWW SyncdWR DpCtrlIsyncdR Prefetch=1:z=T,2:x=T Com=Rf Fr Fr Orig=SyncdWW Rfe DpCtrlIsyncdR Fre SyncdWR Fre Observation A117 Never 0 7 status: 0 real: 131.18 user: 131.09 sys: 0.08 ** Result for A116.litmus ** Test A116 Allowed States 7 1:r1=0; 1:r4=0; 2:r3=0; 1:r1=0; 1:r4=0; 2:r3=1; 1:r1=0; 1:r4=1; 2:r3=0; 1:r1=0; 1:r4=1; 2:r3=1; 1:r1=1; 1:r4=0; 2:r3=1; 1:r1=1; 1:r4=1; 2:r3=0; 1:r1=1; 1:r4=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 1:r4=0 /\ 2:r3=0) Hash=1c7217c7bdc904dcd1f67e0ec62d69a2 Cycle=Rfe DpAddrdR Fre SyncdWR Fre SyncdWW Relax A116 No Safe=Fre BCSyncdWW SyncdWR DpAddrdR Prefetch=1:z=T,2:x=T Com=Rf Fr Fr Orig=SyncdWW Rfe DpAddrdR Fre SyncdWR Fre Observation A116 Never 0 7 status: 0 real: 149.18 user: 149.06 sys: 0.10 ** Result for A014.litmus ** Test A014 Allowed States 9 2:r1=0; [x]=1; [y]=1; 2:r1=0; [x]=1; [y]=2; 2:r1=0; [x]=2; [y]=1; 2:r1=0; [x]=2; [y]=2; 2:r1=1; [x]=1; [y]=1; 2:r1=1; [x]=1; [y]=2; 2:r1=2; [x]=1; [y]=1; 2:r1=2; [x]=1; [y]=2; 2:r1=2; [x]=2; [y]=1; No (allowed not found) Condition exists ([x]=2 /\ [y]=2 /\ 2:r1=2) Hash=d1c3f07f1fa31d922fc825792ed9cef6 Cycle=Rfe SyncdRW Wse SyncdWW Wse Relax A014 No Safe=ACSyncdRW Wse SyncdWW Prefetch=0:x=F,0:y=W,1:y=F,2:x=W Com=Ws Rf Ws Orig=Wse SyncdWW Wse Rfe SyncdRW Observation A014 Never 0 9 status: 0 real: 250.51 user: 250.36 sys: 0.13 ** Result for A096.litmus ** Test A096 Allowed States 9 2:r1=0; [x]=1; [y]=1; 2:r1=0; [x]=1; [y]=2; 2:r1=0; [x]=2; [y]=1; 2:r1=0; [x]=2; [y]=2; 2:r1=1; [x]=1; [y]=1; 2:r1=1; [x]=1; [y]=2; 2:r1=2; [x]=1; [y]=1; 2:r1=2; [x]=1; [y]=2; 2:r1=2; [x]=2; [y]=1; No (allowed not found) Condition exists ([x]=2 /\ [y]=2 /\ 2:r1=2) Hash=7fce924a7efd2052c76e996f5835d7ff Cycle=Rfe LwSyncdRW Wse SyncdWW Wse Relax A096 No Safe=ACLwSyncdRW Wse SyncdWW Prefetch=0:x=F,0:y=W,1:y=F,2:x=W Com=Ws Rf Ws Orig=Wse SyncdWW Wse Rfe LwSyncdRW Observation A096 Never 0 9 status: 0 real: 319.00 user: 318.76 sys: 0.18 ** Result for A015.litmus ** Test A015 Allowed States 9 2:r1=0; [x]=1; [y]=1; 2:r1=0; [x]=1; [y]=2; 2:r1=0; [x]=2; [y]=1; 2:r1=0; [x]=2; [y]=2; 2:r1=1; [x]=1; [y]=1; 2:r1=1; [x]=1; [y]=2; 2:r1=2; [x]=1; [y]=1; 2:r1=2; [x]=1; [y]=2; 2:r1=2; [x]=2; [y]=1; No (allowed not found) Condition exists ([x]=2 /\ [y]=2 /\ 2:r1=2) Hash=5248bb9520bee03f39e74f9f920e4351 Cycle=Rfe SyncdRW Wse LwSyncdWW Wse Relax A015 No Safe=ACSyncdRW Wse LwSyncdWW Prefetch=0:x=F,0:y=W,1:y=F,2:x=W Com=Ws Rf Ws Orig=Wse LwSyncdWW Wse Rfe SyncdRW Observation A015 Never 0 9 status: 0 real: 404.63 user: 404.42 sys: 0.18 ** Result for A053.litmus ** Test A053 Allowed States 7 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=1; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=1) Hash=7fec6f3b9eda741c6021c0d3b636f5a9 Cycle=Rfe SyncdRW Rfe DpDatadW Wse SyncdWW Relax A053 No Safe=ABCSyncdRW Wse SyncdWW DpDatadW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpDatadW Wse SyncdWW Rfe SyncdRW Rfe Observation A053 Never 0 7 status: 0 real: 443.80 user: 443.60 sys: 0.16 ** Result for A054.litmus ** Test A054 Allowed States 7 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=1; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=1) Hash=9cb540cdbd0b7b40f968101f352213ec Cycle=Rfe SyncdRW Rfe DpCtrldW Wse SyncdWW Relax A054 No Safe=ABCSyncdRW Wse SyncdWW DpCtrldW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpCtrldW Wse SyncdWW Rfe SyncdRW Rfe Observation A054 Never 0 7 status: 0 real: 456.70 user: 456.50 sys: 0.17 ** Result for A052.litmus ** Test A052 Allowed States 7 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=1; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=1) Hash=f34f32e555082b2154cf1c7b07101331 Cycle=Rfe SyncdRW Rfe DpAddrdW Wse SyncdWW Relax A052 No Safe=ABCSyncdRW Wse SyncdWW DpAddrdW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpAddrdW Wse SyncdWW Rfe SyncdRW Rfe Observation A052 Never 0 7 status: 0 real: 468.06 user: 467.87 sys: 0.15 ** Result for A035.litmus ** Test A035 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=76085d5e4d55cd611983e6c45bad0c7d Cycle=Rfe SyncdRW Wse SyncdWW Rfe DpDatadW Relax A035 No Safe=ACSyncdRW Wse BCSyncdWW DpDatadW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpDatadW Rfe SyncdRW Observation A035 Never 0 7 status: 0 real: 481.53 user: 481.28 sys: 0.20 ** Result for A097.litmus ** Test A097 Allowed States 9 2:r1=0; [x]=1; [y]=1; 2:r1=0; [x]=1; [y]=2; 2:r1=0; [x]=2; [y]=1; 2:r1=0; [x]=2; [y]=2; 2:r1=1; [x]=1; [y]=1; 2:r1=1; [x]=1; [y]=2; 2:r1=2; [x]=1; [y]=1; 2:r1=2; [x]=1; [y]=2; 2:r1=2; [x]=2; [y]=1; No (allowed not found) Condition exists ([x]=2 /\ [y]=2 /\ 2:r1=2) Hash=0d93c656eef62454089791eac38a0c3a Cycle=Rfe LwSyncdRW Wse LwSyncdWW Wse Relax A097 No Safe=ACLwSyncdRW Wse LwSyncdWW Prefetch=0:x=F,0:y=W,1:y=F,2:x=W Com=Ws Rf Ws Orig=Wse LwSyncdWW Wse Rfe LwSyncdRW Observation A097 Never 0 9 status: 0 real: 485.47 user: 485.18 sys: 0.26 ** Result for A037.litmus ** Test A037 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=9fa38043ac4b2d78c52ffaf09e3b2658 Cycle=Rfe SyncdRW Wse SyncdWW Rfe DpCtrldW Relax A037 No Safe=ACSyncdRW Wse BCSyncdWW DpCtrldW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpCtrldW Rfe SyncdRW Observation A037 Never 0 7 status: 0 real: 488.94 user: 488.70 sys: 0.20 ** Result for A029.litmus ** Test A029 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=4b1c119c40ba6345dd73b312e973c3a0 Cycle=Rfe SyncdRW Wse SyncdWW Rfe DpAddrdW Relax A029 No Safe=ACSyncdRW Wse BCSyncdWW DpAddrdW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpAddrdW Rfe SyncdRW Observation A029 Never 0 7 status: 0 real: 504.31 user: 504.00 sys: 0.20 ** Result for A155.litmus ** Test A155 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=80283d08c83045ece7e3a2900188ca8b Cycle=Rfe LwSyncdRW Rfe DpDatadW Wse SyncdWW Relax A155 No Safe=Wse BCSyncdWW BCLwSyncdRW DpDatadW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=SyncdWW Rfe LwSyncdRW Rfe DpDatadW Wse Observation A155 Never 0 7 status: 0 real: 548.12 user: 547.88 sys: 0.20 ** Result for A033.litmus ** Test A033 Allowed States 7 1:r1=0; 1:r4=0; 2:r1=0; [x]=1; 1:r1=0; 1:r4=0; 2:r1=0; [x]=2; 1:r1=0; 1:r4=0; 2:r1=1; [x]=1; 1:r1=0; 1:r4=0; 2:r1=1; [x]=2; 1:r1=1; 1:r4=0; 2:r1=0; [x]=1; 1:r1=1; 1:r4=0; 2:r1=0; [x]=2; 1:r1=1; 1:r4=0; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1) Hash=c00676e175b01df6189775a4a1492faa Cycle=Rfe SyncdRW Wse SyncdWW Rfe DpAddrdR Fri Relax A033 No Safe=ACSyncdRW Wse BCSyncdWW [DpAddrdR,Fri] Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpAddrdR Fri Rfe SyncdRW Observation A033 Never 0 7 status: 0 real: 559.35 user: 559.06 sys: 0.24 ** Result for A157.litmus ** Test A157 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=0d746c311f10ed89a351bb2ac17f3edd Cycle=Rfe LwSyncdRW Rfe DpCtrldW Wse SyncdWW Relax A157 No Safe=Wse BCSyncdWW BCLwSyncdRW DpCtrldW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=SyncdWW Rfe LwSyncdRW Rfe DpCtrldW Wse Observation A157 Never 0 7 status: 0 real: 561.59 user: 561.33 sys: 0.21 ** Result for A153.litmus ** Test A153 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=f0617f9b7a0e51dd68bdbdc492ad3b04 Cycle=Rfe LwSyncdRW Rfe DpAddrdW Wse SyncdWW Relax A153 No Safe=Wse BCSyncdWW BCLwSyncdRW DpAddrdW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=SyncdWW Rfe LwSyncdRW Rfe DpAddrdW Wse Observation A153 Never 0 7 status: 0 real: 578.10 user: 577.82 sys: 0.22 ** Result for A136.litmus ** Test A136 Allowed States 7 2:r1=0; 2:r3=0; [y]=1; 2:r1=0; 2:r3=0; [y]=2; 2:r1=0; 2:r3=1; [y]=1; 2:r1=0; 2:r3=1; [y]=2; 2:r1=1; 2:r3=0; [y]=1; 2:r1=1; 2:r3=1; [y]=1; 2:r1=1; 2:r3=1; [y]=2; No (allowed not found) Condition exists ([y]=2 /\ 2:r1=1 /\ 2:r3=0) Hash=98cc1331b96b3493cfe6be077f85cc62 Cycle=Rfe DpCtrlIsyncdR Fre SyncdWW Wse SyncdWW Relax A136 No Safe=Fre Wse SyncdWW BCSyncdWW DpCtrlIsyncdR Prefetch=0:y=W,1:y=F,2:x=T Com=Ws Rf Fr Orig=SyncdWW Wse SyncdWW Rfe DpCtrlIsyncdR Fre Observation A136 Never 0 7 status: 0 real: 584.20 user: 583.93 sys: 0.22 ** Result for A109.litmus ** Test A109 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=b707d4dcf4d7263dd89dc61fa169a25d Cycle=Rfe LwSyncdRW Wse SyncdWW Rfe DpDatadW Relax A109 No Safe=ACLwSyncdRW Wse BCSyncdWW DpDatadW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpDatadW Rfe LwSyncdRW Observation A109 Never 0 7 status: 0 real: 614.30 user: 614.02 sys: 0.21 ** Result for A110.litmus ** Test A110 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=de67e5925cc161c0d146cb9779fbe9ea Cycle=Rfe LwSyncdRW Wse SyncdWW Rfe DpCtrldW Relax A110 No Safe=ACLwSyncdRW Wse BCSyncdWW DpCtrldW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpCtrldW Rfe LwSyncdRW Observation A110 Never 0 7 status: 0 real: 624.46 user: 624.19 sys: 0.21 ** Result for A106.litmus ** Test A106 Allowed States 7 1:r1=0; 2:r1=0; [x]=1; 1:r1=0; 2:r1=0; [x]=2; 1:r1=0; 2:r1=1; [x]=1; 1:r1=0; 2:r1=1; [x]=2; 1:r1=1; 2:r1=0; [x]=1; 1:r1=1; 2:r1=0; [x]=2; 1:r1=1; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 2:r1=1) Hash=92456c6d17c0f8558ad9ba3a36602724 Cycle=Rfe LwSyncdRW Wse SyncdWW Rfe DpAddrdW Relax A106 No Safe=ACLwSyncdRW Wse BCSyncdWW DpAddrdW Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpAddrdW Rfe LwSyncdRW Observation A106 Never 0 7 status: 0 real: 647.33 user: 646.95 sys: 0.25 ** Result for A059.litmus ** Test A059 Allowed States 7 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=1; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=1) Hash=4f13613a0bd069ebdc510516e1df2d7d Cycle=Rfe SyncdRW Rfe DpDatadW Wse LwSyncdWW Relax A059 No Safe=ABCSyncdRW Wse LwSyncdWW DpDatadW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpDatadW Wse LwSyncdWW Rfe SyncdRW Rfe Observation A059 Never 0 7 status: 0 real: 648.62 user: 648.34 sys: 0.23 ** Result for A060.litmus ** Test A060 Allowed States 7 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=1; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=1) Hash=7396565da901351729ebc4446e10ba54 Cycle=Rfe SyncdRW Rfe DpCtrldW Wse LwSyncdWW Relax A060 No Safe=ABCSyncdRW Wse LwSyncdWW DpCtrldW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpCtrldW Wse LwSyncdWW Rfe SyncdRW Rfe Observation A060 Never 0 7 status: 0 real: 662.21 user: 661.92 sys: 0.23 ** Result for A132.litmus ** Test A132 Allowed States 7 2:r1=0; 2:r4=0; [y]=1; 2:r1=0; 2:r4=0; [y]=2; 2:r1=0; 2:r4=1; [y]=1; 2:r1=0; 2:r4=1; [y]=2; 2:r1=1; 2:r4=0; [y]=1; 2:r1=1; 2:r4=1; [y]=1; 2:r1=1; 2:r4=1; [y]=2; No (allowed not found) Condition exists ([y]=2 /\ 2:r1=1 /\ 2:r4=0) Hash=9d7f07ce6da224ac7eca2af4a5915a72 Cycle=Rfe DpAddrdR Fre SyncdWW Wse SyncdWW Relax A132 No Safe=Fre Wse SyncdWW BCSyncdWW DpAddrdR Prefetch=0:y=W,1:y=F,2:x=T Com=Ws Rf Fr Orig=SyncdWW Wse SyncdWW Rfe DpAddrdR Fre Observation A132 Never 0 7 status: 0 real: 676.34 user: 675.97 sys: 0.23 ** Result for A058.litmus ** Test A058 Allowed States 7 0:r1=0; 2:r1=0; [y]=1; 0:r1=0; 2:r1=0; [y]=2; 0:r1=0; 2:r1=1; [y]=1; 0:r1=0; 2:r1=1; [y]=2; 0:r1=1; 2:r1=0; [y]=1; 0:r1=1; 2:r1=0; [y]=2; 0:r1=1; 2:r1=1; [y]=1; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 2:r1=1) Hash=be0539b608e4d783a36d89e96f576707 Cycle=Rfe SyncdRW Rfe DpAddrdW Wse LwSyncdWW Relax A058 No Safe=ABCSyncdRW Wse LwSyncdWW DpAddrdW Prefetch=0:y=W,1:y=F Com=Ws Rf Rf Orig=DpAddrdW Wse LwSyncdWW Rfe SyncdRW Rfe Observation A058 Never 0 7 status: 0 real: 684.62 user: 684.33 sys: 0.23 ** Result for A108.litmus ** Test A108 Allowed States 7 1:r1=0; 1:r4=0; 2:r1=0; [x]=1; 1:r1=0; 1:r4=0; 2:r1=0; [x]=2; 1:r1=0; 1:r4=0; 2:r1=1; [x]=1; 1:r1=0; 1:r4=0; 2:r1=1; [x]=2; 1:r1=1; 1:r4=0; 2:r1=0; [x]=1; 1:r1=1; 1:r4=0; 2:r1=0; [x]=2; 1:r1=1; 1:r4=0; 2:r1=1; [x]=1; No (allowed not found) Condition exists ([x]=2 /\ 1:r1=1 /\ 1:r4=0 /\ 2:r1=1) Hash=4056b2f8a8c90d01972a33cc7b9779d6 Cycle=Rfe LwSyncdRW Wse SyncdWW Rfe DpAddrdR Fri Relax A108 No Safe=ACLwSyncdRW Wse BCSyncdWW [DpAddrdR,Fri] Prefetch=0:x=F,2:x=W Com=Rf Rf Ws Orig=Wse SyncdWW Rfe DpAddrdR Fri Rfe LwSyncdRW Observation A108 Never 0 7 status: 0 real: 715.79 user: 715.46 sys: 0.26 ** Result for A137.litmus ** Test A137 Allowed States 8 2:r1=0; 2:r3=0; [y]=1; 2:r1=0; 2:r3=0; [y]=2; 2:r1=0; 2:r3=1; [y]=1; 2:r1=0; 2:r3=1; [y]=2; 2:r1=1; 2:r3=0; [y]=1; 2:r1=1; 2:r3=0; [y]=2; 2:r1=1; 2:r3=1; [y]=1; 2:r1=1; 2:r3=1; [y]=2; Ok Condition exists ([y]=2 /\ 2:r1=1 /\ 2:r3=0) Hash=7535dd2681b9d4f2cf717fe69e976cc3 Cycle=Rfe DpCtrlIsyncdR Fre LwSyncdWW Wse SyncdWW Relax A137 Ok Safe=Fre Wse BCSyncdWW LwSyncdWW DpCtrlIsyncdR Prefetch=0:y=W,1:y=F,2:x=T Com=Ws Rf Fr Orig=LwSyncdWW Wse SyncdWW Rfe DpCtrlIsyncdR Fre Observation A137 Sometimes 1 7 status: 0 real: 941.21 user: 940.82 sys: 0.30 ** Result for A133.litmus ** Test A133 Allowed States 8 2:r1=0; 2:r4=0; [y]=1; 2:r1=0; 2:r4=0; [y]=2; 2:r1=0; 2:r4=1; [y]=1; 2:r1=0; 2:r4=1; [y]=2; 2:r1=1; 2:r4=0; [y]=1; 2:r1=1; 2:r4=0; [y]=2; 2:r1=1; 2:r4=1; [y]=1; 2:r1=1; 2:r4=1; [y]=2; Ok Condition exists ([y]=2 /\ 2:r1=1 /\ 2:r4=0) Hash=c0ed55e7521396eac2e6b3b628d20324 Cycle=Rfe DpAddrdR Fre LwSyncdWW Wse SyncdWW Relax A133 Ok Safe=Fre Wse BCSyncdWW LwSyncdWW DpAddrdR Prefetch=0:y=W,1:y=F,2:x=T Com=Ws Rf Fr Orig=LwSyncdWW Wse SyncdWW Rfe DpAddrdR Fre Observation A133 Sometimes 1 7 status: 0 real: 1082.16 user: 1081.68 sys: 0.37 ** Result for A125.litmus ** Test A125 Allowed States 7 1:r1=0; 2:r3=0; [z]=1; 1:r1=0; 2:r3=0; [z]=2; 1:r1=0; 2:r3=1; [z]=1; 1:r1=0; 2:r3=1; [z]=2; 1:r1=1; 2:r3=0; [z]=1; 1:r1=1; 2:r3=1; [z]=1; 1:r1=1; 2:r3=1; [z]=2; No (allowed not found) Condition exists ([z]=2 /\ 1:r1=1 /\ 2:r3=0) Hash=c04ff3127d66d72483e3246bdc9b2fcb Cycle=Rfe DpDatadW Wse SyncdWR Fre SyncdWW Relax A125 No Safe=Fre Wse BCSyncdWW SyncdWR DpDatadW Prefetch=1:z=W,2:z=F,2:x=T Com=Rf Ws Fr Orig=SyncdWW Rfe DpDatadW Wse SyncdWR Fre Observation A125 Never 0 7 status: 0 real: 1090.80 user: 1090.31 sys: 0.39 ** Result for A126.litmus ** Test A126 Allowed States 7 1:r1=0; 2:r3=0; [z]=1; 1:r1=0; 2:r3=0; [z]=2; 1:r1=0; 2:r3=1; [z]=1; 1:r1=0; 2:r3=1; [z]=2; 1:r1=1; 2:r3=0; [z]=1; 1:r1=1; 2:r3=1; [z]=1; 1:r1=1; 2:r3=1; [z]=2; No (allowed not found) Condition exists ([z]=2 /\ 1:r1=1 /\ 2:r3=0) Hash=db42115d57d57cf452aec0b95b64bfef Cycle=Rfe DpCtrldW Wse SyncdWR Fre SyncdWW Relax A126 No Safe=Fre Wse BCSyncdWW SyncdWR DpCtrldW Prefetch=1:z=W,2:z=F,2:x=T Com=Rf Ws Fr Orig=SyncdWW Rfe DpCtrldW Wse SyncdWR Fre Observation A126 Never 0 7 status: 0 real: 1107.19 user: 1106.75 sys: 0.35 ** Result for A124.litmus ** Test A124 Allowed States 7 1:r1=0; 2:r3=0; [z]=1; 1:r1=0; 2:r3=0; [z]=2; 1:r1=0; 2:r3=1; [z]=1; 1:r1=0; 2:r3=1; [z]=2; 1:r1=1; 2:r3=0; [z]=1; 1:r1=1; 2:r3=1; [z]=1; 1:r1=1; 2:r3=1; [z]=2; No (allowed not found) Condition exists ([z]=2 /\ 1:r1=1 /\ 2:r3=0) Hash=f3987244b10801ba3857394a9988bab7 Cycle=Rfe DpAddrdW Wse SyncdWR Fre SyncdWW Relax A124 No Safe=Fre Wse BCSyncdWW SyncdWR DpAddrdW Prefetch=1:z=W,2:z=F,2:x=T Com=Rf Ws Fr Orig=SyncdWW Rfe DpAddrdW Wse SyncdWR Fre Observation A124 Never 0 7 status: 0 real: 1155.34 user: 1154.79 sys: 0.41 ** Result for A001.litmus ** Test A001 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=56ecab79b42198224f8bc0fbc64d4acc Cycle=Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Relax A001 No Safe=ACSyncdRW Prefetch= Com=Rf Rf Rf Orig=Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Observation A001 Never 0 7 status: 0 real: 1173.64 user: 1173.03 sys: 0.50 ** Result for A016.litmus ** Test A016 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=3b03c4d439cf6615f11241b5075446fd Cycle=Rfe SyncdRW Rfe SyncdRR Fre SyncdWW Relax A016 No Safe=ACSyncdRW ACSyncdRR Fre SyncdWW Prefetch=0:y=T Com=Fr Rf Rf Orig=Rfe SyncdRR Fre SyncdWW Rfe SyncdRW Observation A016 Never 0 7 status: 0 real: 1247.44 user: 1246.84 sys: 0.50 ** Result for A002.litmus ** Test A002 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=6e8db112b0ab6289ef5d7904e3bb6fa2 Cycle=Rfe SyncdRW Rfe SyncdRW Rfe LwSyncdRW Relax A002 No Safe=ACSyncdRW ACLwSyncdRW Prefetch= Com=Rf Rf Rf Orig=Rfe LwSyncdRW Rfe SyncdRW Rfe SyncdRW Observation A002 Never 0 7 status: 0 real: 1511.53 user: 1510.77 sys: 0.62 ** Result for A072.litmus ** Test A072 Allowed States 7 1:r1=0; 2:r1=0; 2:r3=0; 1:r1=0; 2:r1=0; 2:r3=1; 1:r1=0; 2:r1=1; 2:r3=0; 1:r1=0; 2:r1=1; 2:r3=1; 1:r1=1; 2:r1=0; 2:r3=0; 1:r1=1; 2:r1=0; 2:r3=1; 1:r1=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Hash=e6d27e5223cf34c3b52521362bb358fb Cycle=Rfe SyncdRR Fre SyncdWW Rfe LwSyncdRW Relax A072 No Safe=ACSyncdRR ACLwSyncdRW Fre SyncdWW Prefetch=2:x=T Com=Rf Rf Fr Orig=Fre SyncdWW Rfe LwSyncdRW Rfe SyncdRR Observation A072 Never 0 7 status: 0 real: 1567.12 user: 1566.21 sys: 0.58 ** Result for A007.litmus ** Test A007 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=f53ad09007c55a1b3b0f1b7fff62a915 Cycle=Rfe SyncdRW Rfe LwSyncdRW Rfe LwSyncdRW Relax A007 No Safe=ACSyncdRW ACLwSyncdRW Prefetch= Com=Rf Rf Rf Orig=Rfe LwSyncdRW Rfe LwSyncdRW Rfe SyncdRW Observation A007 Never 0 7 status: 0 real: 1848.85 user: 1848.04 sys: 0.66 ** Result for A022.litmus ** Test A022 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=b9f23e89bf7e9fb619fd22884a56ea58 Cycle=Rfe SyncdRW Rfe SyncdRR Fre LwSyncdWW Relax A022 No Safe=ACSyncdRW ACSyncdRR Fre LwSyncdWW Prefetch=0:y=T Com=Fr Rf Rf Orig=Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRW Observation A022 Never 0 7 status: 0 real: 2035.85 user: 2034.94 sys: 0.75 ** Result for A091.litmus ** Test A091 Allowed States 7 0:r1=0; 1:r1=0; 2:r1=0; 0:r1=0; 1:r1=0; 2:r1=1; 0:r1=0; 1:r1=1; 2:r1=0; 0:r1=0; 1:r1=1; 2:r1=1; 0:r1=1; 1:r1=0; 2:r1=0; 0:r1=1; 1:r1=0; 2:r1=1; 0:r1=1; 1:r1=1; 2:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Hash=1b0bb3ba1a0dc46a6674c60afd617090 Cycle=Rfe LwSyncdRW Rfe LwSyncdRW Rfe LwSyncdRW Relax A091 No Safe=ACLwSyncdRW Prefetch= Com=Rf Rf Rf Orig=Rfe LwSyncdRW Rfe LwSyncdRW Rfe LwSyncdRW Observation A091 Never 0 7 status: 0 real: 2073.96 user: 2073.08 sys: 0.68 ** Result for A073.litmus ** Test A073 Allowed States 7 1:r1=0; 2:r1=0; 2:r3=0; 1:r1=0; 2:r1=0; 2:r3=1; 1:r1=0; 2:r1=1; 2:r3=0; 1:r1=0; 2:r1=1; 2:r3=1; 1:r1=1; 2:r1=0; 2:r3=0; 1:r1=1; 2:r1=0; 2:r3=1; 1:r1=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Hash=8c879ef10b2f67896f187b0082426039 Cycle=Rfe SyncdRR Fre LwSyncdWW Rfe LwSyncdRW Relax A073 No Safe=ACSyncdRR ACLwSyncdRW Fre LwSyncdWW Prefetch=2:x=T Com=Rf Rf Fr Orig=Fre LwSyncdWW Rfe LwSyncdRW Rfe SyncdRR Observation A073 Never 0 7 status: 0 real: 2524.78 user: 2523.43 sys: 0.84 ** Result for A049.litmus ** Test A049 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=b67c6d5b69764bf1d4195afb96757bf9 Cycle=Rfe SyncdRW Rfe LwSyncdRR Fre SyncdWW Relax A049 No Safe=ABCSyncdRW Fre SyncdWW LwSyncdRR Prefetch=0:y=T Com=Fr Rf Rf Orig=LwSyncdRR Fre SyncdWW Rfe SyncdRW Rfe Observation A049 Never 0 7 status: 0 real: 2690.63 user: 2689.46 sys: 0.94 ** Result for A030.litmus ** Test A030 Allowed States 10 0:r1=0; 1:r1=0; 2:r1=0; [z]=2; 0:r1=0; 1:r1=0; 2:r1=1; [z]=2; 0:r1=0; 1:r1=0; 2:r1=2; [z]=2; 0:r1=0; 1:r1=1; 2:r1=0; [z]=2; 0:r1=0; 1:r1=1; 2:r1=1; [z]=2; 0:r1=0; 1:r1=1; 2:r1=2; [z]=2; 0:r1=1; 1:r1=0; 2:r1=0; [z]=2; 0:r1=1; 1:r1=0; 2:r1=1; [z]=2; 0:r1=1; 1:r1=0; 2:r1=2; [z]=2; 0:r1=1; 1:r1=1; 2:r1=0; [z]=2; No (allowed not found) Condition exists ([z]=2 /\ 0:r1=1 /\ 1:r1=1 /\ 2:r1=2) Hash=33daa5a991b2e96e9e09446ecb762221 Cycle=Rfe SyncdRW Rfe SyncdRW Rfe DpAddrdW Wsi Relax A030 No Safe=ACSyncdRW ABCSyncdRW [DpAddrdW,Wsi] Prefetch= Com=Rf Rf Rf Orig=Rfe SyncdRW Rfe DpAddrdW Wsi Rfe SyncdRW Observation A030 Never 0 10 status: 0 real: 2844.25 user: 2842.95 sys: 0.70 ** Result for A130.litmus ** Test A130 Allowed States 7 1:r1=0; 2:r1=0; 2:r3=0; 1:r1=0; 2:r1=0; 2:r3=1; 1:r1=0; 2:r1=1; 2:r3=0; 1:r1=0; 2:r1=1; 2:r3=1; 1:r1=1; 2:r1=0; 2:r3=0; 1:r1=1; 2:r1=0; 2:r3=1; 1:r1=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Hash=8ddb210570879a91055da0f14cb696ad Cycle=Rfe LwSyncdRW Rfe LwSyncdRR Fre SyncdWW Relax A130 No Safe=Fre BCSyncdWW BCLwSyncdRW LwSyncdRR Prefetch=2:x=T Com=Rf Rf Fr Orig=SyncdWW Rfe LwSyncdRW Rfe LwSyncdRR Fre Observation A130 Never 0 7 status: 0 real: 3289.59 user: 3288.14 sys: 1.16 ** Result for A064.litmus ** Test A064 Allowed States 10 0:r1=0; 1:r1=0; 2:r1=0; [z]=2; 0:r1=0; 1:r1=0; 2:r1=1; [z]=2; 0:r1=0; 1:r1=0; 2:r1=2; [z]=2; 0:r1=0; 1:r1=1; 2:r1=0; [z]=2; 0:r1=0; 1:r1=1; 2:r1=1; [z]=2; 0:r1=0; 1:r1=1; 2:r1=2; [z]=2; 0:r1=1; 1:r1=0; 2:r1=0; [z]=2; 0:r1=1; 1:r1=0; 2:r1=1; [z]=2; 0:r1=1; 1:r1=0; 2:r1=2; [z]=2; 0:r1=1; 1:r1=1; 2:r1=0; [z]=2; No (allowed not found) Condition exists ([z]=2 /\ 0:r1=1 /\ 1:r1=1 /\ 2:r1=2) Hash=4691a6450a346d1766dd2929217c7dbf Cycle=Rfe SyncdRW Rfe LwSyncdRW Rfe DpAddrdW Wsi Relax A064 No Safe=ABCSyncdRW BCLwSyncdRW [DpAddrdW,Wsi] Prefetch= Com=Rf Rf Rf Orig=LwSyncdRW Rfe DpAddrdW Wsi Rfe SyncdRW Rfe Observation A064 Never 0 10 status: 0 real: 3530.62 user: 3529.10 sys: 0.83 ** Result for A039.litmus ** Test A039 Allowed States 10 0:r1=0; 1:r1=0; 2:r1=0; [y]=2; 0:r1=0; 1:r1=0; 2:r1=1; [y]=2; 0:r1=0; 1:r1=1; 2:r1=0; [y]=2; 0:r1=0; 1:r1=1; 2:r1=1; [y]=2; 0:r1=0; 1:r1=2; 2:r1=0; [y]=2; 0:r1=0; 1:r1=2; 2:r1=1; [y]=2; 0:r1=1; 1:r1=0; 2:r1=0; [y]=2; 0:r1=1; 1:r1=0; 2:r1=1; [y]=2; 0:r1=1; 1:r1=1; 2:r1=0; [y]=2; 0:r1=1; 1:r1=2; 2:r1=0; [y]=2; No (allowed not found) Condition exists ([y]=2 /\ 0:r1=1 /\ 1:r1=2 /\ 2:r1=1) Hash=832b5d816acc245781020bae48554fa1 Cycle=Rfe SyncdRW Rfe DpAddrdW Wsi Rfe LwSyncdRW Relax A039 No Safe=ABCSyncdRW ACLwSyncdRW [DpAddrdW,Wsi] Prefetch= Com=Rf Rf Rf Orig=DpAddrdW Wsi Rfe LwSyncdRW Rfe SyncdRW Rfe Observation A039 Never 0 10 status: 0 real: 3532.69 user: 3531.08 sys: 0.86 ** Result for A086.litmus ** Test A086 Allowed States 10 1:r1=0; 2:r1=0; 2:r3=0; [z]=2; 1:r1=0; 2:r1=0; 2:r3=1; [z]=2; 1:r1=0; 2:r1=1; 2:r3=0; [z]=2; 1:r1=0; 2:r1=1; 2:r3=1; [z]=2; 1:r1=0; 2:r1=2; 2:r3=0; [z]=2; 1:r1=0; 2:r1=2; 2:r3=1; [z]=2; 1:r1=1; 2:r1=0; 2:r3=0; [z]=2; 1:r1=1; 2:r1=0; 2:r3=1; [z]=2; 1:r1=1; 2:r1=1; 2:r3=1; [z]=2; 1:r1=1; 2:r1=2; 2:r3=1; [z]=2; No (allowed not found) Condition exists ([z]=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) Hash=1b43c68e1bc3875836b5d5e7cb624127 Cycle=Rfe SyncdRR Fre SyncdWW Rfe DpAddrdW Wsi Relax A086 No Safe=ACSyncdRR Fre BCSyncdWW [DpAddrdW,Wsi] Prefetch=2:x=T Com=Rf Rf Fr Orig=Fre SyncdWW Rfe DpAddrdW Wsi Rfe SyncdRR Observation A086 Never 0 10 status: 0 real: 3707.11 user: 3705.71 sys: 1.08 ** Result for A078.litmus ** Test A078 Allowed States 7 0:r3=0; 2:r1=0; 2:r3=0; 0:r3=0; 2:r1=0; 2:r3=1; 0:r3=0; 2:r1=1; 2:r3=1; 0:r3=1; 2:r1=0; 2:r3=0; 0:r3=1; 2:r1=0; 2:r3=1; 0:r3=1; 2:r1=1; 2:r3=0; 0:r3=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Hash=d99b2c9fcd24d521255a6c4ef185df57 Cycle=Rfe SyncdRR Fre SyncdWR Fre SyncdWW Relax A078 No Safe=ACSyncdRR Fre SyncdWW SyncdWR Prefetch=0:y=T,2:x=T Com=Fr Rf Fr Orig=Fre SyncdWR Fre SyncdWW Rfe SyncdRR Observation A078 Never 0 7 status: 0 real: 3898.98 user: 3897.34 sys: 1.28 ** Result for A055.litmus ** Test A055 Allowed States 7 0:r1=0; 0:r3=0; 2:r1=0; 0:r1=0; 0:r3=0; 2:r1=1; 0:r1=0; 0:r3=1; 2:r1=0; 0:r1=0; 0:r3=1; 2:r1=1; 0:r1=1; 0:r3=0; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=0; 0:r1=1; 0:r3=1; 2:r1=1; No (allowed not found) Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1) Hash=3c24fffa3d1148f4d64f351d9a0ba727 Cycle=Rfe SyncdRW Rfe LwSyncdRR Fre LwSyncdWW Relax A055 No Safe=ABCSyncdRW Fre LwSyncdWW LwSyncdRR Prefetch=0:y=T Com=Fr Rf Rf Orig=LwSyncdRR Fre LwSyncdWW Rfe SyncdRW Rfe Observation A055 Never 0 7 status: 0 real: 4217.64 user: 4215.86 sys: 1.42 ** Result for A082.litmus ** Test A082 Allowed States 7 0:r3=0; 2:r1=0; 2:r3=0; 0:r3=0; 2:r1=0; 2:r3=1; 0:r3=0; 2:r1=1; 2:r3=1; 0:r3=1; 2:r1=0; 2:r3=0; 0:r3=1; 2:r1=0; 2:r3=1; 0:r3=1; 2:r1=1; 2:r3=0; 0:r3=1; 2:r1=1; 2:r3=1; No (allowed not found) Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Hash=a4f543f0d0b7b763d028766f2fc68faf Cycle=Rfe SyncdRR Fre SyncdWR Fre LwSyncdWW Relax A082 No Safe=ACSyncdRR Fre SyncdWR LwSyncdWW Prefetch=0:y=T,2:x=T Com=Fr Rf Fr Orig=Fre SyncdWR Fre LwSyncdWW Rfe SyncdRR Observation A082 Never 0 7 status: 0 real: 6285.63 user: 6283.21 sys: 1.84 ** Result for A112.litmus ** status: 2 real: 6995.24 user: 6992.54 sys: 2.06 Warning: stderr Fatal error: out of memory. ** Result for A115.litmus ** status: 2 real: 7032.33 user: 7029.61 sys: 2.07 Warning: stderr Fatal error: out of memory. ** Result for A145.litmus ** Test A145 Allowed States 7 1:r1=0; [x]=1; [z]=1; 1:r1=0; [x]=1; [z]=2; 1:r1=0; [x]=2; [z]=1; 1:r1=0; [x]=2; [z]=2; 1:r1=1; [x]=1; [z]=1; 1:r1=1; [x]=1; [z]=2; 1:r1=1; [x]=2; [z]=1; No (allowed not found) Condition exists ([x]=2 /\ [z]=2 /\ 1:r1=1) Hash=4f37f7324b14c7de897821f5e3303454 Cycle=Rfe DpDatadW Wse SyncdWW Wse SyncdWW Relax A145 No Safe=Wse SyncdWW BCSyncdWW DpDatadW Prefetch=0:x=F,1:z=W,2:z=F,2:x=W Com=Rf Ws Ws Orig=SyncdWW Rfe DpDatadW Wse SyncdWW Wse Observation A145 Never 0 7 status: 0 real: 7164.86 user: 7162.95 sys: 1.24 ** Result for A146.litmus ** Test A146 Allowed States 7 1:r1=0; [x]=1; [z]=1; 1:r1=0; [x]=1; [z]=2; 1:r1=0; [x]=2; [z]=1; 1:r1=0; [x]=2; [z]=2; 1:r1=1; [x]=1; [z]=1; 1:r1=1; [x]=1; [z]=2; 1:r1=1; [x]=2; [z]=1; No (allowed not found) Condition exists ([x]=2 /\ [z]=2 /\ 1:r1=1) Hash=93ee1ac4c0d636f57db96dfb6354e333 Cycle=Rfe DpCtrldW Wse SyncdWW Wse SyncdWW Relax A146 No Safe=Wse SyncdWW BCSyncdWW DpCtrldW Prefetch=0:x=F,1:z=W,2:z=F,2:x=W Com=Rf Ws Ws Orig=SyncdWW Rfe DpCtrldW Wse SyncdWW Wse Observation A146 Never 0 7 status: 0 real: 7260.65 user: 7258.73 sys: 1.25 ** Result for A144.litmus ** Test A144 Allowed States 7 1:r1=0; [x]=1; [z]=1; 1:r1=0; [x]=1; [z]=2; 1:r1=0; [x]=2; [z]=1; 1:r1=0; [x]=2; [z]=2; 1:r1=1; [x]=1; [z]=1; 1:r1=1; [x]=1; [z]=2; 1:r1=1; [x]=2; [z]=1; No (allowed not found) Condition exists ([x]=2 /\ [z]=2 /\ 1:r1=1) Hash=61706d506aedff4395c0fcabfb3f3625 Cycle=Rfe DpAddrdW Wse SyncdWW Wse SyncdWW Relax A144 No Safe=Wse SyncdWW BCSyncdWW DpAddrdW Prefetch=0:x=F,1:z=W,2:z=F,2:x=W Com=Rf Ws Ws Orig=SyncdWW Rfe DpAddrdW Wse SyncdWW Wse Observation A144 Never 0 7 status: 0 real: 7551.01 user: 7548.82 sys: 1.48 ** Result for A079.litmus ** status: 2 real: 9910.16 user: 9906.25 sys: 1.96 Warning: stderr Fatal error: out of memory. ** Result for A129.litmus ** status: 2 real: 10035.81 user: 10032.79 sys: 2.11 Warning: stderr Fatal error: out of memory. ** Result for A114.litmus ** status: 2 real: 10042.18 user: 10039.49 sys: 1.77 Warning: stderr Fatal error: out of memory. ** Result for A084.litmus ** status: 2 real: 10047.98 user: 10045.24 sys: 1.87 Warning: stderr Fatal error: out of memory. ** Result for A080.litmus ** status: 2 real: 10066.50 user: 10062.58 sys: 1.84 Warning: stderr Fatal error: out of memory. ** Result for A083.litmus ** status: 2 real: 10311.39 user: 10308.46 sys: 2.01 Warning: stderr Fatal error: out of memory. ** Result for A128.litmus ** status: 2 real: 10421.61 user: 10418.82 sys: 1.84 Warning: stderr Fatal error: out of memory. ** Result for A113.litmus ** status: 2 real: 10452.68 user: 10449.80 sys: 1.94 Warning: stderr Fatal error: out of memory. ** Result for A010.litmus ** status: 2 real: 10591.52 user: 10588.77 sys: 1.90 Warning: stderr Fatal error: out of memory. ** Result for A094.litmus ** status: 2 real: 10606.98 user: 10604.17 sys: 1.83 Warning: stderr Fatal error: out of memory. ** Result for A023.litmus ** status: 2 real: 10641.88 user: 10639.14 sys: 1.87 Warning: stderr Fatal error: out of memory. ** Result for A004.litmus ** status: 2 real: 10695.98 user: 10693.15 sys: 1.84 Warning: stderr Fatal error: out of memory. ** Result for A102.litmus ** status: 2 real: 10724.88 user: 10722.00 sys: 1.89 Warning: stderr Fatal error: out of memory. ** Result for A017.litmus ** status: 2 real: 10948.41 user: 10945.42 sys: 2.13 Warning: stderr Fatal error: out of memory. ** Result for A019.litmus ** status: 2 real: 10988.84 user: 10985.68 sys: 2.26 Warning: stderr Fatal error: out of memory. ** Result for A009.litmus ** status: 2 real: 10989.95 user: 10987.18 sys: 1.91 Warning: stderr Fatal error: out of memory. ** Result for A150.litmus ** Test A150 Allowed States 7 1:r1=0; [x]=1; [z]=1; 1:r1=0; [x]=1; [z]=2; 1:r1=0; [x]=2; [z]=1; 1:r1=0; [x]=2; [z]=2; 1:r1=1; [x]=1; [z]=1; 1:r1=1; [x]=1; [z]=2; 1:r1=1; [x]=2; [z]=1; No (allowed not found) Condition exists ([x]=2 /\ [z]=2 /\ 1:r1=1) Hash=4e004ab91a29a596a6d336e1b1fc7755 Cycle=Rfe DpDatadW Wse LwSyncdWW Wse SyncdWW Relax A150 No Safe=Wse BCSyncdWW LwSyncdWW DpDatadW Prefetch=0:x=F,1:z=W,2:z=F,2:x=W Com=Rf Ws Ws Orig=SyncdWW Rfe DpDatadW Wse LwSyncdWW Wse Observation A150 Never 0 7 status: 0 real: 11026.96 user: 11024.03 sys: 1.90 ** Result for A151.litmus ** status: 2 real: 11157.73 user: 11154.97 sys: 1.74 Warning: stderr Fatal error: out of memory. ** Result for A149.litmus ** status: 2 real: 11172.56 user: 11169.60 sys: 1.93 Warning: stderr Fatal error: out of memory. ** Result for A093.litmus ** status: 2 real: 11311.57 user: 11308.86 sys: 1.69 Warning: stderr Fatal error: out of memory. ** Result for A025.litmus ** status: 2 real: 11318.00 user: 11312.80 sys: 1.77 Warning: stderr Fatal error: out of memory. ** Result for A005.litmus ** status: 2 real: 11675.47 user: 11672.44 sys: 1.95 Warning: stderr Fatal error: out of memory. ** Result for A098.litmus ** status: 2 real: 11726.26 user: 11723.25 sys: 1.93 Warning: stderr Fatal error: out of memory. ** Result for A031.litmus ** status: 2 real: 13129.79 user: 13126.66 sys: 1.95 Warning: stderr Fatal error: out of memory. ** Result for A119.litmus ** status: 2 real: 13572.79 user: 13569.74 sys: 1.83 Warning: stderr Fatal error: out of memory. ** Result for A120.litmus ** status: 2 real: 13615.40 user: 13612.37 sys: 1.81 Warning: stderr Fatal error: out of memory. ** Result for A107.litmus ** status: 2 real: 13963.95 user: 13960.82 sys: 1.89 Warning: stderr Fatal error: out of memory. ** Result for A122.litmus ** status: 2 real: 14014.76 user: 14011.71 sys: 1.80 Warning: stderr Fatal error: out of memory. ** Result for A123.litmus ** status: 2 real: 14369.72 user: 14366.13 sys: 2.11 Warning: stderr Fatal error: out of memory. ** Result for A105.litmus ** status: 2 real: 15193.35 user: 15190.05 sys: 1.92 Warning: stderr Fatal error: out of memory. ** Result for A021.litmus ** status: 2 real: 15376.19 user: 15372.66 sys: 2.10 Warning: stderr Fatal error: out of memory. ** Result for A027.litmus ** status: 2 real: 15533.03 user: 15526.86 sys: 1.85 Warning: stderr Fatal error: out of memory. ** Result for A104.litmus ** status: 2 real: 15977.53 user: 15973.83 sys: 2.26 Warning: stderr Fatal error: out of memory. ** Result for A101.litmus ** status: 2 real: 16159.42 user: 16155.46 sys: 2.25 Warning: stderr Fatal error: out of memory. ** Result for A020.litmus ** status: 2 real: 16299.62 user: 16296.32 sys: 1.97 Warning: stderr Fatal error: out of memory. ** Result for A026.litmus ** status: 2 real: 16374.15 user: 16367.47 sys: 2.17 Warning: stderr Fatal error: out of memory. ** Result for A100.litmus ** status: 2 real: 16702.17 user: 16698.70 sys: 1.94 Warning: stderr Fatal error: out of memory. ** Result for A141.litmus ** status: 2 real: 20738.15 user: 20734.66 sys: 1.74 Warning: stderr Fatal error: out of memory. ** Result for A140.litmus ** status: 2 real: 20954.25 user: 20949.46 sys: 2.36 Warning: stderr Fatal error: out of memory. ** Result for A148.litmus ** status: 2 real: 21321.20 user: 21317.38 sys: 1.86 Warning: stderr Fatal error: out of memory. ** Result for A143.litmus ** status: 2 real: 21461.02 user: 21456.43 sys: 2.21 Warning: stderr Fatal error: out of memory. ** FINI **