%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.amd10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* amd10 *)
{x = 0; y = 0};
~exists (%r2 = 0 /\ %r4 = 0);
        P0      |       P1      ;
  mov [x], 1  	|  mov [y], 1  	;
  mfence        |  mfence       ;
  mov %r1, [x] 	|  mov %r3, [y] ;
  mov %r2, [y] 	|  mov %r4, [x] 
Generated assembler
	_litmus_P1_0_: movl $1, (%rdx)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl (%rdx), %edi
	_litmus_P1_3_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, (%rdx)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl (%rdx), %edi
	_litmus_P2_3_: movl x(,%rax,4), %ecx

The constraint not exists r2 = 0 /\ r4 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    98668
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    99171
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    2161



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.amd.3-a
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 3-a: Loads may be reordered with older stores to
  different locations, with MFENCE added on AMD suggestion *)
{x = 0; y = 0};
exists (%r1 = 0 /\ %r2 = 0);
        P0      |       P1      ;
  mov [x], 1  	|  mov [y], 1 	;
  mfence        |  mfence       ;
  mov %r1, [y] 	|  mov %r2, [x] ;
               	|               
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rcx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl y(,%rax,4), %edx
	_litmus_P2_0_: movl $1, y(,%rcx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl x(,%rax,4), %edx

There is no witness of this case : exists r1 = 0 /\ r2 = 0

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,1)    99654
(x,1) (y,1) (%r1,1) (%r2,0)    99973
(x,1) (y,1) (%r1,1) (%r2,1)    373



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.amd.4
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 4 : Intra Processor forwarding is allowed,
    with mfences suggested by AMD*)
{x = 0; y = 0};
exists (%r2 = 0 /\ %r4 = 0);
        P0      |       P1      ;
  mov [x], 1  	|  mov [y], 1  	;
  mfence        |  mfence       ;
  mov %r1, [x] 	|  mov %r3, [y] ;
  mov %r2, [y] 	|  mov %r4, [x] 
Generated assembler
	_litmus_P1_0_: movl $1, (%rdx)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl (%rdx), %edi
	_litmus_P1_3_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, (%rdx)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl (%rdx), %edi
	_litmus_P2_3_: movl x(,%rax,4), %ecx

There is no witness of this case : exists r2 = 0 /\ r4 = 0

Histogram of results

(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    98657
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    99147
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    2196



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.amd5
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* amd5 *)
{x = 0; y = 0};
~exists (%r1 = 0 /\ %r2 = 0);
        P0      |       P1      ;
  mov [x], 1  	|  mov [y], 1 	;
  mfence        |  mfence       ;
  mov %r1, [y] 	|  mov %r2, [x] ;
               	|               
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rcx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl y(,%rax,4), %edx
	_litmus_P2_0_: movl $1, y(,%rcx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl x(,%rax,4), %edx

The constraint not exists r1 = 0 /\ r2 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,1)    99762
(x,1) (y,1) (%r1,1) (%r2,0)    99989
(x,1) (y,1) (%r1,1) (%r2,1)    249



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.amd.stores
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Suggested by AMD, MF thought not possible on non-hyperthreaded archs *)
{x = 0; y = 0; %r1 = 0; %r2 = 0; %r3 = 0; %r4 = 0};
exists (%r1 = 1 /\ %r2 = 0 /\ %r3 = 1 /\ %r4 = 0);
       P0         |        P1       |       P2       |        P3;
   mov [x], 1     |  mov [y],  1    |  mov %r1, [x]  |  mov %r3, [y];
                  |                 |  mov %r2, [y]  |  mov %r4, [x];
                  |                 |                |               
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P2_0_: movl $1, y(,%rax,4)
	_litmus_P3_0_: movl x(,%rax,4), %ecx
	_litmus_P3_1_: movl y(,%rdx,4), %ebx
	_litmus_P4_0_: movl y(,%rax,4), %ecx
	_litmus_P4_1_: movl x(,%rdx,4), %ebx

There is no witness of this case : exists r1 = 1 /\ r2 = 0 /\ r3 = 1 /\ r4 = 0

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    34469
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    2219
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    20071
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    13582
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    22426
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    25430
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    9486
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    758
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    16396
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    5129
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    6490
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    10628
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    7551
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    25365



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.debug.2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(*
Test 1 :  Loads are not reordered with other loads and stores are not
reordered with other stores
*)
{x = 0; y = 0};
~exists (%r1 = 1 /\ %r2 = 0);
        P0      |       P1      ;
  mov [x], 1  |  mov %r1, [y] ;
  mov [y], 1  |  mov %r2, [x];
              |               


Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl y(,%rax,4), %ecx
	_litmus_P2_1_: movl x(,%rdx,4), %ebx

