[mirror_ubuntu-hirsute-kernel.git] / tools / memory-model / litmus-tests / LB+poacquireonce+pooncerelease.litmus

C LB+poacquireonce+pooncerelease

(*
 * Result: Never
 *
 * Does a release-acquire pair suffice for the load-buffering litmus
 * test, where each process reads from one of two variables then writes
 * to the other?
 *)

{}

P0(int *x, int *y)
{
	int r0;

	r0 = READ_ONCE(*x);
	smp_store_release(y, 1);
}

P1(int *x, int *y)
{
	int r0;

	r0 = smp_load_acquire(y);
	WRITE_ONCE(*x, 1);
}

exists (0:r0=1 /\ 1:r0=1)
Commit	Line	Data
1c27b644 PM	1	C LB+poacquireonce+pooncerelease
1c27b644 PM	2
8f32543b PM	3	(*
	4	* Result: Never
	5	*
	6	* Does a release-acquire pair suffice for the load-buffering litmus
	7	* test, where each process reads from one of two variables then writes
	8	* to the other?
	9	*)
	10
1c27b644 PM	11	{}
	12
	13	P0(int x, int y)
	14	{
	15	int r0;
	16
	17	r0 = READ_ONCE(*x);
	18	smp_store_release(y, 1);
	19	}
	20
	21	P1(int x, int y)
	22	{
	23	int r0;
	24
	25	r0 = smp_load_acquire(y);
	26	WRITE_ONCE(*x, 1);
	27	}
	28
	29	exists (0:r0=1 /\ 1:r0=1)