herd models vs. Power hardware, atomic instructions

This notes compares the herd models models for load-reserve and store-conditional instructions. Herd models are the default “atomic” model power.cat. and an experimental model exp.cat. Those two models are refinements of our power model, the first, default, “atomic” model performs a change of preserved-program-order; while the second model performs a change of the propagation check.

Notice that ppcmem does not always terminate in the allocated time and memory bounds, so that these comparisons do not cover all our test set. In effect, we have ppcmem output for 11088 tests out of 13963.

• Comparison with operational model
  • More behaviours
  • Less behaviours
• Comparison with herd experimental Power model
  • More behaviours
  • Less behaviours
• Comparison of herd experimental Power model with operationnal model
  • More behaviours
  • Less behaviours
• Comparison with Power hardware
  • Invalid behaviours, herd model
  • Invalid behaviours, experimental model

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