%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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, x(,%rdx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl x(,%rdx,4), %esi
	_litmus_P1_3_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rdx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl y(,%rdx,4), %esi
	_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)    999006
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    998980
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    2014



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rdx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl x(,%rax,4), %ecx

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

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,1)    999010
(x,1) (y,1) (%r1,1) (%r2,0)    998874
(x,1) (y,1) (%r1,1) (%r2,1)    2116



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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, x(,%rdx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl x(,%rdx,4), %esi
	_litmus_P1_3_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rdx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl y(,%rdx,4), %esi
	_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)    997200
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    997958
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    4842



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rdx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl x(,%rax,4), %ecx

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

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,1)    997669
(x,1) (y,1) (%r1,1) (%r2,0)    997266
(x,1) (y,1) (%r1,1) (%r2,1)    5065



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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), %esi
	_litmus_P3_1_: movl y(,%rdx,4), %ecx
	_litmus_P4_0_: movl y(,%rax,4), %esi
	_litmus_P4_1_: movl x(,%rdx,4), %ecx

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)    324066
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    79027
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    81780
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    176064
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    92575
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    10
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    145156
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    96705
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    84356
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    179470
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    73666
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    162468
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    85076
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    83485
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    336096



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl y(,%rax,4), %esi
	_litmus_P2_1_: movl x(,%rdx,4), %ecx

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

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0)    1001123
(x,1) (y,1) (%r1,0) (%r2,1)    1399
(x,1) (y,1) (%r1,1) (%r2,1)    997478



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl y(,%rax,4), %esi
	_litmus_P2_1_: movl x(,%rdx,4), %ecx

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

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0)    1000907
(x,1) (y,1) (%r1,0) (%r2,1)    1226
(x,1) (y,1) (%r1,1) (%r2,1)    997867



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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), %ecx
	_litmus_P1_1_: movl $1, y(,%rdx,4)
	_litmus_P2_0_: movl y(,%rax,4), %ecx
	_litmus_P2_1_: movl $1, x(,%rdx,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)    3396
(x,1) (y,1) (%r1,0) (%r2,1)    998663
(x,1) (y,1) (%r1,1) (%r2,0)    997941



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P1_1_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rdx,4)
	_litmus_P2_1_: movl x(,%rax,4), %ecx

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

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,0)    4981
(x,1) (y,1) (%r1,0) (%r2,1)    998022
(x,1) (y,1) (%r1,1) (%r2,0)    996972
(x,1) (y,1) (%r1,1) (%r2,1)    25



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P1_1_: mfence
	_litmus_P1_2_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rdx,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl x(,%rax,4), %ecx

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

Histogram of results

(x,1) (y,1) (%r1,0) (%r2,1)    999125
(x,1) (y,1) (%r1,1) (%r2,0)    998857
(x,1) (y,1) (%r1,1) (%r2,1)    2018



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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, x(,%rax,4)
	_litmus_P1_1_: movl x(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rax,4)
	_litmus_P2_1_: movl y(,%rax,4), %ecx

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

