Classification of the invalid executions of the less relaxed model

In this note we classify the execution that are forbidden by the “less relaxed model” lessrelaxed.cat, yet observed on hardware, or invalid executions. We use the classification of invalid states of the original model defined here.

The following two tables give the number of invalid tests and executions by batch. For instance the S batch gathers 3853 tests (4945246 executions), of which 15 (144 executions) invalidate the ARM llh model. One may observe that the sum of batch size as number of executions (Row “Sum”) equals the number of all invalid executions (Row “All” in the right table below).

Number of tests
 BatchInvalid
ALL 5697 33
S 3853 15
T 974 0
O 0 0
P 2239 0
ST 1043 0
SO 622 5
SP 1708 3
TO 0 0
TP 96 0
OP 934 21
STO 174 0
STP 35 0
SOP 1060 9
TOP 1 0
STOP 103 0
Sum1284253
        
Number of executions
 BatchInvalid
ALL 14028679 1160
S 4945246 144
T 7410 0
O 0 0
P 8841 0
ST 304893 0
SO 2727028 16
SP 242404 10
TO 0 0
TP 149 0
OP 9595 460
STO 99767 0
STP 1945 0
SOP 5378232 530
TOP 1 0
STOP 303168 0
Sum140286791160

The ALL table gathers all invalid executions, with links to the relevant, more specific, batches on a test by test basis.

We also give table of invalid executions for specific architecture, namely Tegra3 and Exynos4412.


This document was translated from LATEX by HEVEA.