Are the verification conditions unique in the tests generated by diyone7?

[wxmwy]

Hello, developer. If there are four decision parameters (x1,x2,x3,x4), it is considered relaxed as long as x1=0,x2 =0,x3 =0. That is, there are at most 2^4=16 test results, and two results are considered relaxed. Does diyone7 produce such a test? If so, is the verification condition all relaxed results (x1=0, x2=0, x3=0) or just one of them (x1=0, x2=0, x3=0, x4=0)?

In addition, I tried to reproduce such a test： https://github.com/litmus-tests/litmus-tests-x86/blob/main/tests/non-mixed-size/CO/CoRR1.litmus

X86_64 CoRR1
"Rfe PosRR Fre"
Generator=diyone7 (version 7.55+01(dev))
Com=Rf Fr
Orig=Rfe PosRR Fre
Align=
{
uint64_t x; uint64_t 1:rbx; uint64_t 1:rax;

}
 P0          | P1            ;
 movq $1,(x) | movq (x),%rax ;
             | movq (x),%rbx ;
forall
(x=1 /\ ((1:rbx=1 /\ (1:rax=1 \/ 1:rax=0)) \/ (1:rbx=0 /\ 1:rax=0)))

use:

diyone7 -arch X86_64 Rfe PosRR Fre

But i got "Unique location", is such test generation no longer supported?

[maranget]

Hi @wxmwy. I do not understand your first question. As to your second question, diyone7 will produce the test if you add the command line option -oneloc.

[wxmwy]

Thanks for your reply @maranget !

I mean, if a four-thread litmus test is used, the criteria for determining relaxed can be: (1) exists (0:r1=0 /\ 1:r1=0 /\ 2:r1 = 0 /\ 3:r1 = 0) or (2) exists (0:r1=0 /\ 1:r1=0 /\ 2:r1 = 0 /\ 3:r1 = 1)

The diy tool generated test will be (3) exists (0: r1 = 0 / \ 1: r1 = 0 / \ 2: r1 = 0) or one in (1) and (2)

Or does diy not generate such a test?

In fact, what I mean is, is the criterion for relax the set of all non-SC results or just one of them?

[maranget]

Generally speaking diy produces one exists final condition than characterise one Non-SC behavior. To generate more sophisticated conditions, one can combine several tools. Consider the following test:

% diyone7 -arch X86_64   PodWR Fre PodWR Fre PodWR Fre -norm
% cat 3.SB.litmus 
X86_64 3.SB
"PodWR Fre PodWR Fre PodWR Fre"
Generator=diyone7 (version 7.57+1)
Prefetch=0:x=F,0:y=T,1:y=F,1:z=T,2:z=F,2:x=T
Com=Fr Fr Fr
Orig=PodWR Fre PodWR Fre PodWR Fre
{
}
 P0            | P1            | P2            ;
 movl $1,(x)   | movl $1,(y)   | movl $1,(z)   ;
 movl (y),%eax | movl (z),%eax | movl (x),%eax ;
exists (0:rax=0 /\ 1:rax=0 /\ 2:rax=0)

The final condition here charaterises the cycle given as argument to diyone7: .

For a test that checks compliance with the SC model, one would first run the test on top of the SC model and translate the resulting outcome into a forall condition:

% herd7 -cat sc.cat 3.SB.litmus > SC
% mlog2cond7 -forall true -optcond true SC > sc.txt
% cat sc.txt
3.SB "forall 0:rax=1 /\ (1:rax=0 /\ (2:rax=0 \/ 2:rax=1) \/ 1:rax=1 /\ (2:rax=1 \/ 2:rax=0)) \/ 0:rax=0 /\ (1:rax=1 /\ (2:rax=1 \/ 2:rax=0) \/ 1:rax=0 /\ 2:rax=1)"

It then suffices to change the final condition of the test as follows:

