Flowing operational model vs. herd model and hardware, atomic instructions

This notes compares herd and ppcmem models for load-reserve and store-condtional instructions.

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 124 tests out of 130. Also notice that, at the moment, we refrain from comparing models on tests that feature the .st qualified fences, for the sake of simplicity.

• Comparison with herd ARM model
  • More behaviours
  • Less behaviours
• Comparison with herd experimental ARM model
  • More behaviours
  • Less behaviours
• Comparison with ARM hardware
  • Invalid behaviours
  • Unseen behaviours

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