MIME-Version: 1.0
References: <20230204004843.GA2677518@paulmck-ThinkPad-P17-Gen-1>
 <Y920w4QRLtC6kd+x@rowland.harvard.edu> <20230204014941.GS2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y95yhJgNq8lMXPdF@rowland.harvard.edu> <20230204222411.GC2948950@paulmck-ThinkPad-P17-Gen-1>
 <Y9+41ctA54pjm/KG@google.com> <Y+FJSzUoGTgReLPB@rowland.harvard.edu>
 <Y+fN2fvUjGDWBYrv@google.com> <Y+f4TYZ9BPlt8y8B@rowland.harvard.edu>
In-Reply-To: <Y+f4TYZ9BPlt8y8B@rowland.harvard.edu>
From:   Joel Fernandes <joel@joelfernandes.org>
Date:   Sat, 11 Feb 2023 19:30:32 -0500
Message-ID: <CAEXW_YRuTfjc=5OAskTV0Qt_zSJTPP3-01=Y=SypMdPsF_weAQ@mail.gmail.com>
Subject: Re: Current LKMM patch disposition
To:     Alan Stern <stern@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
Content-Type: text/plain; charset="UTF-8"
Precedence: bulk

On Sat, Feb 11, 2023 at 3:19 PM Alan Stern <stern@rowland.harvard.edu> wrote:
>
> On Sat, Feb 11, 2023 at 05:18:17PM +0000, Joel Fernandes wrote:
>
[..]
> > +
> > +(* Data dependency between lock and idx store *)
> > +let srcu-lock-to-store-idx = ([Srcu-lock]; data)
> > +
> > +(* Data dependency between idx load and unlock *)
> > +let srcu-load-idx-to-unlock = (data; [Srcu-unlock])
> > +
> > +(* Read-from dependency between idx store on one CPU and load on same/another.
> > + * This is required to model the splitting of critical section across CPUs. *)
> > +let srcu-store-to-load-idx = (rf ; srcu-load-idx-to-unlock)
> > +
> > +(* SRCU data dependency flow. Exclude the Srcu-unlock to not transcend back to back rscs *)
> > +let carry-srcu-data = (srcu-lock-to-store-idx ; [~ Srcu-unlock] ; srcu-store-to-load-idx)*
> > +
> > +let srcu-rscs = ([Srcu-lock] ; carry-srcu-data ; [Srcu-unlock]) & loc
>
> That doesn't look right at all.  Does it work with the following?
>
> P0(struct srcu_struct *lock)
> {
>         int r1;
>
>         r1 = srcu_read_lock(lock);
>         srcu_read_unlock(lock, r1);
> }
>
> or
>
> P0(struct srcu_struct *lock, int *x, int *y)
> {
>         *x = srcu_read_lock(lock);
>         *y = *x;
>         srcu_read_unlock(lock, *y);
> }
>
> 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.

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

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
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.

> 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]).

Thanks!

 - Joel