Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
From:   Joel Fernandes <joel@joelfernandes.org>
Mime-Version: 1.0 (1.0)
Subject: Re: Current LKMM patch disposition
Date:   Sat, 11 Feb 2023 22:35:44 -0500
Message-Id: <478E76E6-8DA4-4F55-B789-8D8DE0FE6621@joelfernandes.org>
References: <Y+hWAksfk4C0M2gB@rowland.harvard.edu>
Cc:     "Paul E. McKenney" <paulmck@kernel.org>,
        linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
        kernel-team@meta.com, mingo@kernel.org, parri.andrea@gmail.com,
        will@kernel.org, peterz@infradead.org, boqun.feng@gmail.com,
        npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk,
        luc.maranget@inria.fr, akiyks@gmail.com
In-Reply-To: <Y+hWAksfk4C0M2gB@rowland.harvard.edu>
To:     Alan Stern <stern@rowland.harvard.edu>
Precedence: bulk


> On Feb 11, 2023, at 9:59 PM, Alan Stern <stern@rowland.harvard.edu> wrote:=

>=20
> =EF=BB=BFOn 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> w=
rote:
>>> 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.
>>=20
>> 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.
>=20
> In which case the sequence has length 0.  Exactly right.

Got it.

>=20
>> Damn, that's really complicated.. and I still don't fully understand it.
>=20
> It sounds like you've made an excellent start.  :-)

Thanks. :-)

>=20
>> 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
>=20
> I can't argue against that; it _is_ hard.  It helps to have had the=20
> 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.
>=20
> Would you like to post a few examples showing some of the most difficult=20=

> points you encountered?  Maybe explanation.txt can be improved.

Sure, I will share some things I faced difficult with, tomorrow or so. Off t=
he top, cumulativity was certainly pretty hard to parse.

>=20
>>> I'm not sure that breaking this relation up into pieces will make it any=

>>> easier to understand.
>>=20
>> 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 =3D ([Srcu-lock]; data; [Srcu-unlock]).
>=20
> You have to understand that herd7 does not track dependencies through=20
> stores and subsequent loads.  That is, if you have something like:
>=20
>    r1 =3D READ_ONCE(*x);
>    WRITE_ONCE(*y, r1);
>    r2 =3D READ_ONCE(*y);
>    WRITE_ONCE(*z, r2);
>=20
> then herd7 will realize that the write to y depends on the value read=20
> from x, and it will realize that the write to z depends on the value=20
> read from y.  But it will not realize that the write to z depends on the=20=

> value read from x; it loses track of that dependency because of the=20
> intervening store/load from y.
>=20
> More to the point, if you have:
>=20
>    r1 =3D srcu_read_lock(lock);
>    WRITE_ONCE(*y, r1);
>    r2 =3D READ_ONCE(*y);
>    srcu_read_unlock(lock, r2);
>=20
> then herd7 will not realize that the value of r2 depends on the value of=20=

> r1.  So there will be no data dependency from the srcu_read_lock() to=20
> the srcu_read_unlock().

Got it!  Now I understand why the intermediate load stores needs to be model=
ed with your carry-srcu-data formula, even on the same CPU! Thank you so muc=
h Alan!!

Thanks,

 - Joel

>=20
> Alan