The constraint not exists r1 = 1 /\ r2 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0)    99998
(x,1) (y,1) (%r1,0) (%r2,1)    5
(x,1) (y,1) (%r1,1) (%r2,1)    99997



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(*
Test 1 :  Loads are not reordered with other loads and stores are not
reordered with other stores
*)
{x = 0; y = 0};
~exists (%r1 = 1 /\ %r2 = 0);
        P0      |       P1      ;
  mov [x], 1  |  mov %r1, [y] ;
  mov [y], 1  |  mov %r2, [x];
              |               


Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl y(,%rax,4), %ecx
	_litmus_P2_1_: movl x(,%rdx,4), %ebx

The constraint not exists r1 = 1 /\ r2 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0)    100001
(x,1) (y,1) (%r1,0) (%r2,1)    2
(x,1) (y,1) (%r1,1) (%r2,1)    99997



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(*Test 2 : Stores are not reordered with older loads*)
{x = 0; y = 0};
~exists (%r1 = 1 /\ %r2 = 1);
        P0     |       P1      ;
  mov %r1, [x] |  mov %r2, [y] ;
  mov [y], 1   |  mov [x], 1   ;
               |               
Generated assembler
	_litmus_P1_0_: movl x(,%rax,4), %edx
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl y(,%rax,4), %edx
	_litmus_P2_1_: movl $1, x(,%rcx,4)

The constraint not exists r1 = 1 /\ r2 = 1 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0)    143
(x,1) (y,1) (%r1,0) (%r2,1)    99897
(x,1) (y,1) (%r1,1) (%r2,0)    99960



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.3-a
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 3-a: Loads may be reordered with older stores to
  different locations *)
{x = 0; y = 0};
exists (%r1 = 0 /\ %r2 = 0);
        P0      |       P1      ;
  mov [x], 1  	|  mov [y], 1 	;
  mov %r1, [y] 	|  mov %r2, [x] ;
               	|               
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rcx,4)
	_litmus_P1_1_: movl y(,%rax,4), %edx
	_litmus_P2_0_: movl $1, y(,%rcx,4)
	_litmus_P2_1_: movl x(,%rax,4), %edx

We found a witness for the case : exists r1 = 0 /\ r2 = 0

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0)    8
(x,1) (y,1) (%r1,0) (%r2,1)    99998
(x,1) (y,1) (%r1,1) (%r2,0)    99993
(x,1) (y,1) (%r1,1) (%r2,1)    1



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.3-a.mfence
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 3-a: Loads may be reordered with older stores to
  different locations *)
{x = 0; y = 0};
exists (%r1 = 0 /\ %r2 = 0);
        P0      |       P1      ;
  mov [x], 1  	|  mov [y], 1 	;
  mfence        |  mfence       ;
  mov %r1, [y] 	|  mov %r2, [x] ;
               	|               
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rcx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl y(,%rax,4), %edx
	_litmus_P2_0_: movl $1, y(,%rcx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl x(,%rax,4), %edx

There is no witness of this case : exists r1 = 0 /\ r2 = 0

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,1)    99501
(x,1) (y,1) (%r1,1) (%r2,0)    99977
(x,1) (y,1) (%r1,1) (%r2,1)    522



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.3-b
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 3-b: Loads are not reordered with older stores to
  the same location *)
{x = 0; y = 0};
forall (%r1 = 1 /\ %r2 = 1);
        P0      |       P1      ;
  mov [x], 1  |  mov [y], 1  	;
  mov %r1, [x] |  mov %r2, [y]  ;
               |               
Generated assembler
	_litmus_P1_0_: movl $1, (%rax)
	_litmus_P1_1_: movl (%rax), %ecx
	_litmus_P2_0_: movl $1, (%rax)
	_litmus_P2_1_: movl (%rax), %ecx

The constraint forall r1 = 1 /\ r2 = 1 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,1) (%r2,1)    200000



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.4
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 4 : Intra Processor forwarding is allowed*)
{x = 0; y = 0};
exists (%r2 = 0 /\ %r4 = 0);
        P0      |       P1      ;
  mov [x], 1  	|  mov [y], 1  	;
  mov %r1, [x] 	|  mov %r3, [y] ;
  mov %r2, [y] 	|  mov %r4, [x] 
