The Phat Experiment

Abstract: We ran The Phat Experiment from December 2009 to January 2010. We tested 3 Power machines with our diy tool. We present here the experimental protocol and results.

1  Experimental Protocol

1. Make a directory exp, with a sub-directory src for sources. We provide the sources of our tests as the archive src.tgz. Those tests were produced with the diy tool from configuration files that are present in the archive.
2. The structure of the src sub-directory is as follows:
   • plain for the plain relaxations, sub-divided in: podrr, podrw, podwr, posrr, rfe, rfi;
   • nc for the barriers relaxations involving no cumulativity, sub-divided in: lwdwr, lwswr;
   • ac for the barriers relaxations involving A-cumulativity; aclwdrr aclwsrr;
   • bc for the barriers relaxations involving B-cumulativity. bclwdww, bclwsww;
   • safe, for all the other relaxations to be tested, i.e.:
     • dpdr, dpdw, dpsr, dpsw, fre, fri, wse, wsi;
     • lwdrr, lwdrw, lwdww, lwsrr, lwsrw, lwsww, sdrr, sdrw, sdwr, sdww, ssrr, ssrw, sswr;
     • aclwdrw, aclwsrw acsdrr acsdrw acssrr acssrw;
     • bclwdrw, bclwsrw, bcsdrw, bcsdww, bcssrw bcssww.
     Notice that the names of leaf directories reflect the names of relaxations, in lowercase, with LwSync being replaced by lw and Sync being replaced by s. For instance sdrw stands for SyncdRW.

     Tests in plain, nc, ac and bc are allowed to yield Ok, thereby confirming our hypothesis on the relaxations of the Power architecture. We call the corresponding relaxations expected relaxations.

     By contrast, tests in safe should never yield Ok. We call the corresponding relaxations non-relaxations.

     Reflecting that aim, expected relaxation are tested individually, while non-relaxations are tested together. See the example of X86 in diy manual.

3. Make the same directory hierarchy as the one of src in each of the machine sub-directories. In each leaf directory, make a symbolic link to the corresponding source directory. This way, litmus can be run as litmus src/@all…
4. For a given machine, create a file rem that initially lists all the leaf directories. One complete run is a (litmus) run of all the tests in rem.
5. After each complete run, check the output logs (we provide a simple tool readRelax). If a relaxation is confirmed, remove the corresponding line from rem.
6. The parameters of litmus have been previously tuned so that most expected relaxations are confirmed after the first complete run. We run a total of about 10 complete runs.

During our experiment on hpcx, some tests in safe yielded Ok — see Sec. 2.2. We then followed a different procedure — see Sec. 5

2  Summary of the experimental results

2.1  Relaxations observed on squale, vargas and hpcx

When a relaxed relaxation is confirmed, the array cell above holds a link to the log of one run of one litmus test that confirms the relaxation. The cell also shows the number of outcomes that yielded Ok/total number of outcomes, for the selected log.

When a relaxed relaxation is not confirmed, the array cell holds 0/total number of outcomes for all tests of all performed complete runs.

2.2  Anomalies observed on hpcx

Incidentally, those anomalies explain why we selected such a high number of outcomes per run for hpcx.

3  Detailed results on squale (Power 5)

3.1  Description of the machine

squale is a PowerPC G5 with 4 cores, running Mac Os X (a Power Mac G5).

3.2  Plain relaxations

When an expected relaxation is confirmed, the relevant line in the table above gives the number of Ok states observed (and the number of outcomes collected) for a few typical tests, with a link to the complete litmus log of the run that yielded Ok. When an expected relaxation is not confirmed, we rather give the total number of outcomes collected for this relaxation, and links to all logs. This number may vary a lot, since it critically depends on the number of tests produced by diy. See for instance ACLwSyncsRR and ACLwSyncdRR below.

We notice that no relaxation of Rfe is observed.

3.3  Barriers relaxations

3.4  A-Cumulativity relaxations

Not observing expected cumulativity relaxations is compatible with the result of experiments on Rfe.

3.5  B-Cumulativity relaxations

Again, we did not observed the expected cumulativity relaxations.

3.6  Safe (non)-relaxations

The nouts entry above counts the total number of final states (or outcomes) collected for a given test in safe. The number of outcomes varies from test to test, depending on the number of threads in the test. It also varies from log to log due to changes in litmus parameters. This number is to be compared to the number of outcomes needed to observe a relaxation (typically a few millions).

The last column shows the total number of outcomes collected.

4  Detailed results on vargas (Power 6)

4.1  Description of the machine

vargas is a Power 6 with 112 nodes of 32 cores. The operating system is AIX. We run our experiments on one node, i.e. on 32 cores.

4.2  Plain relaxations

Our experiments do not confirm PodRR, which is confirmed on Power 5. This may be related to Power 6 being more in-order.

4.3  Barriers relaxations

4.4  A-Cumulativity relaxations

It is to be noticed that the test aclwdrr010 is iriw with lwsync.

4.5  B-Cumulativity relaxations

4.6  Safe (non)-relaxations

The nouts entry above counts the total number of final states (or outcomes) collected for a given test in safe. The number of outcomes varies from test to test, depending on the number of threads in the test. It also varies from log to log due to changes in litmus parameters. This number is to be compared to the number of outcomes needed to observe a relaxation (typically 16–32 millions).

5  Detailed results on hpcx (Power 5)

Due to the discovery of relaxations that do not follow our Power model, we have altered our procedure:

• We separate the safe set into three subsets: A-cumulativity, B-cumulativity and plain.
• We test cumulativity relaxations individually.
• We test the safe plain relaxations as a whole.

As a result, we find anomalous relaxations for A-cumulativity, and none for B-cumulativity nor safe plain. Thus, we may venture to assume that the problem originates in either our model of A-cumulativity, or in hpcx implementation of A-cumulativity.

5.1  Description of the machine

hpcx is a Power 5 with 160 nodes of 16 physical cores. The operating system is AIX. We run our experiments on one node, i.e. on 16 cores, with the possibility to enable SMT.

5.2  Plain relaxations

5.3  Barriers relaxations

5.4  A-Cumulativity relaxations

We confirm expected relaxations.

All the remaining cases of A-cumulativity are anomalously relaxed.

5.5  B-Cumulativity relaxations

We easily confirm the expected relaxations involving the B-cumulativity of lwsync.

None of the remaining cases of B-cumulativity is observed to be relaxed.

5.6  Safe (non)-relaxations

The safe set is restricted to plain relaxations.

6  PodRW is relaxed

To confirm the relaxation of PodRW, which our models predicts, we used an advanced feature of diy: composite relaxations. Namely, the configuration file podrwposwr.conf sets the relax list to [PodRW,PosWR]. That is, PodRW followed by PosWR.

Observe that PosWR is not safe, hence absent from the cycles of standard experiments on PodRW. The litmus tests are in podrwposwr.

The experiments show the sequence “PodRW followed by PosWR” to be relaxed on squale and hpcx. If PodRW was not relaxed, then PodRW followed by PosWR would not be either, by the definition of preserved programming order we give in the associated paper. As the sequence is observed to be relaxed, we consider that PodRW is observed to be relaxed.

References

[1]

H.-J. Boehm and S.V. Adve. Foundations of the C++ concurrency memory model. In Proc. PLDI, 2008.

[2]

Power ISA Version 2.06. 2009.

3

See Sec. 6 for detailed explanations.

1

This test makes use of BCSyncdWW, which has not been observed to be relaxed, thus is considered as safe.

2

We enabled SMT for this test.

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