Interpretation of exists (not(*)) conditions

[deepsrc]

Hi,
I need some help with understanding how the exists (not(*)) conditions at the end of the test needs to be interpreted.

Let's consider this test as an example.

======================================
LITMUS_FILE : non-mixed-size/HAND/CoRR-cleaninit.litmus
======================================
RISCV CoRR-cleaninit
(* adapted from HAND/CoRR.litmus, initialising 0:x5 instead of using an extra instruction*)
(* why is the final condition so complex? *)
{
0:x6=x;
0:x5=1;
1:x6=x;
}
 P0          | P1          ;
 sw x5,0(x6) | lw x5,0(x6) ;
             | lw x7,0(x6) ;
exists (not (x=1 /\ (1:x5=0 /\ (1:x7=0 \/ 1:x7=1) \/ 1:x5=1 /\ 1:x7=1)))

Does this mean that one of the values outside x=1 /\ (1:x5=0 /\ (1:x7=0 \/ 1:x7=1) \/ 1:x5=1 /\ 1:x7=1) this set may exist?

Isn't that incorrect as x is always supposed to contain 1 as a result of the store on P0?

[hernanponcedeleon]

You should interpret the final condition as a question rather than as a statement. Then a tool can say that it is not true such an execution exists

Condition exists (!x==1int && (1:x5==0int && (1:x7==0int || 1:x7==1int) || 1:x5==1int && 1:x7==1int))
No

[fshaked]

Hi @deepsrc,

In addition to what @hernanponcedeleon wrote, you shouldn't think of the assertion as part of any kind of specification. It's mostly a hint for why the litmus test might be interesting.

If you are testing H/W, you should use the litmus tool (or a similar tool) to collect results from the H/W under testing (you can find such results in the hw-results folder, for example). Those results are lists of exhibited final states, regardless of whether they satisfy the assertion or not. The H/W results should be compared, using the mcompare tool, to exhaustive executions of the model you are interested in (you can find those in the model-results folder). mcompare will tell you exactly which states in the H/W don't match the model. Those can be states that the H/W exhibit but the model did not (i.e. H/W is not sound), or states that the model allows but the H/W did not exhibit (this is expected, as usually H/W is not as relaxed as the model allows it to be).

All this mostly ignores the litmus assertion. Just to confuse you a bit, the litmus tool and the exhaustive executions of the model, both report which states satisfy the assertion, but this is not important.

Best,
Shaked

[PeterSewell]

On Tue, 29 Aug 2023 at 15:26, Shaked Flur ***@***.***> wrote: Hi @deepsrc <https://github.com/deepsrc>, In addition to what @hernanponcedeleon <https://github.com/hernanponcedeleon> wrote, you shouldn't think of the assertion as part of any kind of specification. It's mostly a hint for why the litmus test might be interesting. If you are testing H/W, you should use the litmus tool <https://diy.inria.fr/> (or a similar tool) to collect results from the H/W under testing (you can find such results in the hw-results folder, for example). Those results are lists of exhibited final states, regardless of whether they satisfy the assertion or not. The H/W results should be compared, using the mcompare tool <https://diy.inria.fr/>, to exhaustive executions of the model you are interested in (you can find those in the model-results folder). mcompare will tell you exactly which states in the H/W don't match the model. Those can be states that the H/W exhibit but the model did not (i.e. H/W is not sound), or states that the model allows but the H/W did not exhibit (this is expected, as usually H/W is not as relaxed as the model allows it to be). All this mostly ignores the litmus assertion. Just to confuse you a bit, the litmus tool and the exhaustive executions of the model, both report which states satisfy the assertion, but this is not important.

Just to add: the above is correct for comparing models using either rmem or herd - it's best to check the set of allowed final states where one can - but the isla-axiomatic SMT-based tool does check whether the assertion is exhibited by any legal execution, rather than producing such a list of exhibited final states.

…

Best, Shaked — Reply to this email directly, view it on GitHub <#12 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZUDAHVAAKMSIHNFQM3XXX3ZLANCNFSM6AAAAAA3XZTROA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[deepsrc]

Hi @fshaked @PeterSewell

Thanks for the clarification. I have one last question. In case the hardware produces a state outside of the states present in model-results/flag.logs for a given test, could that be considered as a possible violation?

[fshaked]

Yes, this indicates the H/W is exhibiting behaviour that the Flat model does not allow. Can you share the test and H/W states?