Comparing hardware with the model

• Invalid behaviours
• Behaviours allowed by the model and not observed

Model is NEW.cat.

As no behaviour that the model forbids is observed, our model is not invalidated by experiments and can be considered validated by experiments. Furthermore, there are very few (64 tests in a test suite of 2208 tests) behaviours that the model predicts and that are not observed.

Invalid behaviours

Behaviours allowed by the model and not observed

We separate those behaviours into non-SC (53 tests) and SC ones (11 tests).

• Non-SC behaviours all correspond to tests that comprise the clflushopt instruction. Those not being observed on hardware suggests that the tested hardware implementation of the clflushopt is stronger than its specification.
• The non-observed SC behaviours are difficult to observe, as they stem form tight interleaving of threads which do not occur frequently in practice.