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:¹ 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.

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

• Invalid behaviours in the ALL batch
• Invalid behaviours in the E batch
• Invalid behaviours in the ME batch
• Invalid behaviours in the SME batch

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:

• The 245 invalid executions in class SME match the 245 invalid executions that contain a cycle “si;rfe;si;fre”.
• The 87 invalid executions in class ME match the 87 invalid executions that contain a cycle “si;coi;rfe;si;fre”
• The 1 invalid execution in class E matches the 1 invalid execution that contain a cycle “ fence; rfe ; si; fre”. One may notice that this invalid execution is quite similar to the archetypal SME execution CO-MIXED-20cc, fenced writes to the subparts of some location being replaced by one large write.

1

We ignore the atomicity condition, which is irrelevant here.

This document was translated from L^AT_EX by H^EV^EA.