Comparing two Power models

This document shows tables for the “Comparing two Power models” experiments. The models we compare are:

• Power2010, the axiomatic, global time style, model introduced in our article “Fences in Weak Memory Models”. There exists an executable version of this model, which is not released yet.
• Power2011, the operational model introduced in our article “Understanding POWER Multiprocessors”. In experiments we used the off-line version of ppcmem, an executable version of Power2011.

We used our toolset, including the automated front-end dont, to find tests that show that the two models are not comparable. Namely, behaviours exist that are allowed by one model and forbidden by the other.

As all such behaviours are unobserved on PowerG5, Power6 and Power7 machines. Both models remain experimentally valid.

Behaviours forbidden by Power2010, allowed by Power2011

In a previous experiment, we have explored Power2010, yielding a particular safe set. By definition, all tests built from those candidate relaxations are forbidden by Power2010. We now use dont in conformance mode to run ppcmem the (off-line) executable version of Power2011 on all such tests up to three processors.

The procedure finally yields five tests allowed by Power2011 and forbidden by Power2010, as shown immediately by the experiment log. See a complete description of the experiment. We give names to those five tests, following the scheme introduced in “Understanding POWER Multiprocessors” and summarised in this document. We then run them on Power machines (or benefit from previous runs, some of the tests being already known to us), resulting in the following table:

The table above reminds the Allow/Forbid status of the tests according to the two models. It also shows how many times the targeted behaviour has been observed on hardware and how many time a test has been run. For instance 0/2.1G means that no observation occured out of about 2.1 × 10⁹ runs of a given test performed on a given implementation.

Strictly speaking, only the last test Z6.3+lwsync+sync+ctrlisync is new. However our tool set proved useful, enabling a painless generation of some tests forbidden by Power2010, and the automation of checking the result of running ppcmem on those.

Behaviours allowed by Power2010, forbidden by Power2011

One can now expect that we explore Power2011 by using dont, deduce forbidden behaviours and check with dont that Power2010 allows some of those. Unfortunately, it does not works, as the prototype ppcmem is two slow and consumes too much memory to withstand a complete exploration in an acceptable time.

Fortunately, the exploration of Power2010 already yielded a bunch of observed behaviours as a by product. Hence, we proceed in the opposite direction. Namely, we simply run ppcmem on those tests, with decent time and memory limits (complete run log), and then select amongst tests that has terminated those that did not produced the targetted behaviour — using the “Observation name Never” information present in logs.

The procedure yields 197 tests that we rename according to our systematic scheme and shall now comment. In this discussion we refer to the “architectural intent”. As Power2011 was designed with help from IBM, we claim it to be close to “architectural intent”. By contrast, Power2010 was designed from black box experiments. However, Power2011 does not, in our opinion, supersedes Power2010, as being still valid valid after two years of intensive experiments on hardware, and given its simplicity, which proves beneficial in applications such as automatic fence insertion.

Simple tests

The MP (message passing) and WRC (write to read causality) tests correspond to known programming idioms. From our understanding, the architectural intent commands that “minimal” protection (the lightweight barrier lwsync and dependencies) suffices.

As demonstrated by the run counts above, implementations follow the architectural intent, to the best of our knowledge.

The following two series are vaguely similar to MP and WRC, but are not claimed to be related to significant programming idioms. Nevertheless, a model has to handle any situation, and here again “minimal” protection suffices.

A new familly of tests

We notice the presence of a previously unknown to us and thus untested familly of tests: W+RW+RW+RR, an extension of WRC (which can be spelled out as W+RW+RR). One may remark that, again, minimal protection suffices, as shown for instance by the first test below:

“Out of thin air”-like tests

Any “causal” cycle must be rejected by a realistic model. Power2010 defines such a cycle by a combination of read to write (data or control dependency) and of Rf (the relation from a write to any read that takes its value from it).

The prototype of a test that exhibit such a causal dependency is LB+addrs (load buffer, with address dependencies):

PPC LB+addrs "DpAddrdW Rfe DpAddrdW Rfe" Cycle=Rfe DpAddrdW Rfe DpAddrdW { 0:r2=x; 0:r5=y; 1:r2=y; 1:r5=x; } P0 | P1 ; lwz r1,0(r2) | lwz r1,0(r2) ; xor r3,r1,r1 | xor r3,r1,r1 ; li r4,1 | li r4,1 ; stwx r4,r3,r5 | stwx r4,r3,r5 ; exists (0:r1=1 /\ 1:r1=1)

The following tests are variations on LB and 3.LB (the three processor extension of LB) which suggests that pure dependencies can be supplemented with read to write and write to write memory accesses to the same location and by the same processor (Fri and Wsi). Namely, in “causal” loops, data, address and control dependencies do not fully account for the natural ordering constraints that core designers follow.

Remaining tests

We give the classified remaining tests for completeness.

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