linux-kernel - Re: [WIP 0/3] Memory model and atomic API in Rust

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: Windows password security audit tool. GUI, reports in PDF.

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

Message-ID: <Zf7qGONJY33KdLCH@Boquns-Mac-mini.home>
Date: Sat, 23 Mar 2024 07:41:28 -0700
From: Boqun Feng <boqun.feng@...il.com>
To: Andrew Lunn <andrew@...n.ch>
Cc: Kent Overstreet <kent.overstreet@...ux.dev>,
	rust-for-linux@...r.kernel.org, linux-kernel@...r.kernel.org,
	linux-arch@...r.kernel.org, llvm@...ts.linux.dev,
	Miguel Ojeda <ojeda@...nel.org>,	Alex Gaynor <alex.gaynor@...il.com>,
	Wedson Almeida Filho <wedsonaf@...il.com>,	Gary Guo <gary@...yguo.net>,
	Björn Roy Baron <bjorn3_gh@...tonmail.com>,
	Benno Lossin <benno.lossin@...ton.me>,
	Andreas Hindborg <a.hindborg@...sung.com>,
	Alice Ryhl <aliceryhl@...gle.com>,
	Alan Stern <stern@...land.harvard.edu>,
	Andrea Parri <parri.andrea@...il.com>,	Will Deacon <will@...nel.org>,
	Peter Zijlstra <peterz@...radead.org>,
	Nicholas Piggin <npiggin@...il.com>,	David Howells <dhowells@...hat.com>,
	Jade Alglave <j.alglave@....ac.uk>,	Luc Maranget <luc.maranget@...ia.fr>,
	"Paul E. McKenney" <paulmck@...nel.org>,
	Akira Yokosawa <akiyks@...il.com>,	Daniel Lustig <dlustig@...dia.com>,
	Joel Fernandes <joel@...lfernandes.org>,
	Nathan Chancellor <nathan@...nel.org>,
	Nick Desaulniers <ndesaulniers@...gle.com>,	kent.overstreet@...il.com,
	Greg Kroah-Hartman <gregkh@...uxfoundation.org>, elver@...gle.com,
	Mark Rutland <mark.rutland@....com>,
	Thomas Gleixner <tglx@...utronix.de>,	Ingo Molnar <mingo@...hat.com>,
 Borislav Petkov <bp@...en8.de>,
	Dave Hansen <dave.hansen@...ux.intel.com>, x86@...nel.org,
	"H. Peter Anvin" <hpa@...or.com>,
	Catalin Marinas <catalin.marinas@....com>,	torvalds@...ux-foundation.org,
 linux-arm-kernel@...ts.infradead.org,	linux-fsdevel@...r.kernel.org
Subject: Re: [WIP 0/3] Memory model and atomic API in Rust

On Sat, Mar 23, 2024 at 03:29:11PM +0100, Andrew Lunn wrote:
> > There are also issues like where one Rust thread does a store(..,
> > RELEASE), and a C thread does a rcu_deference(), in practice, it
> > probably works but no one works out (and no one would work out) a model
> > to describe such an interaction.
> 
> Isn't that what Paul E. McKenney litmus tests are all about?
> 

Litmus tests (or herd, or any other memory model tools) works for either
LKMM or C++ memory model. But there is no model I'm aware of works for
the communication between two memory models. So for example:

	Rust thread:

	let mut foo: Box<Foo> = ...;
	foo.a = 1;
	let global_ptr: &AtomicPtr = ...;
	global_ptr.store(foo.leak() as _, RELEASE);

	
	C thread:

	rcu_read_lock();

	foo = rcu_dereference(global_ptr);
	if (foo) {
		r1 = foo->a;
	}
	
	rcu_read_unlock();

no tool or model yet to guarantee "r1" is 1, but yeah, in practice for
the case we care, it's probably guaranteed. But no tool or model means
challenging for code reasoning.

Regards,
Boqun

> tools/memory-model/litmus-test
> 
> 	Andrew