Test MP

AArch64 MP
"PodWW Rfe PodRR Fre"

(* This is a two-thread message-passing (MP) test: Thread 0 writes to
x and y, while Thread 1 reads from y and x.  The interesting question
is whether Thread 1 can see Thread 0's write to y and (in the same
execution) read x from the initial state.*)

(* The initial-state setup, of memory values (here x and y are
implicitly initially 0) and of register values for each thread: *)
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}

(* The assembly code for each thread: *)
 P0                      | P1                      ;
 MOV W0,#1               | LDR W0,[X1]  (* Ry=1 *) ;
 STR W0,[X1]  (* Wx=1 *) | LDR W2,[X3]  (* Rx=0 *) ;
 MOV W2,#1               |                         ;
 STR W2,[X3]  (* Wy=1 *) |                         ;

(* The final-state condition, identifying the interesting execution: *)

exists
(1:X0=1 /\ 1:X2=0)


(* In general the final condition might be allowed or forbidden on any
specific model, and might be observable or not observable
experimentally on any specific hardware implementation.  For this
test, the final condition identifies the execution shown in the
comments, in which Thread 1 (P1) sees the Thread 0 write of y=1 but
reads the initial-state value x=0 for x, without seeing the Thread 0
write of x=1.  This is a non-sequentially-consistent execution; it is
allowed by the ARM architecture and observable on many ARM
implementations. *)

(* This test was generated by the "diy" tool from the description, on
the second line, of a cycle of edges in a potential
non-sequentially-consistent execution:

  PodWW : a program-order edge (Po), between two write accesses (WW)
          to different addresses (d)
  Rfe   : a reads-from edge (Rf) that is "external" (e), ie inter-thread
  PodRR : a program-order edge (Po), between two read accesses (RR) 
          from different addresses (d) 
  Fre   : a from-reads edge, from a read to a coherence successor of the 
            write it reads from, that is "external" (e), ie inter-thread
*)

(* The following is additional data from the generation process, and a
prefetch hint that can be useful when running the test experimentally
on hardware.

Cycle=Rfe PodRR Fre PodWW
Relax=
Safe=Rfe Fre PodWW PodRR
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
Com=Rf Fr
Orig=PodWW Rfe PodRR Fre
*)