Comparing the proposed ARM model with hardware

In this document, we compare our proposed ARM model (column “ARM” in tables) with hardware (column “Hardware” in tables). This model arm.cat features a relaxed preserved program order, were we have omitted po-loc from the cc0 component of the definition of ppo.

To avoid the noise due to the read-after-read hazard bug, we restrict the comparison to behaviours that cannot result from executions that include a po-loc; fr; rf cycle. However, there are still invalid behaviours, which we have characterized elsewhere as likely bugs of some chips.

• Forbidden by model, observed on hardware
• Allowed by model, unobserved on hardware

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