linux-kernel - Re: [PATCH memory-model 2/3] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite for Android: free password hash cracker in your pocket

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <Zg/M141yzwnwPbCi@andrea>
Date: Fri, 5 Apr 2024 12:05:11 +0200
From: Andrea Parri <parri.andrea@...il.com>
To: "Paul E. McKenney" <paulmck@...nel.org>
Cc: linux-kernel@...r.kernel.org, linux-arch@...r.kernel.org,
	kernel-team@...a.com, mingo@...nel.org, stern@...land.harvard.edu,
	will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
	npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
	luc.maranget@...ia.fr, akiyks@...il.com,
	Frederic Weisbecker <frederic@...nel.org>,
	Daniel Lustig <dlustig@...dia.com>,
	Joel Fernandes <joel@...lfernandes.org>,
	Mark Rutland <mark.rutland@....com>,
	Jonathan Corbet <corbet@....net>, linux-doc@...r.kernel.org
Subject: Re: [PATCH memory-model 2/3] Documentation/litmus-tests: Demonstrate
 unordered failing cmpxchg

>  DCL-broken.litmus
> -	Demonstrates that double-checked locking needs more than just
> -	the obvious lock acquisitions and releases.
> +    Demonstrates that double-checked locking needs more than just
> +    the obvious lock acquisitions and releases.
>  
>  DCL-fixed.litmus
> -	Demonstrates corrected double-checked locking that uses
> -	smp_store_release() and smp_load_acquire() in addition to the
> -	obvious lock acquisitions and releases.
> +    Demonstrates corrected double-checked locking that uses
> +    smp_store_release() and smp_load_acquire() in addition to the
> +    obvious lock acquisitions and releases.
>  
>  RM-broken.litmus
> -	Demonstrates problems with "roach motel" locking, where code is
> -	freely moved into lock-based critical sections.  This example also
> -	shows how to use the "filter" clause to discard executions that
> -	would be excluded by other code not modeled in the litmus test.
> -	Note also that this "roach motel" optimization is emulated by
> -	physically moving P1()'s two reads from x under the lock.
> +    Demonstrates problems with "roach motel" locking, where code is
> +    freely moved into lock-based critical sections.  This example also
> +    shows how to use the "filter" clause to discard executions that
> +    would be excluded by other code not modeled in the litmus test.
> +    Note also that this "roach motel" optimization is emulated by
> +    physically moving P1()'s two reads from x under the lock.
>  
> -	What is a roach motel?	This is from an old advertisement for
> -	a cockroach trap, much later featured in one of the "Men in
> -	Black" movies.	"The roaches check in.	They don't check out."
> +    What is a roach motel?  This is from an old advertisement for
> +    a cockroach trap, much later featured in one of the "Men in
> +    Black" movies.  "The roaches check in.  They don't check out."
>  
>  RM-fixed.litmus
> -	The counterpart to RM-broken.litmus, showing P0()'s two loads from
> -	x safely outside of the critical section.
> +    The counterpart to RM-broken.litmus, showing P0()'s two loads from
> +    x safely outside of the critical section.

AFAIU, the changes above belong to patch #1.  Looks like you realigned
the text, but forgot to integrate the changes in #1?


> +C cmpxchg-fail-ordered-1
> +
> +(*
> + * Result: Never
> + *
> + * Demonstrate that a failing cmpxchg() operation will act as a full
> + * barrier when followed by smp_mb__after_atomic().
> + *)
> +
> +{}
> +
> +P0(int *x, int *y, int *z)
> +{
> +	int r0;
> +	int r1;
> +
> +	WRITE_ONCE(*x, 1);
> +	r1 = cmpxchg(z, 1, 0);
> +	smp_mb__after_atomic();
> +	r0 = READ_ONCE(*y);
> +}
> +
> +P1(int *x, int *y, int *z)
> +{
> +	int r0;
> +
> +	WRITE_ONCE(*y, 1);
> +	r1 = cmpxchg(z, 1, 0);

P1's r1 is undeclared (so klitmus7 will complain).

The same observation holds for cmpxchg-fail-unordered-1.litmus.


> +	smp_mb__after_atomic();
> +	r0 = READ_ONCE(*x);
> +}
> +
> +locations[0:r1;1:r1]
> +exists (0:r0=0 /\ 1:r0=0)


> +C cmpxchg-fail-ordered-2
> +
> +(*
> + * Result: Never
> + *
> + * Demonstrate use of smp_mb__after_atomic() to make a failing cmpxchg
> + * operation have acquire ordering.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r0;
> +	int r1;
> +
> +	WRITE_ONCE(*x, 1);
> +	r1 = cmpxchg(y, 0, 1);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	int r0;
> +
> +	r1 = cmpxchg(y, 0, 1);
> +	smp_mb__after_atomic();
> +	r2 = READ_ONCE(*x);

P1's r1 and r2 are undeclared.  P0's r0 and P1's r0 are unused.

Same for cmpxchg-fail-unordered-2.litmus.

  Andrea