Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)

[Paul E. McKenney]

On Fri, Jan 13, 2023 at 08:43:42PM +0000, Jonas Oberhauser wrote:
> 
> 
> -----Original Message-----
> From: Paul E. McKenney [mailto:paulmck@xxxxxxxxxx] 
> 
> > (* Compute matching pairs of Srcu-lock and Srcu-unlock *) let srcu-rscs = ([Srcu-lock] ; rfi ; [Srcu-unlock]) & loc
> 
> How does the Srcu-unlock read from the Srcu-lock? Is there something in your model or in herd that lets it understand lock and unlock should be treated as writes resp. reads from that specific location?
> 
> Or do you mean that value given to Srcu-unlock should be the value produced by Srcu-lock?

Yes, and in the Linux kernel one does something like this:

	idx = srcu_read_lock(&mysrcu);
	// critical section
	srcu_read_unlock(&mysrcu, idx);

> Perhaps the closest to what you want is to express that as a data dependency if you know how to teach herd that Srcu-unlock is a read and Srcu-lock depends on its second input :D (I have no idea how to do that, hence the questions above)

Given that both you and Alan suggested it, I must try it.  ;-)

> Then you could flag if there's a data dependency from more than one event, meaning that the value is not purely the Srcu-lock-produced value.

Good point, thank you!

> That doesn't guarantee you that you don't do some nasty stuff with constant values though. 

That is the purpose of this statement in the srcu_read_unlock()
implementation:

	WARN_ON_ONCE(idx & ~0x1);

But yes, this WARN_ON_ONCE() can of course be fooled.

> Could you maybe use an opaque datatype for the values?

We could put it in a struct or something.  The problem with making it
completely opaque is that the users must store it somewhere, which means
that the compiler needs to know how big it is.  Of course, languages
other than C have other ways to make this happen.  And correspondingly
slower build times.  ;-)

							Thanx, Paul