Generated assembler
	_litmus_P1_0_: movl $1, (%rdx)
	_litmus_P1_1_: movl (%rdx), %edi
	_litmus_P1_2_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, (%rdx)
	_litmus_P2_1_: movl (%rdx), %edi
	_litmus_P2_2_: movl x(,%rax,4), %ecx

We found a witness for the case : exists r2 = 0 /\ r4 = 0

Histogram of results

(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,0)    33
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    99977
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    99988
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    2



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.5
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 5 :  Stores are transitively visible *)
{x = 0; y = 0};
~ exists (%r1 = 1 /\ %r2 = 1 /\ %r3 = 0);
        P0      |       P1      |     P2;
  mov [x], 1  	|  mov %r1, [x] |  mov %r2, [y]	 ;
               	|  mov [y],   1 |  mov %r3, [x]	 ;
               	|               | 		 
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P2_0_: movl x(,%rax,4), %edx
	_litmus_P2_1_: movl $1, y(,%rcx,4)
	_litmus_P3_0_: movl y(,%rax,4), %ecx
	_litmus_P3_1_: movl x(,%rdx,4), %ebx

The constraint not exists r1 = 1 /\ r2 = 1 /\ r3 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0)    37520
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1)    9
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0)    2282
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1)    64698
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0)    28516
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1)    10690
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1)    56285



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.6
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 6 : Total order on stores to the same location *)
{x = 0};
~ exists (%r1 = 1 /\ %r2 = 2 /\ %r3 = 2 /\ %r4 = 1);
        P0      |       P1        |		P2	|	P3;
  mov [x], 1  	|  mov [x], 2     | 	 mov %r1, [x]	|  mov %r3, [x]	;
               	|      	    	  |   	 mov %r2, [x]	|  mov %r4, [x] ;
               	|                 | 		  	|  	    	
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P2_0_: movl $2, x(,%rax,4)
	_litmus_P3_0_: movl x(,%rax,4), %esi
	_litmus_P3_1_: movl x(,%rax,4), %edx
	_litmus_P4_0_: movl x(,%rax,4), %esi
	_litmus_P4_1_: movl x(,%rax,4), %edx

The constraint not exists r1 = 1 /\ r2 = 2 /\ r3 = 2 /\ r4 = 1 was verified by all states

Histogram of results

