Lazy POP operational model vs. models and hardware

This note gathers variout comparisons of models.

• “Lazy” is ppcmem with options -pop true -model lazy.
• “Pop” is ppcmem with options -pop true.
• “Flowing” is ppcmem with options -flowing true -topauto true.
• “Model” is herd default (Power) model.
• “ARM-Model” Our herd model relaxed to handle legitimate relaxed behaviours observed on hardware.

Other models may appear in tables:

• Our old ppcmem run (column “PLDI11”);
• A more recent ppcmemrun¹ (column “Op”).
• Our herd Qualcomm model, a model in-between the default (Power) and ARM model, that account for the specific behaviours observerd on this vendor’s processors (column “Q”).

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 6755 tests out of 7309. 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 previous run
  • More behaviours
  • Less behaviours
• Comparison with the Pop model
  • More behaviours
  • Less behaviours
• Comparison with the flowing model
  • More behaviours
  • Less behaviours
• Comparison with herd default model
  • More behaviours
  • Less behaviours
• Comparison with herd ARM model
  • More behaviours
  • Less behaviours
• Comparison with ARM hardware
  • Invalid behaviours

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