Histogram of results

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



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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, x(,%rdx,4)
	_litmus_P1_1_: movl x(,%rdx,4), %esi
	_litmus_P1_2_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rdx,4)
	_litmus_P2_1_: movl y(,%rdx,4), %esi
	_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)    2920
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    998910
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    997986
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    184



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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), %ecx
        _litmus_P2_1_: movl $1, y(,%rdx,4)
        _litmus_P3_0_: movl y(,%rax,4), %esi
        _litmus_P3_1_: movl x(,%rdx,4), %ecx

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)    336648
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1)    476
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0)    320276
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1)    349551
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0)    323582
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1)    355627
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1)    313840


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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), %ecx
	_litmus_P4_0_: movl x(,%rax,4), %esi
	_litmus_P4_1_: movl x(,%rax,4), %ecx

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)    177410
(x,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    1
(x,1) (%r1,0) (%r2,0) (%r3,0) (%r4,2)    14
(x,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    84038
(x,1) (%r1,0) (%r2,0) (%r3,2) (%r4,2)    82364
(x,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    4
(x,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    2
(x,1) (%r1,0) (%r2,1) (%r3,2) (%r4,2)    2
(x,1) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    8
(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)    73671
(x,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    2
(x,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    166000
(x,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1)    9
(x,1) (%r1,1) (%r2,1) (%r3,2) (%r4,2)    90809
(x,1) (%r1,2) (%r2,1) (%r3,0) (%r4,0)    8
(x,1) (%r1,2) (%r2,1) (%r3,1) (%r4,1)    10
(x,1) (%r1,2) (%r2,1) (%r3,2) (%r4,2)    2
(x,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    89436
(x,1) (%r1,2) (%r2,2) (%r3,0) (%r4,1)    2
(x,1) (%r1,2) (%r2,2) (%r3,0) (%r4,2)    7
(x,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    89917
(x,1) (%r1,2) (%r2,2) (%r3,2) (%r4,1)    4
(x,1) (%r1,2) (%r2,2) (%r3,2) (%r4,2)    153083
(x,2) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    161917
(x,2) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    9
(x,2) (%r1,0) (%r2,0) (%r3,0) (%r4,2)    4
(x,2) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    72723
(x,2) (%r1,0) (%r2,0) (%r3,1) (%r4,2)    4
(x,2) (%r1,0) (%r2,0) (%r3,2) (%r4,2)    90407
(x,2) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    6
(x,2) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    1
(x,2) (%r1,0) (%r2,2) (%r3,1) (%r4,1)    4
(x,2) (%r1,0) (%r2,2) (%r3,2) (%r4,2)    2
(x,2) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    89590
(x,2) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    4
(x,2) (%r1,1) (%r2,1) (%r3,0) (%r4,2)    2
(x,2) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    178561
(x,2) (%r1,1) (%r2,1) (%r3,1) (%r4,2)    14
(x,2) (%r1,1) (%r2,1) (%r3,2) (%r4,2)    71102
(x,2) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    6
(x,2) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    5
(x,2) (%r1,1) (%r2,2) (%r3,2) (%r4,2)    5
(x,2) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    78764
(x,2) (%r1,2) (%r2,2) (%r3,0) (%r4,1)    2
(x,2) (%r1,2) (%r2,2) (%r3,0) (%r4,2)    1
(x,2) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    86769
(x,2) (%r1,2) (%r2,2) (%r3,1) (%r4,2)    18
(x,2) (%r1,2) (%r2,2) (%r3,2) (%r4,2)    163275



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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 x(,%rdx,4), %eax
	_litmus_P2_0_: xchgl y(,%rdx,4), %eax
	_litmus_P3_0_: movl x(,%rax,4), %esi
	_litmus_P3_1_: movl y(,%rdx,4), %ecx
	_litmus_P4_0_: movl y(,%rax,4), %esi
	_litmus_P4_1_: movl x(,%rdx,4), %ecx

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)    332677
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,1)    74352
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,0)    85672
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,1)    176871
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,0)    87451
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,1)    8
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,0)    139253
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,1)    95443
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,0) (%r6,0)    80097
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,0) (%r6,1)    177379
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,1) (%r6,1)    73048
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,0)    163697
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,1)    93677
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0)    91444
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,1)    328931



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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 x(,%rcx,4), %edx
	_litmus_P1_1_: movl y(,%rax,4), %edi
	_litmus_P2_0_: xchgl y(,%rcx,4), %edx
	_litmus_P2_1_: movl x(,%rax,4), %edi

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)    998991
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    998518
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    2491



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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 x(,%rdx,4), %eax
	_litmus_P1_1_: movl $1, y(,%rcx,4)
	_litmus_P2_0_: movl y(,%rax,4), %esi
	_litmus_P2_1_: movl x(,%rdx,4), %ecx

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)    1002511
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1)    6555
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1)    990934



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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, y(,%rdx,4)
	_litmus_P1_1_: movl y(,%rdx,4), %esi
	_litmus_P1_2_: movl x(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, x(,%rax,4)
	_litmus_P3_0_: movl x(,%rax,4), %esi
	_litmus_P3_1_: movl y(,%rdx,4), %ecx

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)    325393
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    344197
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    324933
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    335790
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    136
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    326671
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    342880



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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, y(,%rdx,4)
	_litmus_P2_1_: movl y(,%rdx,4), %esi
	_litmus_P2_2_: movl x(,%rax,4), %ecx
	_litmus_P3_0_: movl $2, x(,%rax,4)
	_litmus_P4_0_: movl x(,%rax,4), %esi
	_litmus_P4_1_: movl y(,%rdx,4), %ecx