(x,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    13722
(x,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    27
(x,1) (%r1,0) (%r2,0) (%r3,0) (%r4,2)    111
(x,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    18433
(x,1) (%r1,0) (%r2,0) (%r3,2) (%r4,1)    2004
(x,1) (%r1,0) (%r2,0) (%r3,2) (%r4,2)    9194
(x,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    35
(x,1) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    94
(x,1) (%r1,0) (%r2,2) (%r3,1) (%r4,1)    1
(x,1) (%r1,0) (%r2,2) (%r3,2) (%r4,2)    1
(x,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    12300
(x,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    1
(x,1) (%r1,1) (%r2,1) (%r3,0) (%r4,2)    1
(x,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    24109
(x,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1)    562
(x,1) (%r1,1) (%r2,1) (%r3,2) (%r4,2)    7331
(x,1) (%r1,2) (%r2,1) (%r3,0) (%r4,0)    2810
(x,1) (%r1,2) (%r2,1) (%r3,1) (%r4,1)    452
(x,1) (%r1,2) (%r2,1) (%r3,2) (%r4,1)    58
(x,1) (%r1,2) (%r2,1) (%r3,2) (%r4,2)    264
(x,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    11168
(x,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    7356
(x,1) (%r1,2) (%r2,2) (%r3,2) (%r4,1)    369
(x,1) (%r1,2) (%r2,2) (%r3,2) (%r4,2)    9497
(x,2) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    7962
(x,2) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    9
(x,2) (%r1,0) (%r2,0) (%r3,0) (%r4,2)    26
(x,2) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    1678
(x,2) (%r1,0) (%r2,0) (%r3,1) (%r4,2)    1060
(x,2) (%r1,0) (%r2,0) (%r3,2) (%r4,2)    9371
(x,2) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    114
(x,2) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    1
(x,2) (%r1,0) (%r2,1) (%r3,1) (%r4,2)    1
(x,2) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    39
(x,2) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    2246
(x,2) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    9651
(x,2) (%r1,1) (%r2,1) (%r3,1) (%r4,2)    708
(x,2) (%r1,1) (%r2,1) (%r3,2) (%r4,2)    6974
(x,2) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    1364
(x,2) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    504
(x,2) (%r1,1) (%r2,2) (%r3,1) (%r4,2)    154
(x,2) (%r1,1) (%r2,2) (%r3,2) (%r4,2)    676
(x,2) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    6239
(x,2) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    6797
(x,2) (%r1,2) (%r2,2) (%r3,1) (%r4,2)    1542
(x,2) (%r1,2) (%r2,2) (%r3,2) (%r4,2)    22984



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.7
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 7: Locked instructions have a total order *)
{x = 0; y = 0; %r1 = 1; %r2 = 1};
~ exists (%r3 = 1 /\ %r4 = 0 /\ %r5 = 1 /\ %r6 = 0);
        P0         |       P1        |		P2	|	P3;
  xchg [x], %r1   |  xchg [y], %r2   | 	 mov %r3, [x]	|  mov %r5, [y]	;
                  |      	     |   mov %r4, [y]	|  mov %r6, [x] ;
                  |                  | 		  	|  	    	
Generated assembler
	_litmus_P1_0_: xchgl (%rdx), %eax
	_litmus_P2_0_: xchgl (%rdx), %eax
	_litmus_P3_0_: movl x(,%rax,4), %ecx
	_litmus_P3_1_: movl y(,%rdx,4), %ebx
	_litmus_P4_0_: movl y(,%rax,4), %ecx
	_litmus_P4_1_: movl x(,%rdx,4), %ebx

The constraint not exists r3 = 1 /\ r4 = 0 /\ r5 = 1 /\ r6 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,0)    40951
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,1)    4864
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,0)    11717
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,1)    15480
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,0)    24407
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,1)    1
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,0)    14656
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,1)    7966
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,0) (%r6,0)    2417
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,0) (%r6,1)    10669
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,1) (%r6,1)    1965
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,0)    8598
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,1)    18474
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0)    9142
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,1)    28693



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.8-a
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(*Test 8-a: Loads are not reordered with locks*)
{x = 0; y = 0; %r1 = 1; %r3 = 1};
~ exists (%r2 = 0 /\ %r4 = 0 );
        P0         |       P1       ;
  xchg [x], %r1   |  xchg [y], %r3  ;
  mov %r2, [y]    |  mov %r4, [x]   ;
                  |                 

Generated assembler
	_litmus_P1_0_: xchgl (%rcx), %ebx
	_litmus_P1_1_: movl y(,%rax,4), %r8d
	_litmus_P2_0_: xchgl (%rcx), %ebx
	_litmus_P2_1_: movl x(,%rax,4), %r8d

The constraint not exists r2 = 0 /\ r4 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    70434
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    70267
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    59299



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.8-b
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test 8-b: Stores are not reordered with locks *)
{x = 0; y = 0; %r1 = 1};
~ exists (%r2 = 1 /\ %r3 = 0 );
        P0         |       P1        ;
  xchg [x], %r1    |  mov  %r2, [y]   ;
  mov [y], 1       |  mov %r3, [x]     ;
                   |                 
Generated assembler
	_litmus_P1_0_: xchgl (%rdx), %eax
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl y(,%rax,4), %ecx
	_litmus_P2_1_: movl x(,%rdx,4), %ebx

The constraint not exists r2 = 1 /\ r3 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0)    100282
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1)    2830
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1)    96888



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.frmap2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test : Does transitivity go through frmap edges? *)
{x = 0; y = 0};
~ exists (%r1 = 1 /\ %r2 = 0 /\ %r3 = 1 /\ %r4 = 0);
       P0        |  P1          |    P2         ;
  mov [y], 1     |   mov [x], 1 |  mov %r3, [x] ;
  mov %r1, [y]   |              |  mov %r4, [y] ;
  mov %r2, [x]   |              |               ;
                 |              |
