Commit e30d0235 authored by Boqun Feng's avatar Boqun Feng Committed by Paul E. McKenney
Browse files

Documentation/litmus-tests/atomic: Add a test for smp_mb__after_atomic() 



We already use a litmus test in atomic_t.txt to describe atomic RMW +
smp_mb__after_atomic() is stronger than acquire (both the read and the
write parts are ordered). So make it a litmus test in atomic-tests
directory, so that people can access the litmus easily.

Additionally, change the processor numbers "P1, P2" to "P0, P1" in
atomic_t.txt for the consistency with the processor numbers in the
litmus test, which herd can handle.

Acked-by: default avatarAlan Stern <stern@rowland.harvard.edu>
Acked-by: default avatarAndrea Parri <parri.andrea@gmail.com>
Signed-off-by: default avatarBoqun Feng <boqun.feng@gmail.com>
Reviewed-by: default avatarJoel Fernandes (Google) <joel@joelfernandes.org>
Signed-off-by: default avatarPaul E. McKenney <paulmck@kernel.org>
parent 4dcd4d36

Documentation/atomic_t.txt

+5 −5
Original line number Diff line number Diff line
@@ -233,19 +233,19 @@ as well. Similarly, something like: 
is an ACQUIRE pattern (though very much not typical), but again the barrier is

strictly stronger than ACQUIRE. As illustrated:



  C strong-acquire

  C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire



  {

  }



  P1(int *x, atomic_t *y)

  P0(int *x, atomic_t *y)

  {

    r0 = READ_ONCE(*x);

    smp_rmb();

    r1 = atomic_read(y);

  }



  P2(int *x, atomic_t *y)

  P1(int *x, atomic_t *y)

  {

    atomic_inc(y);

    smp_mb__after_atomic();
@@ -253,14 +253,14 @@ strictly stronger than ACQUIRE. As illustrated: 
  }



  exists

  (r0=1 /\ r1=0)

  (0:r0=1 /\ 0:r1=0)



This should not happen; but a hypothetical atomic_inc_acquire() --

(void)atomic_fetch_inc_acquire() for instance -- would allow the outcome,

because it would not order the W part of the RMW against the following

WRITE_ONCE.  Thus:



  P1			P2

  P0			P1



			t = LL.acq *y (0)

			t++;

Documentation/litmus-tests/atomic/Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus

0 → 100644
+32 −0
Original line number Diff line number Diff line 
C Atomic-RMW+mb__after_atomic-is-stronger-than-acquire



(*

 * Result: Never

 *

 * Test that an atomic RMW followed by a smp_mb__after_atomic() is

 * stronger than a normal acquire: both the read and write parts of

 * the RMW are ordered before the subsequential memory accesses.

 *)



{

}



P0(int *x, atomic_t *y)

{

	int r0;

	int r1;



	r0 = READ_ONCE(*x);

	smp_rmb();

	r1 = atomic_read(y);

}



P1(int *x, atomic_t *y)

{

	atomic_inc(y);

	smp_mb__after_atomic();

	WRITE_ONCE(*x, 1);

}



exists

(0:r0=1 /\ 0:r1=0)

Documentation/litmus-tests/atomic/README

+5 −0
Original line number Diff line number Diff line
@@ -7,5 +7,10 @@ tools/memory-model/README. 
LITMUS TESTS

============



Atomic-RMW+mb__after_atomic-is-stronger-than-acquire

	Test that an atomic RMW followed by a smp_mb__after_atomic() is

	stronger than a normal acquire: both the read and write parts of

	the RMW are ordered before the subsequential memory accesses.



Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus

	Test that atomic_set() cannot break the atomicity of atomic RMWs.

CRA Git | Maintained and supported by SUSTech CRA and CCSE