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.
> +\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.
> \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