Generated assembler
	_litmus_P1_0_: movl $1, (%rdx)
	_litmus_P1_1_: movl (%rdx), %edi
	_litmus_P1_2_: movl x(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, x(,%rax,4)
	_litmus_P3_0_: movl x(,%rax,4), %ecx
	_litmus_P3_1_: movl y(,%rdx,4), %ebx

The constraint not exists r1 = 1 /\ r2 = 0 /\ r3 = 1 /\ r4 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    57353
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    42643
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    24209
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    8678
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    89
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    5191
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    61837



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.frmap
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test : Does transitivity go through frmap edges? *)
{x = 0; y = 0};
~ exists (%r1 = 1 /\ %r2 = 1 /\ %r3 = 2 /\ %r4 = 0);
        P0      |       P1        |		P2	|	P3;
  mov [x], 1  	|  mov [y], 1     | 	 mov [x], 2	|  mov %r3, [x]	;
               	|  mov %r1, [y]   |   	        	|  mov %r4, [y] ;
               	|  mov %r2, [x]   | 		  	|  	    	;
                |                 |                     |
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P2_0_: movl $1, (%rdx)
	_litmus_P2_1_: movl (%rdx), %edi
	_litmus_P2_2_: movl x(,%rax,4), %ecx
	_litmus_P3_0_: movl $2, x(,%rax,4)
	_litmus_P4_0_: movl x(,%rax,4), %ecx
	_litmus_P4_1_: movl y(,%rdx,4), %ebx

The constraint not exists r1 = 1 /\ r2 = 1 /\ r3 = 2 /\ r4 = 0 is not satisfied by the states : 
    -  (x,1); (y,1); (r1,1); (r2,1); (r3,2); (r4,0);


Histogram of results

(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    9621
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    6773
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    6471
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,2) (%r4,1)    4965
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    11625
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    53
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    2695
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    6984
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,0)    11364
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1)    157
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    10489
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,1)    20
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    9676
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,0)    8451
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,1)    10691
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    8872
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    14007
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    7908
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,2) (%r4,1)    6439
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    5062
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    2
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    9069
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    10847
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1)    4667
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    7572
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,1)    16
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,0)    15436
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    191
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,0)    4349
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,1)    5528



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.lfence
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
{x = 0; y = 0; z = 0; w = 0;  %r1 = 0; %r2 = 0; %r3 = 0; %r4 = 0};
exists (%r1 = 1 /\ %r2 = 0 /\ %r3 = 1 /\ %r4 = 0);
        P0        |       P1        |		P2	|	P3;
  mov [x], $1     |  mov  [z], $1   | 	 mov %r1, [y]	|  mov %r3, [w]	 ;
                  |            	    |   lfence	  	|  lfence    	 ;
  mov [y], $1     |  mov [w], $1    | 	mov %r2, [z]	| mov %r4, [x]
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: movl $1, w(,%rcx,4)
	_litmus_P3_0_: movl y(,%rax,4), %ecx
	_litmus_P3_1_: lfence
	_litmus_P3_2_: movl z(,%rdx,4), %ebx
	_litmus_P4_0_: movl w(,%rax,4), %ecx
	_litmus_P4_1_: lfence
	_litmus_P4_2_: movl x(,%rdx,4), %ebx

There is no witness of this case : exists r1 = 1 /\ r2 = 0 /\ r3 = 1 /\ r4 = 0

Histogram of results

