Re: Current LKMM patch disposition

[Alan Stern]

On Sat, Feb 11, 2023 at 07:30:32PM -0500, Joel Fernandes wrote:
> On Sat, Feb 11, 2023 at 3:19 PM Alan Stern <stern@xxxxxxxxxxxxxxxxxxx> wrote:
> > The idea is that the value returned by srcu_read_lock() can be stored to
> > and loaded from a sequence (possibly of length 0) of variables, and the
> > final load gets fed to srcu_read_unlock().  That's what the original
> > version of the code expresses.
> 
> Now I understand it somewhat, and I see where I went wrong. Basically,
> you were trying to sequence zero or one "data + rf sequence" starting
> from lock and unlock with a final "data" sequence. That data sequence
> can be between the srcu-lock and srcu-unlock itself, in case where the
> lock/unlock happened on the same CPU.

In which case the sequence has length 0.  Exactly right.

> Damn, that's really complicated.. and I still don't fully understand it.

It sounds like you've made an excellent start.  :-)

> In trying to understand your CAT code, I made some assumptions about
> your formulas by reverse engineering the CAT code with the tests,
> which is kind of my point that it is extremely hard to read CAT. That

I can't argue against that; it _is_ hard.  It helps to have had the 
right kind of training beforehand (my degree was in mathematical logic).

> is kind of why I want to understand the CAT, because for me
> explanation.txt is too much at a higher level to get a proper
> understanding of the memory model.. I tried re-reading explanation.txt
> many times.. then I realized I am just rewriting my own condensed set
> of notes every few months.

Would you like to post a few examples showing some of the most difficult 
points you encountered?  Maybe explanation.txt can be improved.

> > I'm not sure that breaking this relation up into pieces will make it any
> > easier to understand.
> 
> Yes, but I tried. I will keep trying to understand your last patch
> more. Especially I am still not sure, why in the case of an SRCU
> reader on a single CPU, the following does not work:
> let srcu-rscs = ([Srcu-lock]; data; [Srcu-unlock]).

You have to understand that herd7 does not track dependencies through 
stores and subsequent loads.  That is, if you have something like:

	r1 = READ_ONCE(*x);
	WRITE_ONCE(*y, r1);
	r2 = READ_ONCE(*y);
	WRITE_ONCE(*z, r2);

then herd7 will realize that the write to y depends on the value read 
from x, and it will realize that the write to z depends on the value 
read from y.  But it will not realize that the write to z depends on the 
value read from x; it loses track of that dependency because of the 
intervening store/load from y.

More to the point, if you have:

	r1 = srcu_read_lock(lock);
	WRITE_ONCE(*y, r1);
	r2 = READ_ONCE(*y);
	srcu_read_unlock(lock, r2);

then herd7 will not realize that the value of r2 depends on the value of 
r1.  So there will be no data dependency from the srcu_read_lock() to 
the srcu_read_unlock().

Alan