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