[gen] oneloc tests with wrong post condition

[hugookeeffe]

We have found an issue when generating oneloc tests with one Po. These tests seem to be generating the post condition wrong.

In these tests it seems like the write value assigned to the final condition starts calculating between two communication edges, resulting in reads from the previous edge to give the wrong result.
E.g.:

AArch64 A
"Rfe PosRR Fre"
Generator=diyone7 (version 7.56+03)
Com=Rf Fr
Orig=Rfe PosRR Fre
{
0:X1=x;
1:X0=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W1,[X0] ;
 STR W0,[X1] | LDR W2,[X0] ;
exists (1:X1=1 /\ 1:X2=1)

In this example, the postcondition states that the second load reads from the write, even though it is part of Fre. One proposed solution would be to start writing values at the beginning of a communication edge chain (i.e. n.edge = com && n.prev.edge != com), ensuring that the values are properly assigned.

Whilst this seems to work for tests with a single non-communication node such as the one above, it is unclear if this logic still works for tests that have multiple non-communication nodes, e.g.:

AArch64 A
"Rfe PosRR Fre PosWR PosRR Fre"
Generator=diyone7 (version 7.56+03)
Com=Rf Fr Fr
Orig=Rfe PosRR Fre PosWR PosRR Fre
{
0:X1=x;
1:X0=x;
2:X1=x;
}
 P0          | P1          | P2          ;
 MOV W0,#2   | LDR W1,[X0] | MOV W0,#1   ;
 STR W0,[X1] | LDR W2,[X0] | STR W0,[X1] ;
             |             | LDR W2,[X1] ;
             |             | LDR W3,[X1] ;
exists ([x]=1 /\ 1:X1=2 /\ 1:X2=0 /\ 2:X2=1 /\ 2:X3=1)

The test above has the logic previously described assigned, however, I am uncertain whether this test is correct. Specifically, it is unclear what value the first load should be reading in the second thread.

I have made a patch illustrating this change here : (#705)

From this, I have two questions:
is the behaviour seen in the first test a bug, and if so does the linked patch fix this?
Is there a more fundamental issue with how oneloc is generating tests?

[relokin]

Thanks @hugookeeffe for reporting this. I had a little thought about this and I think what you explained makes sense:

In this example, the postcondition states that the second load reads from the write, even though it is part of Fre. One proposed solution would be to start writing values at the beginning of a communication edge chain (i.e. n.edge = com && n.prev.edge != com), ensuring that the values are properly assigned.

However, I am also wondering if we should also allow n.edge = com && n.next.edge != com, which would make the full condition look like:

n.edge = com && (n.next.edge != com || n.prev.edge != com)

I am not sure about the 2nd test, I don't know what the post-condition should look like, currently (before your patch), it would be:

exists ([x]=2 /\ 1:X1=1 /\ 1:X2=1 /\ 2:X2=2 /\ 2:X3=2)

which is satisfied by an execution which not forbidden.

After you patch it would be

exists ([x]=1 /\ 1:X1=2 /\ 1:X2=0 /\ 2:X2=1 /\ 2:X3=1)

which is not ideal because what the shape we're testing is really a coRR. But at least, it's a test that is forbidden which is a step forward.

[hugookeeffe]

Thanks for the comments @relokin !

With the second test you mentioned you aren't sure about the post-condition; is there anything in particular about what my patch would generate that you think is off?

in regards to n.edge = com && n.next.edge != com, I think that this would allow us to start from the middle of a sequence of communication edges.

For example, with Rfe PosRR Fre this logic would allow us to start at the beginning of the Rfe node. However, if we are applying writes sequentially, the write from the Fre would then be applied before its read (as we start at the Rfe's write, which is the same as the Fre's), resulting in the read from the Fre reading from its write. So If i am understanding correctly, I don't think we should apply this logic.

Does this make sense?