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
