tools/memory-model: Add litmus test for full multicopy atomicity

SB+poonceonces.litmus

	As above, but without the smp_mb() invocations.

SB+rfionceonce-poonceonces.litmus

	This litmus test demonstrates that LKMM is not fully multicopy

	atomic.  (Neither is it other multicopy atomic.)  This litmus test

	also demonstrates the "locations" debugging aid, which designates

	additional registers and locations to be printed out in the dump

	of final states in the herd7 output.  Without the "locations"

	statement, only those registers and locations mentioned in the

	"exists" clause will be printed.

S+poonceonces.litmus

	As below, but without the smp_wmb() and acquire load.

C SB+rfionceonce-poonceonces

(*

 * Result: Sometimes

 *

 * This litmus test demonstrates that LKMM is not fully multicopy atomic.

 *)

{}

P0(int *x, int *y)

{

	int r1;

	int r2;

	WRITE_ONCE(*x, 1);

	r1 = READ_ONCE(*x);

	r2 = READ_ONCE(*y);

}

P1(int *x, int *y)

{

	int r3;

	int r4;

	WRITE_ONCE(*y, 1);

	r3 = READ_ONCE(*y);

	r4 = READ_ONCE(*x);

}

locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *)

exists (0:r2=0 /\ 1:r4=0)