Flowing operational model vs. non-flowing operational model |
This note compares two version of the operational model (ppcmem).
-flowing true -topauto true
(“Flowing” model).
-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:
The tables also include hardware runs results (column “PLDI11”). 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.
Flowing | Op | Model | ARM-Model | PLDI11 | ARM | |
MP+dmb+fri-rfi-ctrlisb | Allow | Forbid | Forbid | Allow | Forbid | Ok, 153k/193G |
MP+dmb+data-wsi-rfi-ctrlisb | Allow | Forbid | Forbid | Allow | — | No, 0/113G |
Allow unseen | ||||||
MP+dmb+fri-rfi-pos-ctrlisb | Allow | Forbid | Forbid | Allow | — | Ok, 50k/95G |
MP+dmb+fri-wsi-rfi-ctrlisb | Allow | Forbid | Forbid | Allow | — | Ok, 86k/122G |
MP+dmb+pos-fri-rfi-ctrlisb | Allow | Forbid | Forbid | Allow | — | Ok, 13/97G |
PPO015 | Allow | Forbid | Forbid | Allow | Forbid | No, 0/99G |
Allow unseen | ||||||
MP+dmb+data-wsi-rfi-pos-ctrlisb | Allow | Forbid | Forbid | Allow | — | No, 0/97G |
Allow unseen | ||||||
ISA2+dmb+fri+addr | Allow | Forbid | Forbid | Allow | — | No, 0/41G |
Allow unseen | ||||||
MP+dmb+fri-rfi-ctrlisb+BIS | Allow | Forbid | Forbid | Allow | — | Ok, 29/31G |
This document was translated from LATEX by HEVEA.