Messages in this thread | | | Date | Sat, 11 Feb 2023 21:59:14 -0500 | From | Alan Stern <> | Subject | Re: Current LKMM patch disposition |
| |
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@rowland.harvard.edu> 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
| |