(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    59763
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    5437
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    6246
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    14117
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    6344
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    18829
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    13064
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    1691
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    25207
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    4123
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    6401
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    11739
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    4998
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    22041



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.mfence2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
{x = 0; y = 0; z = 0; w = 0;  %r1 = 0; %r2 = 0; %r3 = 0; %r4 = 0};
exists (%r1 = 1 /\ %r2 = 0 /\ %r3 = 1 /\ %r4 = 0);
        P0        |       P1        |		P2	|	P3;
  mov [x], $1     |  mov  [z], $1   | 	 mov %r1, [y]	|  mov %r3, [w]	 ;
                  |            	    |   mfence	  	|  mfence    	 ;
  mov [y], $1     |  mov [w], $1    | 	mov %r2, [z]	| mov %r4, [x]
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: movl $1, w(,%rcx,4)
	_litmus_P3_0_: movl y(,%rax,4), %ecx
	_litmus_P3_1_: mfence
	_litmus_P3_2_: movl z(,%rdx,4), %ebx
	_litmus_P4_0_: movl w(,%rax,4), %ecx
	_litmus_P4_1_: mfence
	_litmus_P4_2_: movl x(,%rdx,4), %ebx

There is no witness of this case : exists r1 = 1 /\ r2 = 0 /\ r3 = 1 /\ r4 = 0

Histogram of results

(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    59368
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    5498
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    6521
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    14025
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    6767
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    17959
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    13446
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    1777
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    24476
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    3286
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    6056
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    11940
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    4436
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    24445



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.mfence
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
{x = 0; y = 0; z = 0; w = 0;  %r1 = 0; %r2 = 0; %r3 = 0; %r4 = 0};
exists (%r1 = 1 /\ %r2 = 0 /\ %r3 = 1 /\ %r4 = 0);
        P0        |       P1        |		P2	|	P3;
  mov [x], $1     |  mov  [z], $1   | 	 mov %r1, [y]	|  mov %r3, [w]	;
  mfence          |  mfence	    |   mov %r2, [z]	|  mov %r4, [x] ;
  mov [y], $1     |  mov [w], $1    | 		  	|  	    	
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl $1, w(,%rcx,4)
	_litmus_P3_0_: movl y(,%rax,4), %ecx
	_litmus_P3_1_: movl z(,%rdx,4), %ebx
	_litmus_P4_0_: movl w(,%rax,4), %ecx
	_litmus_P4_1_: movl x(,%rdx,4), %ebx

There is no witness of this case : exists r1 = 1 /\ r2 = 0 /\ r3 = 1 /\ r4 = 0

Histogram of results

(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    40206
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    10069
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    2900
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    25656
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    15769
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    109
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    4748
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    17679
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    1117
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    13883
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    3990
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    8671
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    12883
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    1631
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    40689



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.nofence
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
{x = 0; y = 0; z = 0; w = 0;  %r1 = 0; %r2 = 0; %r3 = 0; %r4 = 0};
exists (%r1 = 1 /\ %r2 = 0 /\ %r3 = 1 /\ %r4 = 0);
        P0        |       P1        |		P2	|	P3;
  mov [x], $1     |  mov  [z], $1   | 	mov %r1, [y]	| mov %r3, [w]	 ;
  mov [y], $1     |  mov [w], $1    | 	mov %r2, [z]	| mov %r4, [x]
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: movl $1, w(,%rcx,4)
	_litmus_P3_0_: movl y(,%rax,4), %ecx
	_litmus_P3_1_: movl z(,%rdx,4), %ebx
	_litmus_P4_0_: movl w(,%rax,4), %ecx
	_litmus_P4_1_: movl x(,%rdx,4), %ebx

There is no witness of this case : exists r1 = 1 /\ r2 = 0 /\ r3 = 1 /\ r4 = 0

Histogram of results

(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    60534
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    5694
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    6702
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    13125
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    5234
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    17576
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    12066
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    2441
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    26084
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    3784
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    6293
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    11192
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    6864
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    22411



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.readspec
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
(* Test : Read speculation is allowed by the model *)
{x = 0; y = 0};
exists (%r1 = 0 /\ %r2 = 1 /\ %r3 = 2);
       P0        |		P1	|	P2;
  mov [x], 2     | 	 mov [y], 1	|  mov %r2, [x]	;
  mov %r1, [y]   |   	 mov [x], 1 	|  mov %r3, [x] ;
                 |                      |
Generated assembler
	_litmus_P1_0_: movl $2, x(,%rcx,4)
	_litmus_P1_1_: movl y(,%rax,4), %edx
	_litmus_P2_0_: movl $1, y(,%rax,4)
	_litmus_P2_1_: movl $1, x(,%rcx,4)
	_litmus_P3_0_: movl x(,%rax,4), %esi
	_litmus_P3_1_: movl x(,%rax,4), %edx

There is no witness of this case : exists r1 = 0 /\ r2 = 1 /\ r3 = 2

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0)    54239
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1)    28804
(x,1) (y,1) (%r1,0) (%r2,2) (%r3,1)    563
(x,1) (y,1) (%r1,0) (%r2,2) (%r3,2)    37634
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0)    5
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1)    1
(x,2) (y,1) (%r1,0) (%r2,0) (%r3,0)    4428
(x,2) (y,1) (%r1,0) (%r2,2) (%r3,2)    1
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,0)    7328
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,1)    8476
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,2)    3017
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,2)    55504



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.intel.sfence
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
{x = 0; y = 0; z = 0; w = 0;  %r1 = 0; %r2 = 0; %r3 = 0; %r4 = 0};
exists (%r1 = 1 /\ %r2 = 0 /\ %r3 = 1 /\ %r4 = 0);
        P0        |       P1        |		P2	|	P3;
  mov [x], $1     |  mov  [z], $1   | 	 mov %r1, [y]	|  mov %r3, [w]	;
  sfence          |  sfence	    |   mov %r2, [z]	|  mov %r4, [x] ;
  mov [y], $1     |  mov [w], $1    | 		  	|  	    	
