(New) Operational model vs. Power hardware and axiomatic model

Models are as follows:

• “Op.New” is pccmem with no option.
• “Op.Strong” is pccmem with option -model strong_barrier_coherence.
• “Model” is the default herd Power model.
• “Op” is a december 2013 run of pccmem with option -model restart_on_read_satisfy.
• “PLDI11” is a old ppcmem run.

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 4378 tests for “Op.New” and 5817 tests for “Op.Strong” out of 8144.

• Comparison with Power hardware
  • Invalid behaviours
  • Unseen behaviours
• Comparison with Power model
  • More behaviours
  • Less behaviours
• Regression with respect to Op
  • More behaviours
  • Less behaviours
• Comparison with Op.Strong
  • More behaviours
  • Less behaviours
• Regression with respect to PLDI11
  • More behaviours
  • Less behaviours

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