On Sun, May 21, 2023 at 07:35:56PM +0800, Alan Huang wrote:
>
> > 2023年5月21日 18:20，Paul E. McKenney <paulmck@xxxxxxxxxx> 写道：
> >
> > On Sun, May 14, 2023 at 02:51:23PM +0000, Alan Huang wrote:
> >> The third step and the fourth step seem to have no causal relationship between them.
> >> Therefore, this patch explains under what circumstances both counters will be at least 1.
> >>
> >> Signed-off-by: Alan Huang <mmpgouride@xxxxxxxxx>
> >> ---
> >> formal/spinhint.tex | 5 +++--
> >> 1 file changed, 3 insertions(+), 2 deletions(-)
> >>
> >> diff --git a/formal/spinhint.tex b/formal/spinhint.tex
> >> index 16764aef..dd2e88cc 100644
> >> --- a/formal/spinhint.tex
> >> +++ b/formal/spinhint.tex
> >> @@ -1103,8 +1103,9 @@ follows:
> >> execution.
> >> \item The counter corresponding to this reader will have been
> >> at least 1 during this time interval.
> >> -\item The \co{synchronize_qrcu()} code forces at least one
> >> - of the counters to be at least 1 at all times.
> >
> > So this part is true and fundamental to understanding the code. You can
> > see this on lines 31-33 of Listing 12.14 ("QRCU Updater Process").
> > This code increments the next counter before decrementing the previous
> > counter. I therefore don't see how we can reasonably delete this item.
>
> Yes, this item is completely correct.
>
> >
> >> +\item If the counter corresponding to this reader is 1, then
> >> + the other counter is at least 1 because of the completion of
> >> + counter flip.
> >
> > However, we could potentially add this as an intermediate consequence
> > of items 2 and 3. Maybe something like this?
> >
> > \item The above two items imply that if the counter corresponding
> > to this reader is exactly one, then the other counter must be
> > greater than or equal to one. Similarly, if the other counter
> > is equal to zero, then the counter corresponding to the
> > reader must be greater than or equal to two.
>
> That will be very helpful, adding an item will be better than deleting one!
Very good, thank you! I have added the following, with your
Reported-by.
Thanx, Paul
------------------------------------------------------------------------
commit cbef7a09aa845ca2eded65a124970c6508d4b2b2
Author: Paul E. McKenney <paulmck@xxxxxxxxxx>
Date: Sat May 27 03:35:55 2023 -0700
spinhint: Add clarifying step to QRCU by-hand proof
Reported-by: Alan Huang <mmpgouride@xxxxxxxxx>
Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 16764aef..9e68198e 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -1105,6 +1105,11 @@ follows:
at least 1 during this time interval.
\item The \co{synchronize_qrcu()} code forces at least one
of the counters to be at least 1 at all times.
+\item The above two items imply that if the counter corresponding
+ to this reader is exactly one, then the other counter must be
+ greater than or equal to one.
+ Similarly, if the other counter is equal to zero, then the counter
+ corresponding to the reader must be greater than or equal to two.
\item Therefore, at any given point in time, either one of the
counters will be at least 2, or both of the counters will
be at least one.
