x86 litmus testing: results *************************** We summarize here the results we obtained. We experimented with different benchmark configurations on several machines: -riob Dual-Core AMD Opteron(tm) Processor 2220 (4 cpus) -patate Quad-Core AMD Opteron(tm) Processor 8356 (4 cpus) -asie Intel(R) Xeon(TM) CPU 3.06GHz HT (2 cpus) -optic Intel Intel(R) Core(TM)2 Quad CPU (1 cpu ) A * on a line for a "forall" or "not exists" test means that there was no violation of the constraint specified in the test. A "found a witness" on a line for an "exists" test means that there was a witness of an execution satisfying the constraint specified in the test. A "no witness" on such a line means that no witness was found. The summary of results over all machines is as follows. test_name (in the paper) litmusname constraint ------------------------------------------------------------------------------------------ iwp2.1/amd1 test.intel.1.litmus not exists * iwp2.2/amd2 test.intel.2.litmus not exists * iwp2.3.a/amd4 test.intel.3-a.litmus exists found a witness amd5 test.amd5.litmus not exists * n1 test.intel.readspec.litmus exists no witness iwp2.3.b test.intel.3-b.litmus forall * iwp2.4/amd9 test.intel.4.litmus exists found a witness amd10 test.amd10.litmus not exists * iwp2.5/amd8 test.intel.5.litmus not exists * iwp2.6 test.intel.6.litmus not exists * amd6 test.amd.stores.litmus exists no witness amd7 test.intel.7.litmus not exists * n3 test.thomas.lock.1.litmus exists no witness iwp2.8.a test.intel.8-a.litmus not exists * iwp2.8.b test.intel.8-b.litmus not exists * n2 test.n2.litmus not exists * A more detailed summary, per machine-run, is below. Informations about the settings, and the actual test run in each case can be found in the files asie, patate, patate2, etc. asie patate patate2 riob -------------------------------------------------------------------------------------------------------------------- test.intel.1.litmus not exists * * * * test.intel.2.litmus not exists * * * * test.intel.3-a.litmus exists found a witness _no witness_ found a witness found a witness test.amd5.litmus not exists * * * * test.intel.readspec.litmus exists _no witness_ _no witness_ _no witness_ _no witness_ test.intel.3-b.litmus forall * * * * test.intel.4.litmus exists found a witness _no witness_ found a witness found a witness test.amd10.litmus not exists * * * * test.intel.5.litmus not exists * * * * test.intel.6.litmus not exists * * * * test.amd.stores.litmus exists _no witness_ _no witness_ _no witness_ _no witness_ test.intel.7.litmus not exists * * * * test.thomas.lock.1.litmus exists _no witness_ _no witness_ _no witness_ _no witness_ test.intel.8-a.litmus not exists * * * * test.intel.8-b.litmus not exists * * * * test.n2.litmus not exists * * * * patate3 optic asie2 asie3 -------------------------------------------------------------------------------------------------------------------- test.intel.1.litmus not exists * test.intel.2.litmus not exists * test.intel.3-a.litmus exists found a witness found a witness test.amd5.litmus not exists * * test.intel.readspec.litmus exists _no witness_ _no witness_ _no witness_ _no witness_ test.intel.3-b.litmus forall * test.intel.4.litmus exists found a witness found a witness test.amd10.litmus not exists * * test.intel.5.litmus not exists * test.intel.6.litmus not exists * test.amd.stores.litmus exists _no witness_ _no witness_ _no witness_ _no witness_ test.intel.7.litmus not exists * test.thomas.lock.1.litmus exists _no witness_ _no witness_ _no witness_ _no witness_ test.intel.8-a.litmus not exists * test.intel.8-b.litmus not exists * test.n2.litmus not exists * * * * Correspondence ************** The test names in the paper corresponds to test files as follows. test name (in the paper) litmusname --------------------------------------------------------------------- iwp2.1/amd1 test.intel.1.litmus iwp2.2/amd2 test.intel.2.litmus iwp2.3.a/amd4 test.intel.3-a.litmus amd5 test.amd5.litmus n1 test.intel.readspec.litmus iwp2.3.b test.intel.3-b.litmus iwp2.4/amd9 test.intel.4.litmus amd10 test.amd10.litmus iwp2.5/amd8 test.intel.5.litmus iwp2.6 test.intel.6.litmus amd6 test.amd.stores.litmus amd7 test.intel.7.litmus n3 test.thomas.lock.1.litmus iwp2.8.a test.intel.8-a.litmus iwp2.8.b test.intel.8-b.litmus n2 test.n2.litmus Installation *********** - Requires ocaml - "make" in litmus/plumbing/ (and "make" in memevents/ first) Usage ***** With small disk space /WeakMemory/litmus$ plumbing/litmus -x86 -o machinename -bench config/bench1000.h -suffix -machinename x86/* With huge disk space /WeakMemory/litmus$ plumbing/litmus -x86 -o machinename -bench config/bench10000.h -suffix -machinename x86/* Temporary files are created in the calling directory, and take some space The configuration files in config/ can be tweaked to influence the results obtained.