Commit b6ff3084 authored by Paul E. McKenney's avatar Paul E. McKenney
Browse files

tools/memory-model: Label MP tests' producers and consumers 



This commit adds comments that label the MP tests' producer and consumer
processes, and also that label the "exists" clause as the bad outcome.

Reported-by: default avatarJohannes Weiner <hannes@cmpxchg.org>
Signed-off-by: default avatarPaul E. McKenney <paulmck@kernel.org>
parent acc4bdc5

tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus

+3 −3
Original line number Diff line number Diff line
@@ -13,14 +13,14 @@ C MP+fencewmbonceonce+fencermbonceonce 
	int flag;

}



P0(int *buf, int *flag)

P0(int *buf, int *flag) // Producer

{

	WRITE_ONCE(*buf, 1);

	smp_wmb();

	WRITE_ONCE(*flag, 1);

}



P1(int *buf, int *flag)

P1(int *buf, int *flag) // Consumer

{

	int r0;

	int r1;
@@ -30,4 +30,4 @@ P1(int *buf, int *flag) 
	r1 = READ_ONCE(*buf);

}



exists (1:r0=1 /\ 1:r1=0)
 
exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)

tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus

+3 −3
Original line number Diff line number Diff line
@@ -15,13 +15,13 @@ C MP+onceassign+derefonce 
	int y=0;

}



P0(int *x, int **p)

P0(int *x, int **p) // Producer

{

	WRITE_ONCE(*x, 1);

	rcu_assign_pointer(*p, x);

}



P1(int *x, int **p)

P1(int *x, int **p) // Consumer

{

	int *r0;

	int r1;
@@ -32,4 +32,4 @@ P1(int *x, int **p) 
	rcu_read_unlock();

}



exists (1:r0=x /\ 1:r1=0)
 
exists (1:r0=x /\ 1:r1=0) (* Bad outcome. *)

tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus

+3 −3
Original line number Diff line number Diff line
@@ -15,7 +15,7 @@ C MP+polockmbonce+poacquiresilsil 
	int x;

}



P0(spinlock_t *lo, int *x)

P0(spinlock_t *lo, int *x) // Producer

{

	spin_lock(lo);

	smp_mb__after_spinlock();
@@ -23,7 +23,7 @@ P0(spinlock_t *lo, int *x) 
	spin_unlock(lo);

}



P1(spinlock_t *lo, int *x)

P1(spinlock_t *lo, int *x) // Consumer

{

	int r1;

	int r2;
@@ -34,4 +34,4 @@ P1(spinlock_t *lo, int *x) 
	r3 = spin_is_locked(lo);

}



exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
 
exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)

tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus

+3 −3
Original line number Diff line number Diff line
@@ -15,14 +15,14 @@ C MP+polockonce+poacquiresilsil 
	int x;

}



P0(spinlock_t *lo, int *x)

P0(spinlock_t *lo, int *x) // Producer

{

	spin_lock(lo);

	WRITE_ONCE(*x, 1);

	spin_unlock(lo);

}



P1(spinlock_t *lo, int *x)

P1(spinlock_t *lo, int *x) // Consumer

{

	int r1;

	int r2;
@@ -33,4 +33,4 @@ P1(spinlock_t *lo, int *x) 
	r3 = spin_is_locked(lo);

}



exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
 
exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)

tools/memory-model/litmus-tests/MP+polocks.litmus

+3 −3
Original line number Diff line number Diff line
@@ -17,7 +17,7 @@ C MP+polocks 
	int flag;

}



P0(int *buf, int *flag, spinlock_t *mylock)

P0(int *buf, int *flag, spinlock_t *mylock) // Producer

{

	WRITE_ONCE(*buf, 1);

	spin_lock(mylock);
@@ -25,7 +25,7 @@ P0(int *buf, int *flag, spinlock_t *mylock) 
	spin_unlock(mylock);

}



P1(int *buf, int *flag, spinlock_t *mylock)

P1(int *buf, int *flag, spinlock_t *mylock) // Consumer

{

	int r0;

	int r1;
@@ -36,4 +36,4 @@ P1(int *buf, int *flag, spinlock_t *mylock) 
	r1 = READ_ONCE(*buf);

}



exists (1:r0=1 /\ 1:r1=0)
 
exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)