Classification of the invalid executions of the ARMv8 model

In this note we classify the execution that are forbidden by the ARMv8 model and yet observed on hardware, or invalid executions. It is important to notice that invalid executions that can result from read-to-read hazards are not considered here, as they are listed elsewhere.

We use the classification of invalid states defined here in the case of the ARMv7 model. Principles are identical but models are different: for analysis purpose, we add sca (single-copy-atomicity) and mca (muti-copy-atomicity) conditions to the ARMv8 model, yielding four conditions of interest:1 single-copy-atomicity (sca) “S”, multi-copy-atomicity (mca) “M”, internal “I” and external “E.

  irreflexive co;si;co;si as sca
  irreflexive rf;si;fr;si as sca
  ...
  acyclic (co|rfe|fr);si as mca
  ...
  acyclic po-loc | fr | co  | rf as internal
  ...
  irreflexive ob as external
  ...

The external condition is not detailled — see the Cat model.

From experiments we have found a set of 268 tests that have exhibited some forbidden behaviours. We partition all forbidden executions of those into batches according to the (exact) conditions that reject them. Notice that we define 15 batches as we consider combinations of conditions. Further notice that some of these batches are empty, as failing to pass some condition (e.g.S”) entails failing a more stringent one (e.g.E”). We then distribute observed invalid executions amongst batches, thereby achieving some level of automatic classification that we complete by visual examination.

The following two tables give the number of invalid tests and executions by batch. For instance 195 tests (245 executions) amongst the 267 tests (2732 executions) of the SME batch contradict the ARMv8 model. One may observe that the sum of batch size as number of executions (Row “Sum” in the table on right) equals the number of all invalid executions (Row “All” in the right table below). Due to some tests exhibiting several invalid executions, this is not the case for the table on the left.

Number of tests
 Invalid
ALL268
I0
S0
M0
E1
IS0
IM0
IE0
SM0
SE0
ME72
ISM0
ISE0
IME0
SME195
ISME0
Sum268
      
Number of executions
 Invalid
ALL333
I0
S0
M0
E1
IS0
IM0
IE0
SM0
SE0
ME87
ISM0
ISE0
IME0
SME245
ISME0
Sum333

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

Hand classification

According to the above automatic classification, invalid executions fall into three classes. As close examination of each class suggests and the execution counts below confirm, all the executions in a given class have a particular, relatively simple, cycle in common. More precisely:


1
We ignore the atomicity condition, which is irrelevant here.

This document was translated from LATEX by HEVEA.