% recond7 -conds sc.txt 3.SB.litmus | tee 3.SB+SC.litmus
X86_64 3.SB
"PodWR Fre PodWR Fre PodWR Fre"
Generator=diyone7 (version 7.57+1)
Prefetch=0:x=F,0:y=T,1:y=F,1:z=T,2:z=F,2:x=T
Com=Fr Fr Fr
Orig=PodWR Fre PodWR Fre PodWR Fre
{
}
 P0            | P1            | P2            ;
 movl $1,(x)   | movl $1,(y)   | movl $1,(z)   ;
 movl (y),%eax | movl (z),%eax | movl (x),%eax ;
forall 0:rax=1 /\ (1:rax=0 /\ (2:rax=0 \/ 2:rax=1) \/ 1:rax=1 /\ (2:rax=1 \/ 2:rax=0)) \/ 0:rax=0 /\ (1:rax=1 /\ (2:rax=1 \/ 2:rax=0) \/ 1:rax=0 /\ 2:rax=1)

[maranget]

Sometimes one wants a condition for the legal (here TSO) non-SC outcomes. In other words one wants the difference beetween the SC and TSO models. Consider another test SB+SB.litmus:

% cat SB+SB.litmus
X86_64 SB+SB
"PodWR Fre PodWR Fre+PodWR Fre PodWR Fre"

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

exists (0:rax=0 /\ 1:rax=0 /\ 2:rax=0 /\ 3:rax=0)

Let us compute the difference of models as a condition:

% herd7 SB+SB.litmus > TSO
% herd7 -cat sc.cat SB+SB.litmus > SC
% mcompare7 -cpos p.txt SC TSO
% mcompare7 -cpos p.txt -optcond true  SC TSO
*Diffs*
     |Kind | SC                                    TSO                                   
-----------------------------------------------------------------------------------------
-----------------------------------------------------------------------------------------
SB+SB|Allow| [0:rax=0; 1:rax=1; 2:rax=0; 3:rax=1;] +[0:rax=0; 1:rax=0; 2:rax=0; 3:rax=0;]
     |No   | [0:rax=0; 1:rax=1; 2:rax=1; 3:rax=0;] +[0:rax=0; 1:rax=0; 2:rax=0; 3:rax=1;]
     |     | [0:rax=0; 1:rax=1; 2:rax=1; 3:rax=1;] +[0:rax=0; 1:rax=0; 2:rax=1; 3:rax=0;]
     |     | [0:rax=1; 1:rax=0; 2:rax=0; 3:rax=1;] +[0:rax=0; 1:rax=0; 2:rax=1; 3:rax=1;]
     |     | [0:rax=1; 1:rax=0; 2:rax=1; 3:rax=0;] +[0:rax=0; 1:rax=1; 2:rax=0; 3:rax=0;]
     |     | [0:rax=1; 1:rax=0; 2:rax=1; 3:rax=1;] +[0:rax=1; 1:rax=0; 2:rax=0; 3:rax=0;]
     |     | [0:rax=1; 1:rax=1; 2:rax=0; 3:rax=1;] +[0:rax=1; 1:rax=1; 2:rax=0; 3:rax=0;]
     |     | [0:rax=1; 1:rax=1; 2:rax=1; 3:rax=0;]                                       
     |     | [0:rax=1; 1:rax=1; 2:rax=1; 3:rax=1;]                                       

!!! Warning positive differences in: +SB+SB

Finally, let us change the test condition:

% recond7 -conds p.txt SB+SB.litmus | tee SB+SB+NON-SC.litmus
X86_64 SB+SB
"PodWR Fre PodWR Fre+PodWR Fre PodWR Fre"

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

exists 0:rax=0 /\ (1:rax=0 /\ (2:rax=0 /\ (3:rax=1 \/ 3:rax=0) \/ 2:rax=1 /\ (3:rax=0 \/ 3:rax=1)) \/ 1:rax=1 /\ 2:rax=0 /\ 3:rax=0) \/ 0:rax=1 /\ 2:rax=0 /\ 3:rax=0 /\ (1:rax=0 \/ 1:rax=1)

We can now check again that 7 out of the 16 legal outcomes are non-SC with herd7 SB+SB+NON-SC.litmus, or run the test one hardware with litmus7 to see which of the non-SC tests appear.

See here for a more generic description of the idea,

[wxmwy]

Thank you for your detailed reply.