The constraint not exists r1 = 1 /\ r2 = 1 /\ r3 = 2 /\ r4 = 0 is not satisfied by the states : 
    -  (x,2); (y,1); (r1,1); (r2,1); (r3,2); (r4,0);
    -  (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)    93901
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    70432
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    92690
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,2) (%r4,0)    1
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,2) (%r4,1)    81725
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    81026
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    3
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    65507
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    99922
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,0)    75876
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1)    104
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    84415
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,1)    93
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,0)    26
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    85277
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,0)    83521
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,1)    89777
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    72676
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    89963
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,0)    2
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    83854
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,2) (%r4,1)    81304
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    78122
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    25
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    88485
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    86905
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,0)    16
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1)    74785
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    89881
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,1)    8
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,0)    88860
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    68
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,0)    69579
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,1)    91171



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: movl $1, w(,%rdx,4)
	_litmus_P3_0_: movl y(,%rax,4), %esi
	_litmus_P3_1_: lfence
	_litmus_P3_2_: movl z(,%rdx,4), %ecx
	_litmus_P4_0_: movl w(,%rax,4), %esi
	_litmus_P4_1_: lfence
	_litmus_P4_2_: movl x(,%rdx,4), %ecx

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)    296725
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    72047
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    76214
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    186012
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    138470
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    26
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    152831
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    74381
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    58413
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    172479
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    45103
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    172400
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    106213
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    83486
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    365200



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: movl $1, w(,%rdx,4)
	_litmus_P3_0_: movl y(,%rax,4), %esi
	_litmus_P3_1_: mfence
	_litmus_P3_2_: movl z(,%rdx,4), %ecx
	_litmus_P4_0_: movl w(,%rax,4), %esi
	_litmus_P4_1_: mfence
	_litmus_P4_2_: movl x(,%rdx,4), %ecx

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)    292569
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    76933
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    71906
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    188649
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    138361
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    38
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    149224
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    72986
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    54283
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    169795
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    41541
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    177618
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    109276
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    67923
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    388898



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: mfence
	_litmus_P2_2_: movl $1, w(,%rdx,4)
	_litmus_P3_0_: movl y(,%rax,4), %esi
	_litmus_P3_1_: movl z(,%rdx,4), %ecx
	_litmus_P4_0_: movl w(,%rax,4), %esi
	_litmus_P4_1_: movl x(,%rdx,4), %ecx

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)    474017
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    89213
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    28340
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    146384
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    93589
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    153
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    175018
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    146498
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    34011
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    185306
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    47478
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    136476
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    132520
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    68236
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    242761



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: movl $1, w(,%rdx,4)
	_litmus_P3_0_: movl y(,%rax,4), %esi
	_litmus_P3_1_: movl z(,%rdx,4), %ecx
	_litmus_P4_0_: movl w(,%rax,4), %esi
	_litmus_P4_1_: movl x(,%rdx,4), %ecx

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)    350582
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    74224
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    82664
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    170568
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    91651
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    10
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    153130
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    79535
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    71486
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    179233
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    62249
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    159740
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    98761
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    92899
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    333268



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P1_1_: movl y(,%rax,4), %ecx
	_litmus_P2_0_: movl $1, y(,%rax,4)
	_litmus_P2_1_: movl $1, x(,%rdx,4)
	_litmus_P3_0_: movl x(,%rax,4), %esi
	_litmus_P3_1_: movl x(,%rax,4), %ecx

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)    323667
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1)    4
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,2)    7
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1)    328688
(x,1) (y,1) (%r1,0) (%r2,2) (%r3,1)    14
(x,1) (y,1) (%r1,0) (%r2,2) (%r3,2)    339871
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,0)    1627
(x,1) (y,1) (%r1,1) (%r2,0) (%r3,1)    1
(x,1) (y,1) (%r1,1) (%r2,1) (%r3,1)    356
(x,1) (y,1) (%r1,1) (%r2,2) (%r3,2)    16
(x,2) (y,1) (%r1,0) (%r2,0) (%r3,0)    160
(x,2) (y,1) (%r1,0) (%r2,1) (%r3,1)    3
(x,2) (y,1) (%r1,0) (%r2,2) (%r3,2)    149
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,0)    338466
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,1)    8
(x,2) (y,1) (%r1,1) (%r2,0) (%r3,2)    4
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,1)    329379
(x,2) (y,1) (%r1,1) (%r2,1) (%r3,2)    17
(x,2) (y,1) (%r1,1) (%r2,2) (%r3,2)    337563



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl $1, z(,%rax,4)
	_litmus_P2_1_: sfence
	_litmus_P2_2_: movl $1, w(,%rdx,4)
	_litmus_P3_0_: movl y(,%rax,4), %esi
	_litmus_P3_1_: movl z(,%rdx,4), %ecx
	_litmus_P4_0_: movl w(,%rax,4), %esi
	_litmus_P4_1_: movl x(,%rdx,4), %ecx

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)    350341
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    70188
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    82734
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    171795
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    94656
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1)    25
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0)    148563
(w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1)    80194
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0)    66211
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1)    173673
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1)    64185
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    165000
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    99732
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    94624
(w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    338079



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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(,%rdx,4)
	_litmus_P2_0_: movl $2, x(,%rax,4)
	_litmus_P2_1_: movl $1, z(,%rdx,4)
	_litmus_P3_0_: movl x(,%rax,4), %esi
	_litmus_P3_1_: movl x(,%rax,4), %ecx
	_litmus_P4_0_: movl z(,%rax,4), %esi
	_litmus_P4_1_: movl y(,%rdx,4), %ecx

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)    167692
(x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    78
(x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0)    84973
(x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    91810
(x,1) (y,1) (z,1) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    3
(x,1) (y,1) (z,1) (%r1,0) (%r2,2) (%r3,1) (%r4,0)    2
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    70925
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    123
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0)    88600
(x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    164063
(x,1) (y,1) (z,1) (%r1,2) (%r2,1) (%r3,0) (%r4,0)    9
(x,1) (y,1) (z,1) (%r1,2) (%r2,1) (%r3,1) (%r4,0)    7
(x,1) (y,1) (z,1) (%r1,2) (%r2,1) (%r3,1) (%r4,1)    4
(x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    91660
(x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,1)    21
(x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,0)    151268
(x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    95387
(x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0)    169613
(x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1)    77791
(x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1)    81202
(x,2) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0)    5
(x,2) (y,1) (z,1) (%r1,0) (%r2,2) (%r3,0) (%r4,0)    1
(x,2) (y,1) (z,1) (%r1,0) (%r2,2) (%r3,0) (%r4,1)    1
(x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0)    87325
(x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1)    185469
(x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1)    66272
(x,2) (y,1) (z,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0)    6
(x,2) (y,1) (z,1) (%r1,1) (%r2,2) (%r3,0) (%r4,1)    5
(x,2) (y,1) (z,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1)    7
(x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0)    78599
(x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,1)    100386
(x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1)    146693



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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 %edx, x(,%rax,4)
	_litmus_P2_0_: movl $1, y(,%rax,4)
	_litmus_P3_0_: movl y(,%rax,4), %edi
	_litmus_P3_1_: movl x(,%rdx,4), %esi
	_litmus_P3_2_: movl x(,%rdx,4), %ecx
	_litmus_P4_0_: movl x(,%rax,4), %edi
	_litmus_P4_1_: movl y(,%rdx,4), %esi
	_litmus_P4_2_: movl y(,%rdx,4), %ecx

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)    322230
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,0) (%r7,1)    4
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,1) (%r7,1)    87759
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,0) (%r7,0)    70607
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,1) (%r7,1)    177189
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,0) (%r7,0)    4
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,1) (%r7,1)    1
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,0) (%r7,0)    93505
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,0) (%r7,1)    1
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,1) (%r7,1)    15
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,0)    162156
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,1)    11
(x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,1) (%r7,1)    76329
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,0) (%r6,0) (%r7,0)    95763
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,0) (%r6,0) (%r7,1)    3
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,0) (%r6,1) (%r7,1)    125708
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,1) (%r6,1) (%r7,1)    63662
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) (%r5,1) (%r6,1) (%r7,1)    1
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,0) (%r6,0) (%r7,0)    154532
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,0) (%r6,0) (%r7,1)    2
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,0) (%r6,1) (%r7,1)    106825
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,0)    91122
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,1)    8
(x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,1) (%r6,1) (%r7,1)    372563

