Introduction

• A typical table of results
• Hand-written tests
• Experiment report

A typical table of results

The following table is the same as the one given in the paper. Other tables in this document have a similar structure,

• The first column lists tests, with hyperlinks to test (assembly) source code and, sometimes a diagram that describes the targeted execution, or behaviour. Note that a test is essentially a particular behaviour of a program (the source code together with an initial state and a constraint on the final state that picks out a single execution of interest), not the program only.
• The second column list kinds. The kind of a test is Allow (behaviour allowed), Forbid (behaviour forbidden) or — (no opinion). How kinds are fixed depends on the series considered; most of the time kinds are taken from model output.
• The third column list model output, condensed as an Allow/Forbid statement, written “=” when equal to the test kind defined in the previous column. When the executable model did not terminate in the allocated memory space (at most 16Gb), this cell contains “—”.
• The remaining columns list hardware experiment output, condensed as Ok/No, showing whether experiments agree with the kind or not, together with the number of occurrences of the behaviour found over the total number of runs of the considered test.

Generally, we ran a test as long as its behaviour remains unobserved. This, and the differences as regards speed and core numbers of the tested machines, explains why number of runs vary from test to test.

Overall, for an unobserved behaviour, the number of runs is at least 91M (91 · 10⁶) for PowerG5, 1.2G (1.2 · 10⁹) for Power6 and 2.6G (2.6 · 10⁹) for Power7, and often more.

Hand-written tests

The “RSV” tests are basic checks of lwarx/stwcx. semantics.

The first three tests, RSV+FAIL+SIMPLE, RSV+FAIL and RSV+SPC0 are of interest, as they illustrate the reservation granule issue — see p. 663 in Power ISA. Namely, reservations are held on aligned memory chunks whose size is unspecified by the architecture.

Consider for instance the simplest test, RSV+FAIL+SIMPLE: the test performs a load reserve (lwarx) from some location y and then attempt a store conditional (stwcx.) to a different location x. The execution of interest of this test is when the store conditional succeeds:

In our model the size of the reservation granule is word size. As a result, our model forbids the execution above (i.e. the store conditional never succeeds). However, we tested machines whose reservation granule is larger that a word (typically a cache line size, i.e. 128 bytes). As a result we observe the execution above, when the addresses of locations x and y are close enough one to the other, so that they are in the same reservation granule.

The remaining “PPO” tests are variations of PPOCA (and of PPOAA). Test PPOCA is MP with a complex second thread:

(a):Ry0 -control-> (b):Wx1 -> (c):Rx1 -addr-> (d):Rz0

Among those, test PPO+CXA replaces the load (c) by a lwarx, while tests PPO+CA+A and PPO+CA+B replace the store (b) by a stwcx., with the companion lwarx being far apart or just before. All these PPO… variations are forbidden by the model and unobserved.

Experiment report

Taking all tests together is 13963 tests. Our model exploration tool terminated in less then 16GB memory for 11029 tests¹. We checked that simulator output, when available, is not contradicted by hardware.

Namely, our simulator execute OCaml code derived from lem formal specifications. As a result, the simulator can be trusted to follow model specifications. However, our executable code is not optimised for speed and the simulators do not always terminate in decent time or memory space on input that features three processors or more, complex code sequences, or numerous memory accesses.

We thus resort to distributed execution of the simulators on two clusters of AMD opteron and Intel Xeon processors. Overall we have more than 650 cores available, which we share with other users. Our experiments lasted weeks and consist in repetitively running the simulator on the complete test base under increasing processor time and memory usage limits.

The following table accounts for our simulator experiments:

The “N” column shows how many tests finally completed successfully in the allocated processor time and memory limits. We also give a few statistics: the “avg” (resp. “geom”) column shows the arithmetic (resp. geometric) mean of successful runs; while the “max” column show the time of the test that takes longer to complete successfully (here 33.3 hours). This test is Z6.1+rfipr-datarp+lwsync+data:

The “effort” column shows the total CPU time allocated to simulator runs (including failed runs due to intentional resource limits): the total computing effort amounts to about 3317 days of machine time. Finally, the “memory” column shows the maximum memory limit we used.