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