%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 99017 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 99252 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 1731 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 98097 (x,1) (y,1) (%r1,1) (%r2,0) 99623 (x,1) (y,1) (%r1,1) (%r2,1) 2280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 99435 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 99322 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 1243 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 99148 (x,1) (y,1) (%r1,1) (%r2,0) 99774 (x,1) (y,1) (%r1,1) (%r2,1) 1078 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 19648 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 13037 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) 6815 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 11271 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) 393 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0) 12000 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) 5670 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0) 30384 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 31415 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 279 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 18290 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 17557 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 14391 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 18850 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 100191 (x,1) (y,1) (%r1,0) (%r2,1) 644 (x,1) (y,1) (%r1,1) (%r2,1) 99165 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 100093 (x,1) (y,1) (%r1,0) (%r2,1) 668 (x,1) (y,1) (%r1,1) (%r2,1) 99239 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 87 (x,1) (y,1) (%r1,0) (%r2,1) 99941 (x,1) (y,1) (%r1,1) (%r2,0) 99972 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 13 (x,1) (y,1) (%r1,0) (%r2,1) 99992 (x,1) (y,1) (%r1,1) (%r2,0) 99993 (x,1) (y,1) (%r1,1) (%r2,1) 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 98076 (x,1) (y,1) (%r1,1) (%r2,0) 99029 (x,1) (y,1) (%r1,1) (%r2,1) 2895 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 1 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 100033 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 99923 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 40907 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) 1 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) 27559 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) 39438 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) 25088 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) 26547 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) 40460 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 11322 (x,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 6936 (x,1) (%r1,0) (%r2,0) (%r3,2) (%r4,2) 9707 (x,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 23925 (x,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 24932 (x,1) (%r1,1) (%r2,1) (%r3,2) (%r4,2) 23501 (x,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0) 1382 (x,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1) 538 (x,1) (%r1,2) (%r2,2) (%r3,2) (%r4,2) 1220 (x,2) (%r1,0) (%r2,0) (%r3,0) (%r4,0) 10941 (x,2) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 6419 (x,2) (%r1,0) (%r2,0) (%r3,2) (%r4,2) 5813 (x,2) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 1381 (x,2) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 2226 (x,2) (%r1,1) (%r2,1) (%r3,2) (%r4,2) 593 (x,2) (%r1,2) (%r2,2) (%r3,0) (%r4,0) 21999 (x,2) (%r1,2) (%r2,2) (%r3,1) (%r4,1) 28262 (x,2) (%r1,2) (%r2,2) (%r3,2) (%r4,2) 18903 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 22854 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,1) 2650 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,0) 6870 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,1) 29071 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,0) 9042 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,0) (%r6,1) 7 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,0) 794 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) (%r5,1) (%r6,1) 712 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,0) (%r6,0) 3524 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,0) (%r6,1) 1622 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) (%r5,1) (%r6,1) 762 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,0) 25725 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,1) 714 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0) 454 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,1) 95199 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 98858 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) 99375 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) 1767 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 101141 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) 672 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) 98187 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 2315 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 29387 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 36065 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 63734 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 26 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 64614 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 3859 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 12234 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 4722 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 7476 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,2) (%r4,1) 5526 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 5420 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 4766 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 10840 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,0) 5171 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1) 21 (x,1) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0) 10416 (x,1) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1) 12239 (x,1) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,0) 6603 (x,1) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,1) 10364 (x,2) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0) 8785 (x,2) (y,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 8380 (x,2) (y,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 13139 (x,2) (y,1) (%r1,1) (%r2,0) (%r3,2) (%r4,1) 10765 (x,2) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 7367 (x,2) (y,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 1 (x,2) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 9430 (x,2) (y,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 13349 (x,2) (y,1) (%r1,1) (%r2,1) (%r3,2) (%r4,1) 9120 (x,2) (y,1) (%r1,1) (%r2,2) (%r3,0) (%r4,0) 5785 (x,2) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,0) 5588 (x,2) (y,1) (%r1,1) (%r2,2) (%r3,1) (%r4,1) 16 (x,2) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,0) 4954 (x,2) (y,1) (%r1,1) (%r2,2) (%r3,2) (%r4,1) 7523 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 15555 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 452 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) 439 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 48483 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) 9457 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) 1 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0) 544 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) 12721 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0) 5070 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 1339 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 22142 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 20495 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 462 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 384 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 62456 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 10758 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 684 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) 372 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 47032 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) 13393 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) 7 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0) 554 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) 12357 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0) 904 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 1521 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 20469 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 24519 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 1380 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 198 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 65852 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 29995 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 15089 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) 966 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 5468 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) 686 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) 15 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0) 15503 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) 9506 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0) 28830 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 27293 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 294 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 19334 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 21565 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 12447 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 13009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 12962 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 427 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) 495 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 48701 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) 12699 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,1) 8 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0) 567 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) 12601 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0) 5677 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 1286 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 22669 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 18967 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 333 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 240 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 62368 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 842 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) 26282 (x,1) (y,1) (%r1,0) (%r2,2) (%r3,1) 1 (x,1) (y,1) (%r1,0) (%r2,2) (%r3,2) 40708 (x,1) (y,1) (%r1,1) (%r2,0) (%r3,0) 40 (x,1) (y,1) (%r1,1) (%r2,1) (%r3,1) 21 (x,1) (y,1) (%r1,1) (%r2,2) (%r3,2) 12 (x,2) (y,1) (%r1,0) (%r2,2) (%r3,2) 2 (x,2) (y,1) (%r1,1) (%r2,0) (%r3,0) 65732 (x,2) (y,1) (%r1,1) (%r2,1) (%r3,1) 64851 (x,2) (y,1) (%r1,1) (%r2,2) (%r3,2) 1509 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 24135 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 15038 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) 4746 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 7048 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) 260 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,0) 11649 (w,1) (x,1) (y,1) (z,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) 5391 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,0) 33371 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,0) (%r4,1) 31792 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,0) (%r3,1) (%r4,1) 313 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 15459 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 17239 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 14834 (w,1) (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 18725 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 31596 (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 221 (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,0) 5493 (x,1) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 5293 (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 5905 (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 32 (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,0) 11143 (x,1) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 13978 (x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0) 8623 (x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,0) 18373 (x,1) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1) 6702 (x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) 17699 (x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,0) (%r4,1) 10224 (x,2) (y,1) (z,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) 2784 (x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,0) 7389 (x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,0) (%r4,1) 24503 (x,2) (y,1) (z,1) (%r1,1) (%r2,1) (%r3,1) (%r4,1) 4336 (x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,0) 5419 (x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,0) (%r4,1) 12874 (x,2) (y,1) (z,1) (%r1,2) (%r2,2) (%r3,1) (%r4,1) 7413 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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) 18806 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,0) (%r6,1) (%r7,1) 12680 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,0) (%r7,0) 1517 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,0) (%r4,0) (%r5,1) (%r6,1) (%r7,1) 17648 (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) 734 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,0) (%r6,1) (%r7,1) 5 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,0) 1187 (x,1) (y,1) (%r1,0) (%r2,0) (%r3,1) (%r4,1) (%r5,1) (%r6,1) (%r7,1) 646 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,0) (%r6,0) (%r7,0) 987 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,0) (%r6,1) (%r7,1) 822 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,0) (%r4,0) (%r5,1) (%r6,1) (%r7,1) 290 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,0) (%r6,0) (%r7,0) 46931 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,0) (%r6,1) (%r7,1) 24983 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,1) (%r6,0) (%r7,0) 22031 (x,1) (y,1) (%r1,0) (%r2,1) (%r3,1) (%r4,1) (%r5,1) (%r6,1) (%r7,1) 50732 Computer processor : 0 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 0 siblings : 4 core id : 0 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4674.04 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 1 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 0 siblings : 4 core id : 1 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4580.15 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 2 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 0 siblings : 4 core id : 2 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4623.76 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 3 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 0 siblings : 4 core id : 3 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4668.86 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 4 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 1 siblings : 4 core id : 0 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4623.83 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 5 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 1 siblings : 4 core id : 1 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4623.85 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 6 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 1 siblings : 4 core id : 2 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4624.28 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 7 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 1 siblings : 4 core id : 3 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4580.60 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 8 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 2 siblings : 4 core id : 0 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4623.56 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 9 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 2 siblings : 4 core id : 1 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4624.16 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 10 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 2 siblings : 4 core id : 2 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4668.41 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 11 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 2 siblings : 4 core id : 3 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4623.91 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 12 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 3 siblings : 4 core id : 0 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4624.00 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 13 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 3 siblings : 4 core id : 1 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4623.68 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 14 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 3 siblings : 4 core id : 2 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4626.67 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate processor : 15 vendor_id : AuthenticAMD cpu family : 16 model : 2 model name : Quad-Core AMD Opteron(tm) Processor 8356 stepping : 3 cpu MHz : 2311.847 cache size : 512 KB physical id : 3 siblings : 4 core id : 3 cpu cores : 4 fpu : yes fpu_exception : yes cpuid level : 5 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 fxsr_opt pdpe1gb rdtscp lm 3dnowext 3dnow constant_tsc rep_good pni cx16 popcnt lahf_lm cmp_legacy svm extapic cr8_legacy altmovcr8 abm sse4a misalignsse 3dnowprefetch osvw bogomips : 4624.00 TLB size : 1024 4K pages clflush size : 64 cache_alignment : 64 address sizes : 48 bits physical, 48 bits virtual power management: ts ttp tm stc 100mhzsteps hwpstate Parameters #define PROC_1 0 #define PROC_2 4 #define PROC_3 2 #define PROC_4 5 #define V_NO #define NUMBER_OF_RUN 1000 #define SIZE_OF_TEST 200 #define BUFFER_SIZE 318000