Computer
processor	: 0
vendor_id	: AuthenticAMD
cpu family	: 15
model		: 65
model name	: Dual-Core AMD Opteron(tm) Processor 2220
stepping	: 3
cpu MHz		: 2800.369
cache size	: 1024 KB
physical id	: 0
siblings	: 2
core id		: 0
cpu cores	: 2
fpu		: yes
fpu_exception	: yes
cpuid level	: 1
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 ht syscall nx mmxext lm 3dnowext 3dnow pni cx16
bogomips	: 5604.84
TLB size	: 1088 4K pages
clflush size	: 64
cache_alignment	: 64
address sizes	: 40 bits physical, 48 bits virtual
power management: ts fid vid ttp [4] [5]

processor	: 1
vendor_id	: AuthenticAMD
cpu family	: 15
model		: 65
model name	: Dual-Core AMD Opteron(tm) Processor 2220
stepping	: 3
cpu MHz		: 2800.369
cache size	: 1024 KB
physical id	: 1
siblings	: 2
core id		: 0
cpu cores	: 2
fpu		: yes
fpu_exception	: yes
cpuid level	: 1
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 ht syscall nx mmxext lm 3dnowext 3dnow pni cx16
bogomips	: 5600.14
TLB size	: 1088 4K pages
clflush size	: 64
cache_alignment	: 64
address sizes	: 40 bits physical, 48 bits virtual
power management: ts fid vid ttp [4] [5]

