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

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



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




[Index of Archives]     [Linux Kernel]     [Kernel Newbies]     [x86 Platform Driver]     [Netdev]     [Linux Wireless]     [Netfilter]     [Bugtraq]     [Linux Filesystems]     [Yosemite Discussion]     [MIPS Linux]     [ARM Linux]     [Linux Security]     [Linux RAID]     [Samba]     [Device Mapper]

  Powered by Linux