Flowing operational model vs. non-flowing operational model

Contents

• More behaviours
• Less behaviours

This note compares two version of the operational model (ppcmem).

• The flowing model, i.e. options -flowing true -topauto true (“Flowing” model).
• The non-flowing model, i.e. options -flowing false (“Op” model).

Notice other notes compare the flowing model with herd models and the non-flowing model with herd models.

Other models may appear in tables:

• Our herd model (column ”Model”)
• Our herd model relaxed to handle legitimate relaxed behaviours observed on hardware (column “ARM-Model”).
• Our old ppcmem run (column “PLDI11”).

The tables also include hardware runs results (column “ARM”). Notice that those may be unreliable, due to part bugs.

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.

• For the flowing model, we have output for 5891 out of 7309 tests.
• For the non-flowing model, we have output for 5943 out of 7309 tests.

More behaviours

Less behaviours

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