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
