> On Feb 11, 2023, at 9:59 PM, Alan Stern <stern@xxxxxxxxxxxxxxxxxxx> wrote: > > 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. Got it. > >> Damn, that's really complicated.. and I still don't fully understand it. > > It sounds like you've made an excellent start. :-) Thanks. :-) > >> 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). Got it, I am reviewing the academic material on these as well. >> 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. Sure, I will share some things I faced difficult with, tomorrow or so. Off the top, cumulativity was certainly pretty hard to parse. > >>> 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(). Got it! Now I understand why the intermediate load stores needs to be modeled with your carry-srcu-data formula, even on the same CPU! Thank you so much Alan!! Thanks, - Joel > > Alan