processor	: 2
vendor_id	: AuthenticAMD
cpu family	: 15
model		: 65
model name	: Dual-Core AMD Opteron(tm) Processor 2220
stepping	: 3
cpu MHz		: 2800.369
cache size	: 1024 KB
physical id	: 0
siblings	: 2
core id		: 1
cpu cores	: 2
fpu		: yes
fpu_exception	: yes
cpuid level	: 1
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 ht syscall nx mmxext lm 3dnowext 3dnow pni cx16
bogomips	: 5600.12
TLB size	: 1088 4K pages
clflush size	: 64
cache_alignment	: 64
address sizes	: 40 bits physical, 48 bits virtual
power management: ts fid vid ttp [4] [5]

processor	: 3
vendor_id	: AuthenticAMD
cpu family	: 15
model		: 65
model name	: Dual-Core AMD Opteron(tm) Processor 2220
stepping	: 3
cpu MHz		: 2800.369
cache size	: 1024 KB
physical id	: 1
siblings	: 2
core id		: 1
cpu cores	: 2
fpu		: yes
fpu_exception	: yes
cpuid level	: 1
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 ht syscall nx mmxext lm 3dnowext 3dnow pni cx16
bogomips	: 5600.21
TLB size	: 1088 4K pages
clflush size	: 64
cache_alignment	: 64
address sizes	: 40 bits physical, 48 bits virtual
power management: ts fid vid ttp [4] [5]

Parameters


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

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