On Thu, May 18, 2023 at 01:02:21AM +0800, Alan Huang wrote:
> Hi Akira,
>
> > 2023年5月17日 下午10:55，Akira Yokosawa <akiyks@xxxxxxxxx> 写道：
> >
> > Hi Alan,
> >
> > On Tue, 16 May 2023 18:15:31 +0800, Alan Huang wrote:
> >> Hi Akira,
> >>
> >>> 2023年5月16日 下午6:07，Akira Yokosawa <akiyks@xxxxxxxxx> 写道：
> >>>
> >>> Hi Alan,
> >>>
> >>> On Sun, 14 May 2023 14:51:23 +0000, Alan Huang wrote:
> >>>> The third step and the fourth step seem to have no causal relationship between them.
> >>>
> >>> Why do you expect causal relationship between the two?
> >>>
> >>>> 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.
> >>>> +\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.
> >>>> \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.
> >>>
> >>> "Therefore" on item 4 looks to me assumes all of items 1, 2, and 3.
> >>
> >> Yeah, that’s right. My commit message is misleading.
> >>
> >> This patch makes item 3 more specific.
> >
> > I might be too nit-picky, but you are changing the simple statement
> > of observation:
> >
> > The synchronize_qrcu() code forces at least one of the counters
> > to be at least 1 at all times.
> >
> > to a complex sentence of:
> >
> > If the counter corresponding to this reader is 1, then
> > the other counter is at least 1 because of the completion of
> > counter flip.
> >
> > Your wording describes something different from the original one,
> > doesn't it?
> >
> > Can you elaborate what you find hard to follow in this _informal_
> > proof?
>
> Item 4 says:
>
> 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.
>
> “at least 2” is obvious, but it took me some time to figure this out:
>
> "or both of the counters will be at least one”
>
> The original item 3 is not very helpful to me.
>
> But others may prefer the original one :)
I will take a closer look before the end of the weekend. Sorry to be
slow, but a Linux-kernel RCU issue has me by the ankle.
Thanx, Paul
