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.
Thanks,
Alan
>
> What am I missing?
>
> Thanks, Akira
