Up Next

Description of experiments

Simulators

We compare the output of two simulators: (1) ppcmem (in this note “Operational”) the model introduced in Understanding POWER Multiprocesors, and (2) “Axiom”, an implementation of the proposed axiomatic model that re-uses ppcmem front-end.

Base of tests

Our present test base results from aggregating several test bases:

As a result, the present test base includes 4503 tests. We provide an archive of all test sources which are valid input for the simulator ppcmem and litmus, a tool to run tests on hardware. We give synthetic model output (Allow/Forbid) for all tests as the kind file k.txt.

Most of our tests are produced by one of the generators of the diy tool suite from cycles of candidate relaxations, a concise and precise mean to describe violations of sequential consistency, and thus relevant tests for memory model testing. The cycles are available for 5544 tests.

Experimental setting

The “Operational” and “Axiom” simulators execute OCaml code derived from lem formal specifications. As a result, the simulators 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 500 cores available, which we share with other users. Our experiments lasted weeks and consist in repetitively running the simulators on the complete test base under increasing processor time and memory usage limits. The following table accounts for our experiments:

 Navg (sec.)geom (sec.)max (sec.)effort (days)memory (Gb)
Operational35652562.21126.262.4e+051024.1840.0
Axiom44801394.1420.572.3e+0582.174.0

The “N” column shows how many tests finally completed successfully in the allocated processor time and memory limits. We see that we achieved an (almost) complete run of the “Axiom” simulator. 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.

The “effort” column shows the total CPU time allocated to running the simulators (including failed runs due to intentional resource limits): the total computing effort amounts to 1106.35 days of machine time. Finally, the “memory” column shows the maximum memory limit we used. All together, those figure demonstrate that our implementation of “Axiom” is one order of magnitude more efficient than the one of “Operational”. As the implementation techniques are similar, we can interpret the result at the model level: “Axiom” is inherently easier to implement efficiently than “Operational”. Also notice that some preliminary experiments suggest the possibility of dramatic efficiency improvements for the “Axiom” model by using SMT/SAT solving.


Up Next