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

This document was translated from LATEX by HEVEA.