Lines 19 and 39 of dyntickRCU-irqnn-ssl.spin is too long. This commit
shortens the lines.
Signed-off-by: SeongJae Park <sj38.park@xxxxxxxxx>
---
formal/dyntickrcu.tex | 68 ++++++++++++++++++++++++++-------------------------
1 file changed, 35 insertions(+), 33 deletions(-)
diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index e31996d..922e556 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1272,46 +1272,48 @@ The \co{grace_period()} process then becomes as follows:
16 :: 1 ->
17 atomic {
18 assert(!shouldexit);
- 19 shouldexit = dyntick_nohz_done && dyntick_irq_done;
- 20 curr = dynticks_progress_counter;
- 21 if
- 22 :: (curr - snap) >= 2 || (curr & 1) == 0 ->
- 23 break;
- 24 :: else -> skip;
- 25 fi;
- 26 }
- 27 od;
- 28 gp_state = GP_DONE;
- 29 gp_state = GP_IDLE;
- 30 atomic {
- 31 shouldexit = 0;
- 32 snap = dynticks_progress_counter;
- 33 gp_state = GP_WAITING;
- 34 }
- 35 do
- 36 :: 1 ->
- 37 atomic {
- 38 assert(!shouldexit);
- 39 shouldexit = dyntick_nohz_done && dyntick_irq_done;
- 40 curr = dynticks_progress_counter;
- 41 if
- 42 :: (curr != snap) || ((curr & 1) == 0) ->
- 43 break;
- 44 :: else -> skip;
- 45 fi;
- 46 }
- 47 od;
- 48 gp_state = GP_DONE;
- 49 }
+ 19 shouldexit = dyntick_nohz_done &&
+ 20 dyntick_irq_done;
+ 21 curr = dynticks_progress_counter;
+ 22 if
+ 23 :: (curr - snap) >= 2 || (curr & 1) == 0 ->
+ 24 break;
+ 25 :: else -> skip;
+ 26 fi;
+ 27 }
+ 28 od;
+ 29 gp_state = GP_DONE;
+ 30 gp_state = GP_IDLE;
+ 31 atomic {
+ 32 shouldexit = 0;
+ 33 snap = dynticks_progress_counter;
+ 34 gp_state = GP_WAITING;
+ 35 }
+ 36 do
+ 37 :: 1 ->
+ 38 atomic {
+ 39 assert(!shouldexit);
+ 40 shouldexit = dyntick_nohz_done &&
+ 41 dyntick_irq_done;
+ 42 curr = dynticks_progress_counter;
+ 43 if
+ 44 :: (curr != snap) || ((curr & 1) == 0) ->
+ 45 break;
+ 46 :: else -> skip;
+ 47 fi;
+ 48 }
+ 49 od;
+ 50 gp_state = GP_DONE;
+ 51 }
\end{verbatim}
}
The implementation of \co{grace_period()} is very similar
to the earlier one.
The only changes are the addition of line~10 to add the new
-interrupt-count parameter, changes to lines~19 and~39 to
+interrupt-count parameter, changes to lines~19-20 and~40-41 to
add the new \co{dyntick_irq_done} variable to the liveness
-checks, and of course the optimizations on lines~22 and~42.
+checks, and of course the optimizations on lines~23 and~44.
This model (\path{dyntickRCU-irqnn-ssl.spin})
results in a correct verification with roughly half a million
--
2.10.0
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
