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