Fri Jan 12 04:55:00 PM CET 2024
%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for SB.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 SB
"PodWR Fre PodWR Fre"

{
}
 P0            | P1            ;
 movl $1,(x)   | movl $1,(y)   ;
 movl (y),%eax | movl (x),%eax ;

exists (0:rax=0 /\ 1:rax=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	movl (%rsi),%eax
#START _litmus_P1
	movl $1,(%rsi)
	movl (%rdi),%eax
Test SB Allowed
Histogram (4 states)
731   *>0:rax=0; 1:rax=0;
2999598:>0:rax=1; 1:rax=0;
2999643:>0:rax=0; 1:rax=1;
28    :>0:rax=1; 1:rax=1;
Ok

Witnesses
Positive: 731, Negative: 5999269
Condition exists (0:rax=0 /\ 1:rax=0) is validated
Hash=055f9747fd517835a93f2f188e15e163
Cycle=Fre PodWR Fre PodWR
Generator=diycross7 (version 7.56+03)
Com=Fr Fr
Orig=PodWR Fre PodWR Fre
Observation SB Sometimes 731 5999269
Time SB 0.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for SB+mfence+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 SB+mfence+po
"MFencedWR Fre PodWR Fre"

{
}
 P0            | P1            ;
 movl $1,(x)   | movl $1,(y)   ;
 mfence        | movl (x),%eax ;
 movl (y),%eax |               ;

exists (0:rax=0 /\ 1:rax=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	mfence
	movl (%rsi),%eax
#START _litmus_P1
	movl $1,(%rsi)
	movl (%rdi),%eax
Test SB+mfence+po Allowed
Histogram (4 states)
7     *>0:rax=0; 1:rax=0;
3000198:>0:rax=1; 1:rax=0;
2996277:>0:rax=0; 1:rax=1;
3518  :>0:rax=1; 1:rax=1;
Ok

Witnesses
Positive: 7, Negative: 5999993
Condition exists (0:rax=0 /\ 1:rax=0) is validated
Hash=19317c3c2de40cc3e21bb396dc5d2961
Cycle=Fre PodWR Fre MFencedWR
Generator=diycross7 (version 7.56+03)
Com=Fr Fr
Orig=MFencedWR Fre PodWR Fre
Observation SB+mfence+po Sometimes 7 5999993
Time SB+mfence+po 0.32
%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 R
"PodWW Coe PodWR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl $2,(y)   ;
 movl $1,(y) | movl (x),%eax ;

exists ([y]=2 /\ 1:rax=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	movl $1,(%rsi)
#START _litmus_P1
	movl $2,(%rsi)
	movl (%rdi),%eax
Test R Allowed
Histogram (4 states)
3000510:>1:rax=0; [y]=1;
3556  :>1:rax=1; [y]=1;
61    *>1:rax=0; [y]=2;
2995873:>1:rax=1; [y]=2;
Ok

Witnesses
Positive: 61, Negative: 5999939
Condition exists ([y]=2 /\ 1:rax=0) is validated
Hash=b66b3ce129b44b61416afa21c7cc6972
Cycle=Fre PodWW Coe PodWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=PodWW Coe PodWR Fre
Observation R Sometimes 61 5999939
Time R 0.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R+mfence+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 R+mfence+po
"MFencedWW Coe PodWR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl $2,(y)   ;
 mfence      | movl (x),%eax ;
 movl $1,(y) |               ;

exists ([y]=2 /\ 1:rax=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl $2,(%rsi)
	movl (%rdi),%eax
Test R+mfence+po Allowed
Histogram (4 states)
3000634:>1:rax=0; [y]=1;
8905  :>1:rax=1; [y]=1;
16    *>1:rax=0; [y]=2;
2990445:>1:rax=1; [y]=2;
Ok

Witnesses
Positive: 16, Negative: 5999984
Condition exists ([y]=2 /\ 1:rax=0) is validated
Hash=8fb1341c0cc04121abffe4a6c0950341
Cycle=Fre MFencedWW Coe PodWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=MFencedWW Coe PodWR Fre
Observation R+mfence+po Sometimes 16 5999984
Time R+mfence+po 0.30
%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 MP
"PodWW Rfe PodRR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl (y),%eax ;
 movl $1,(y) | movl (x),%ebx ;

exists (1:rax=1 /\ 1:rbx=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	movl $1,(%rsi)
#START _litmus_P1
	movl (%r8),%eax
	movl (%rdi),%esi
Test MP Allowed
Histogram (3 states)
3000205:>1:rax=0; 1:rbx=0;
33323 :>1:rax=0; 1:rbx=1;
2966472:>1:rax=1; 1:rbx=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (1:rax=1 /\ 1:rbx=0) is NOT validated
Hash=31b99cfc4847232dfdc0acc372e4fe78
Cycle=Rfe PodRR Fre PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=PodWW Rfe PodRR Fre
Observation MP Never 0 6000000
Time MP 0.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP+mfence+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 MP+mfence+po
"MFencedWW Rfe PodRR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl (y),%eax ;
 mfence      | movl (x),%ebx ;
 movl $1,(y) |               ;

exists (1:rax=1 /\ 1:rbx=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl (%r8),%eax
	movl (%rdi),%esi
Test MP+mfence+po Allowed
Histogram (3 states)
3000590:>1:rax=0; 1:rbx=0;
158264:>1:rax=0; 1:rbx=1;
2841146:>1:rax=1; 1:rbx=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (1:rax=1 /\ 1:rbx=0) is NOT validated
Hash=5604bc7b4a6d7596d31c1675d771f100
Cycle=Rfe PodRR Fre MFencedWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=MFencedWW Rfe PodRR Fre
Observation MP+mfence+po Never 0 6000000
Time MP+mfence+po 0.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for SB+mfences.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 SB+mfences
"MFencedWR Fre MFencedWR Fre"

{
}
 P0            | P1            ;
 movl $1,(x)   | movl $1,(y)   ;
 mfence        | mfence        ;
 movl (y),%eax | movl (x),%eax ;

exists (0:rax=0 /\ 1:rax=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	mfence
	movl (%rsi),%eax
#START _litmus_P1
	movl $1,(%rsi)
	mfence
	movl (%rdi),%eax
Test SB+mfences Allowed
Histogram (3 states)
2995070:>0:rax=1; 1:rax=0;
2995456:>0:rax=0; 1:rax=1;
9474  :>0:rax=1; 1:rax=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (0:rax=0 /\ 1:rax=0) is NOT validated
Hash=927b984265892178e3f1f0753929d0cd
Cycle=Fre MFencedWR Fre MFencedWR
Generator=diycross7 (version 7.56+03)
Com=Fr Fr
Orig=MFencedWR Fre MFencedWR Fre
Observation SB+mfences Never 0 6000000
Time SB+mfences 0.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R+po+mfence.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 R+po+mfence
"PodWW Coe MFencedWR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl $2,(y)   ;
 movl $1,(y) | mfence        ;
             | movl (x),%eax ;

exists ([y]=2 /\ 1:rax=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	movl $1,(%rsi)
#START _litmus_P1
	movl $2,(%rsi)
	mfence
	movl (%rdi),%eax
Test R+po+mfence Allowed
Histogram (3 states)
2998930:>1:rax=0; [y]=1;
5476  :>1:rax=1; [y]=1;
2995594:>1:rax=1; [y]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([y]=2 /\ 1:rax=0) is NOT validated
Hash=c7c970fdedb04feea0a03d93eafe2c5c
Cycle=Fre PodWW Coe MFencedWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=PodWW Coe MFencedWR Fre
Observation R+po+mfence Never 0 6000000
Time R+po+mfence 0.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for R+mfences.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 R+mfences
"MFencedWW Coe MFencedWR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl $2,(y)   ;
 mfence      | mfence        ;
 movl $1,(y) | movl (x),%eax ;

exists ([y]=2 /\ 1:rax=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl $2,(%rsi)
	mfence
	movl (%rdi),%eax
Test R+mfences Allowed
Histogram (3 states)
2998716:>1:rax=0; [y]=1;
10152 :>1:rax=1; [y]=1;
2991132:>1:rax=1; [y]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([y]=2 /\ 1:rax=0) is NOT validated
Hash=7959e75eb0356a95501150d07daf1488
Cycle=Fre MFencedWW Coe MFencedWR
Generator=diycross7 (version 7.56+03)
Com=Co Fr
Orig=MFencedWW Coe MFencedWR Fre
Observation R+mfences Never 0 6000000
Time R+mfences 0.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP+po+mfence.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 MP+po+mfence
"PodWW Rfe MFencedRR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl (y),%eax ;
 movl $1,(y) | mfence        ;
             | movl (x),%ebx ;

exists (1:rax=1 /\ 1:rbx=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	movl $1,(%rsi)
#START _litmus_P1
	movl (%r8),%eax
	mfence
	movl (%rdi),%esi
Test MP+po+mfence Allowed
Histogram (3 states)
2998750:>1:rax=0; 1:rbx=0;
7523  :>1:rax=0; 1:rbx=1;
2993727:>1:rax=1; 1:rbx=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (1:rax=1 /\ 1:rbx=0) is NOT validated
Hash=6968e69e5f9297bce75094491b8e6fd3
Cycle=Rfe MFencedRR Fre PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=PodWW Rfe MFencedRR Fre
Observation MP+po+mfence Never 0 6000000
Time MP+po+mfence 0.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for MP+mfences.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 MP+mfences
"MFencedWW Rfe MFencedRR Fre"

{
}
 P0          | P1            ;
 movl $1,(x) | movl (y),%eax ;
 mfence      | mfence        ;
 movl $1,(y) | movl (x),%ebx ;

exists (1:rax=1 /\ 1:rbx=0)
Generated assembler
#START _litmus_P0
	movl $1,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl (%r8),%eax
	mfence
	movl (%rdi),%esi
Test MP+mfences Allowed
Histogram (3 states)
2998554:>1:rax=0; 1:rbx=0;
33229 :>1:rax=0; 1:rbx=1;
2968217:>1:rax=1; 1:rbx=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (1:rax=1 /\ 1:rbx=0) is NOT validated
Hash=bb8b1083ff652c5f4dd226e273c6394a
Cycle=Rfe MFencedRR Fre MFencedWW
Generator=diycross7 (version 7.56+03)
Com=Rf Fr
Orig=MFencedWW Rfe MFencedRR Fre
Observation MP+mfences Never 0 6000000
Time MP+mfences 0.34
%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 S
"PodWW Rfe PodRW Coe"

{
}
 P0          | P1            ;
 movl $2,(x) | movl (y),%eax ;
 movl $1,(y) | movl $1,(x)   ;

exists ([x]=2 /\ 1:rax=1)
Generated assembler
#START _litmus_P0
	movl $2,(%rdi)
	movl $1,(%rsi)
#START _litmus_P1
	movl (%rsi),%eax
	movl $1,(%rdi)
Test S Allowed
Histogram (3 states)
20353 :>1:rax=0; [x]=1;
2979655:>1:rax=1; [x]=1;
2999992:>1:rax=0; [x]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([x]=2 /\ 1:rax=1) is NOT validated
Hash=d04c589784a76284bcc284b161c38db6
Cycle=Rfe PodRW Coe PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=PodWW Rfe PodRW Coe
Observation S Never 0 6000000
Time S 0.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S+po+mfence.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 S+po+mfence
"PodWW Rfe MFencedRW Coe"

{
}
 P0          | P1            ;
 movl $2,(x) | movl (y),%eax ;
 movl $1,(y) | mfence        ;
             | movl $1,(x)   ;

exists ([x]=2 /\ 1:rax=1)
Generated assembler
#START _litmus_P0
	movl $2,(%rdi)
	movl $1,(%rsi)
#START _litmus_P1
	movl (%rsi),%eax
	mfence
	movl $1,(%rdi)
Test S+po+mfence Allowed
Histogram (3 states)
2238  :>1:rax=0; [x]=1;
2998812:>1:rax=1; [x]=1;
2998950:>1:rax=0; [x]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([x]=2 /\ 1:rax=1) is NOT validated
Hash=61e1de21a70746a0249616c175fabc4f
Cycle=Rfe MFencedRW Coe PodWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=PodWW Rfe MFencedRW Coe
Observation S+po+mfence Never 0 6000000
Time S+po+mfence 0.32
%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for LB.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 LB
"PodRW Rfe PodRW Rfe"

{
}
 P0            | P1            ;
 movl (x),%eax | movl (y),%eax ;
 movl $1,(y)   | movl $1,(x)   ;

exists (0:rax=1 /\ 1:rax=1)
Generated assembler
#START _litmus_P0
	movl (%rdi),%eax
	movl $1,(%rsi)
#START _litmus_P1
	movl (%rsi),%eax
	movl $1,(%rdi)
Test LB Allowed
Histogram (3 states)
654   :>0:rax=0; 1:rax=0;
2999666:>0:rax=1; 1:rax=0;
2999680:>0:rax=0; 1:rax=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (0:rax=1 /\ 1:rax=1) is NOT validated
Hash=37842746c7cdd7427ed57f09a03afc35
Cycle=Rfe PodRW Rfe PodRW
Generator=diycross7 (version 7.56+03)
Com=Rf Rf
Orig=PodRW Rfe PodRW Rfe
Observation LB Never 0 6000000
Time LB 0.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for LB+mfence+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 LB+mfence+po
"MFencedRW Rfe PodRW Rfe"

{
}
 P0            | P1            ;
 movl (x),%eax | movl (y),%eax ;
 mfence        | movl $1,(x)   ;
 movl $1,(y)   |               ;

exists (0:rax=1 /\ 1:rax=1)
Generated assembler
#START _litmus_P0
	movl (%rdi),%eax
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl (%rsi),%eax
	movl $1,(%rdi)
Test LB+mfence+po Allowed
Histogram (3 states)
79478 :>0:rax=0; 1:rax=0;
2999762:>0:rax=1; 1:rax=0;
2920760:>0:rax=0; 1:rax=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (0:rax=1 /\ 1:rax=1) is NOT validated
Hash=c2efa11c0fa03649ed5b7398dca3e1f7
Cycle=Rfe PodRW Rfe MFencedRW
Generator=diycross7 (version 7.56+03)
Com=Rf Rf
Orig=MFencedRW Rfe PodRW Rfe
Observation LB+mfence+po Never 0 6000000
Time LB+mfence+po 0.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S+mfence+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 S+mfence+po
"MFencedWW Rfe PodRW Coe"

{
}
 P0          | P1            ;
 movl $2,(x) | movl (y),%eax ;
 mfence      | movl $1,(x)   ;
 movl $1,(y) |               ;

exists ([x]=2 /\ 1:rax=1)
Generated assembler
#START _litmus_P0
	movl $2,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl (%rsi),%eax
	movl $1,(%rdi)
Test S+mfence+po Allowed
Histogram (3 states)
180293:>1:rax=0; [x]=1;
2819731:>1:rax=1; [x]=1;
2999976:>1:rax=0; [x]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([x]=2 /\ 1:rax=1) is NOT validated
Hash=9b46c46f1b1c44ac6ebef1c0b479a5c5
Cycle=Rfe PodRW Coe MFencedWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=MFencedWW Rfe PodRW Coe
Observation S+mfence+po Never 0 6000000
Time S+mfence+po 0.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for S+mfences.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 S+mfences
"MFencedWW Rfe MFencedRW Coe"

{
}
 P0          | P1            ;
 movl $2,(x) | movl (y),%eax ;
 mfence      | mfence        ;
 movl $1,(y) | movl $1,(x)   ;

exists ([x]=2 /\ 1:rax=1)
Generated assembler
#START _litmus_P0
	movl $2,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl (%rsi),%eax
	mfence
	movl $1,(%rdi)
Test S+mfences Allowed
Histogram (3 states)
21193 :>1:rax=0; [x]=1;
2979679:>1:rax=1; [x]=1;
2999128:>1:rax=0; [x]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([x]=2 /\ 1:rax=1) is NOT validated
Hash=0e4bfa1f40d55103ac2579146fbdb2ba
Cycle=Rfe MFencedRW Coe MFencedWW
Generator=diycross7 (version 7.56+03)
Com=Rf Co
Orig=MFencedWW Rfe MFencedRW Coe
Observation S+mfences Never 0 6000000
Time S+mfences 0.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for LB+mfences.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 LB+mfences
"MFencedRW Rfe MFencedRW Rfe"

{
}
 P0            | P1            ;
 movl (x),%eax | movl (y),%eax ;
 mfence        | mfence        ;
 movl $1,(y)   | movl $1,(x)   ;

exists (0:rax=1 /\ 1:rax=1)
Generated assembler
#START _litmus_P0
	movl (%rdi),%eax
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl (%rsi),%eax
	mfence
	movl $1,(%rdi)
Test LB+mfences Allowed
Histogram (3 states)
21253 :>0:rax=0; 1:rax=0;
2988222:>0:rax=1; 1:rax=0;
2990525:>0:rax=0; 1:rax=1;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists (0:rax=1 /\ 1:rax=1) is NOT validated
Hash=a42b81f5f6896f3fb7f013a9307defa1
Cycle=Rfe MFencedRW Rfe MFencedRW
Generator=diycross7 (version 7.56+03)
Com=Rf Rf
Orig=MFencedRW Rfe MFencedRW Rfe
Observation LB+mfences Never 0 6000000
Time LB+mfences 0.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for 2+2W.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 2+2W
"PodWW Coe PodWW Coe"

{
}
 P0          | P1          ;
 movl $2,(x) | movl $2,(y) ;
 movl $1,(y) | movl $1,(x) ;

exists ([x]=2 /\ [y]=2)
Generated assembler
#START _litmus_P0
	movl $2,(%rdi)
	movl $1,(%rsi)
#START _litmus_P1
	movl $2,(%rsi)
	movl $1,(%rdi)
Test 2+2W Allowed
Histogram (3 states)
382   :>[x]=1; [y]=1;
2999817:>[x]=2; [y]=1;
2999801:>[x]=1; [y]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([x]=2 /\ [y]=2) is NOT validated
Hash=cf8b5379389ded920e2996197a2e5d0c
Cycle=Coe PodWW Coe PodWW
Generator=diycross7 (version 7.56+03)
Com=Co Co
Orig=PodWW Coe PodWW Coe
Observation 2+2W Never 0 6000000
Time 2+2W 0.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for 2+2W+mfence+po.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 2+2W+mfence+po
"MFencedWW Coe PodWW Coe"

{
}
 P0          | P1          ;
 movl $2,(x) | movl $2,(y) ;
 mfence      | movl $1,(x) ;
 movl $1,(y) |             ;

exists ([x]=2 /\ [y]=2)
Generated assembler
#START _litmus_P0
	movl $2,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl $2,(%rsi)
	movl $1,(%rdi)
Test 2+2W+mfence+po Allowed
Histogram (3 states)
4900  :>[x]=1; [y]=1;
2999729:>[x]=2; [y]=1;
2995371:>[x]=1; [y]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([x]=2 /\ [y]=2) is NOT validated
Hash=779200c1aeca1a146a8ba71d74b574b0
Cycle=Coe PodWW Coe MFencedWW
Generator=diycross7 (version 7.56+03)
Com=Co Co
Orig=MFencedWW Coe PodWW Coe
Observation 2+2W+mfence+po Never 0 6000000
Time 2+2W+mfence+po 0.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for 2+2W+mfences.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
X86_64 2+2W+mfences
"MFencedWW Coe MFencedWW Coe"

{
}
 P0          | P1          ;
 movl $2,(x) | movl $2,(y) ;
 mfence      | mfence      ;
 movl $1,(y) | movl $1,(x) ;

exists ([x]=2 /\ [y]=2)
Generated assembler
#START _litmus_P0
	movl $2,(%rdi)
	mfence
	movl $1,(%rsi)
#START _litmus_P1
	movl $2,(%rsi)
	mfence
	movl $1,(%rdi)
Test 2+2W+mfences Allowed
Histogram (3 states)
10132 :>[x]=1; [y]=1;
2995026:>[x]=2; [y]=1;
2994842:>[x]=1; [y]=2;
No

Witnesses
Positive: 0, Negative: 6000000
Condition exists ([x]=2 /\ [y]=2) is NOT validated
Hash=d7b072e85e7817477661e09815ac08b0
Cycle=Coe MFencedWW Coe MFencedWW
Generator=diycross7 (version 7.56+03)
Com=Co Co
Orig=MFencedWW Coe MFencedWW Coe
Observation 2+2W+mfences Never 0 6000000
Time 2+2W+mfences 0.32
Revision 0d2618c15372514c72a90b12caa6b5ca4f144e42, version 7.56+03
Command line: litmus7 -mach x86_64 -a 12 -o R @all
Parameters
#define SIZE_OF_TEST 5000
#define NUMBER_OF_RUN 200
#define AVAIL 12
#define STRIDE 1
#define MAX_LOOP 0
/* gcc options: -D_GNU_SOURCE -Wall -std=gnu99 -fomit-frame-pointer -O2 -pthread */
/* barrier: user */
/* launch: changing */
/* affinity: incr0 */
/* memory: direct */
/* stride: 1 */
/* safer: write */
/* preload: random */
/* speedcheck: no */
/* alloc: dynamic */
/* proc used: 12 */
GCC=gcc
LITMUSOPTS=
Fri Jan 12 04:55:07 PM CET 2024