New operational model vs. Power hardware and model

This note gathers two sets of comparison tables:

• Comparing ppcmem, with option -model restart_on_read_satisfy (“Op” model) and our herd model (column “Model”). We also show our old ppcmem run (column “PLDI11”).
• Comparing ppcmem, with option -model restart_on_read_satisfy (“Op” model) and experiments on Power hardware.

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 5972 tests out of 8121.

• Comparison with Power model
  • More behaviours
  • Less behaviours
• Comparison with Power hardware
  • Invalid behaviours
  • Unseen behaviours

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