> 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!
Thanks,
Alan
>
>> \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.
>
> Would that help, or am I missing your point?
>
> Thanx, Paul
