Invalidation of X86-CC+fences

In this note we show the usage of our tools to prove that X86-CC+fences is not a valid memory model of x86 machines.

Generating tests

We generate tests whose outcome is observed in the TSO model. To that aim we use diy, with the following configuration file A.conf:

-arch X86
-name A
-safe PodR*,PodWW,MFenced**,Rfe,Fre,Wse
-relax [Rfi,PodRR],PodWR
-nprocs 2
-size 8

That is, we generate some tests that may exhibit relaxed behaviour on a TSO machine.

% diy -conf A.conf 
Generator produced 13 tests
Relaxations tested: {[Rfi,PodRR]} {PodWR}

In pratice, we generate 13 tests with names ranging from A000 to A012.

Finding tests forbidden by X86-CC+fences

We run our simulator memevents on the tests above, selecting the X86-CC+fences model (-model cc below), saving the output for later analysis:

% memevents -model cc src/@all > A.M

Reading A.M reveals that four tests are forbidden: A003.litmus, A004.litmus, A007.litmus, A008.litmus. We list them in the index file @cc-forbidden. Those four tests are conveniently described by their cycles:

Running the forbidden tests

We run the tests on chianti a modern AMD64 machine that features 8 cores and 2-way hyperthreading. We first compile the tests with litmus, with appropriate parameters (configuration file chianti.cfg):

% mkdir run
% litmus -mach chianti -o run @cc-forbidden

Then we compile litmus output and run the tests twice, disabling affinity control during the second run:

% cd run
% make
% sh run.sh > ../A.00
% sh run.sh -i 0 > ../A.01

All outcomes forbidden by X86-CC+fences are observed, as can be found by looking at log files A.00 and A.01. The following table sumarises the situation:

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