Generated assembler
	_litmus_P1_0_: movl $1, x(,%rax,4)
	_litmus_P1_1_: sfence
	_litmus_P1_2_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: sfence
	_litmus_P2_2_: movl $1, w(,%rcx,4)
	_litmus_P3_0_: movl y(,%rax,4), %ecx
	_litmus_P3_1_: movl z(,%rdx,4), %ebx
	_litmus_P4_0_: movl w(,%rax,4), %ecx
	_litmus_P4_1_: movl x(,%rdx,4), %ebx

There is no witness of this case : exists r1 = 1 /\ r2 = 0 /\ r3 = 1 /\ r4 = 0

Histogram of results

(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    28521
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    7743
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    4034
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    30187
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    11031
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    5558
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    13848
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    2446
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    13265
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    4281
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    16101
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    12105
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    2492
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    48388



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.n2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
{x = 0; y = 0; z = 0; %r1 = 0; %r2 = 0; %r3 = 0; %r4 = 0};
~exists (%r1 = 1 /\ %r2 = 2 /\ %r3 = 1 /\ %r4 = 0);
        P0        |       P1        |		P2	|	P3;
  mov [y],  1     |  mov [x],  2    | 	mov %r1, [x]	| mov %r3, [z]	 ;
  mov [x],  1     |  mov [z],  1    | 	mov %r2, [x]	| mov %r4, [y]
Generated assembler
	_litmus_P1_0_: movl $1, y(,%rax,4)
	_litmus_P1_1_: movl $1, x(,%rcx,4)
	_litmus_P2_0_: movl $2, x(,%rax,4)
	_litmus_P2_1_: movl $1, z(,%rcx,4)
	_litmus_P3_0_: movl x(,%rax,4), %esi
	_litmus_P3_1_: movl x(,%rax,4), %edx
	_litmus_P4_0_: movl z(,%rax,4), %ecx
	_litmus_P4_1_: movl y(,%rdx,4), %ebx

The constraint not exists r1 = 1 /\ r2 = 2 /\ r3 = 1 /\ r4 = 0 was verified by all states

Histogram of results

(x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    21925
(x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    6972
(x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    10837
(x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    16
(x,1) (y,1) (z,1) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    308
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    6369
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    2
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    9857
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    18809
(x,1) (y,1) (z,1) (%r1,2) (%r2,1) (%r3,0) (%r4,0)    1288
(x,1) (y,1) (z,1) (%r1,2) (%r2,1) (%r3,1) (%r4,0)    797
(x,1) (y,1) (z,1) (%r1,2) (%r2,1) (%r3,1) (%r4,1)    584
(x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    7043
(x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,0)    13537
(x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    6375
(x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    18255
(x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    9625
(x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    4093
(x,2) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    391
(x,2) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    1
(x,2) (y,1) (z,1) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    9
(x,2) (y,1) (z,1) (%r1,0) (%r2,2) (%r3,1) (%r4,1)    1
(x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    6330
(x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    21338
(x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    2349
(x,2) (y,1) (z,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    1063
(x,2) (y,1) (z,1) (%r1,1) (%r2,2) (%r3,0) (%r4,1)    2705
(x,2) (y,1) (z,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    786
(x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    5525
(x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,1)    12551
(x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    10259



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
x86/test.thomas.lock.1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Test
{x = 0; y = 0; %r1 = 1};
exists (%r2 = 1 /\ %r3 = 0 /\ %r4 = 1 /\ %r5 = 1 /\ %r6 = 0 /\ %r7 = 1);
 P0           |        P1   |     P2        |   P3           ;
 xchg %r1,[x] |   mov [y],1 | mov %r2,[y]  |   mov %r5, [x]  ;
              |             | mov %r3,[x]  |   mov %r6, [y]  ;
              |             | mov %r4,[x]  |   mov %r7, [y]  ;
              |             |              |

Generated assembler
	_litmus_P1_0_: xchgl %eax, (%rdx)
	_litmus_P2_0_: movl $1, y(,%rax,4)
	_litmus_P3_0_: movl y(,%rax,4), %r9d
	_litmus_P3_1_: movl x(,%rdx,4), %ecx
	_litmus_P3_2_: movl x(,%rdx,4), %ebx
	_litmus_P4_0_: movl x(,%rax,4), %r9d
	_litmus_P4_1_: movl y(,%rdx,4), %ecx
	_litmus_P4_2_: movl y(,%rdx,4), %ebx

There is no witness of this case : exists r2 = 1 /\ r3 = 0 /\ r4 = 1 /\ r5 = 1 /\ r6 = 0 /\ r7 = 1

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,0) (%r7,0)    54438
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,0) (%r7,1)    165
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,1) (%r7,1)    12592
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,0) (%r7,0)    3743
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,0) (%r7,1)    4
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,1) (%r7,1)    13102
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,0) (%r7,0)    14
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,1) (%r7,1)    1
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,0) (%r7,0)    7
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,1) (%r7,1)    7
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,0) (%r7,0)    6581
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,0)    19663
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,1)    1
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,1) (%r7,1)    13664
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,0) (%r6,0) (%r7,0)    4505
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,0) (%r6,1) (%r7,1)    20869
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,1) (%r6,1) (%r7,1)    7116
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) (%r5,0) (%r6,0) (%r7,0)    1
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) (%r5,0) (%r6,1) (%r7,1)    6
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,0) (%r6,0) (%r7,0)    6574
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,0) (%r6,1) (%r7,1)    10090
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,0)    3073
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,1) (%r6,1) (%r7,1)    23784

