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