Computer
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 15
model name	: Intel(R) Core(TM)2 Quad CPU           @ 2.40GHz
stepping	: 7
cpu MHz		: 1596.000
cache size	: 4096 KB
physical id	: 0
siblings	: 4
core id		: 0
cpu cores	: 4
fpu		: yes
fpu_exception	: yes
cpuid level	: 10
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good pni monitor ds_cpl vmx est tm2 ssse3 cx16 xtpr lahf_lm
bogomips	: 4802.10
clflush size	: 64
cache_alignment	: 64
address sizes	: 36 bits physical, 48 bits virtual
power management:

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 15
model name	: Intel(R) Core(TM)2 Quad CPU           @ 2.40GHz
stepping	: 7
cpu MHz		: 2394.000
cache size	: 4096 KB
physical id	: 0
siblings	: 4
core id		: 2
cpu cores	: 4
fpu		: yes
fpu_exception	: yes
cpuid level	: 10
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good pni monitor ds_cpl vmx est tm2 ssse3 cx16 xtpr lahf_lm
bogomips	: 4799.50
clflush size	: 64
cache_alignment	: 64
address sizes	: 36 bits physical, 48 bits virtual
power management:

processor	: 2
vendor_id	: GenuineIntel
cpu family	: 6
model		: 15
model name	: Intel(R) Core(TM)2 Quad CPU           @ 2.40GHz
stepping	: 7
cpu MHz		: 1596.000
cache size	: 4096 KB
physical id	: 0
siblings	: 4
core id		: 1
cpu cores	: 4
fpu		: yes
fpu_exception	: yes
cpuid level	: 10
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good pni monitor ds_cpl vmx est tm2 ssse3 cx16 xtpr lahf_lm
bogomips	: 4799.55
clflush size	: 64
cache_alignment	: 64
address sizes	: 36 bits physical, 48 bits virtual
power management:

processor	: 3
vendor_id	: GenuineIntel
cpu family	: 6
model		: 15
model name	: Intel(R) Core(TM)2 Quad CPU           @ 2.40GHz
stepping	: 7
cpu MHz		: 1596.000
cache size	: 4096 KB
physical id	: 0
siblings	: 4
core id		: 3
cpu cores	: 4
fpu		: yes
fpu_exception	: yes
cpuid level	: 10
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good pni monitor ds_cpl vmx est tm2 ssse3 cx16 xtpr lahf_lm
bogomips	: 4799.48
clflush size	: 64
cache_alignment	: 64
address sizes	: 36 bits physical, 48 bits virtual
power management:

Parameters


#define PROC_1 0
#define PROC_2 1
#define PROC_3 2
#define PROC_4 3

#define V_NO
#define NUMBER_OF_RUN 1000
#define SIZE_OF_TEST 200
#define BUFFER_SIZE 128000