We take the same general approach for NMIs as we do for interrupts, keeping in mind that NMIs do not nest. This results in a dyntick_nmi() process as follows:
1 proctype dyntick_nmi()
2 {
3 byte tmp;
4 byte i = 0;
5 bit old_gp_idle;
6
7 do
8 :: i >= MAX_DYNTICK_LOOP_NMI -> break;
9 :: i < MAX_DYNTICK_LOOP_NMI ->
10 in_dyntick_nmi = 1;
11 if
12 :: rcu_update_flag > 0 ->
13 tmp = rcu_update_flag;
14 rcu_update_flag = tmp + 1;
15 :: else -> skip;
16 fi;
17 if
18 :: !in_interrupt &&
19 (dynticks_progress_counter & 1) == 0 ->
20 tmp = dynticks_progress_counter;
21 dynticks_progress_counter = tmp + 1;
22 tmp = rcu_update_flag;
23 rcu_update_flag = tmp + 1;
24 :: else -> skip;
25 fi;
26 tmp = in_interrupt;
27 in_interrupt = tmp + 1;
28 old_gp_idle = (grace_period_state == GP_IDLE);
29 assert(!old_gp_idle || grace_period_state != GP_DONE);
30 tmp = in_interrupt;
31 in_interrupt = tmp - 1;
32 if
33 :: rcu_update_flag != 0 ->
34 tmp = rcu_update_flag;
35 rcu_update_flag = tmp - 1;
36 if
37 :: rcu_update_flag == 0 ->
38 tmp = dynticks_progress_counter;
39 dynticks_progress_counter = tmp + 1;
40 :: else -> skip;
41 fi;
42 :: else -> skip;
43 fi;
44 atomic {
45 i++;
46 in_dyntick_nmi = 0;
47 }
48 od;
49 dyntick_nmi_done = 1;
50 }
Of course, the fact that we have NMIs requires adjustments in the other components. For example, the EXECUTE_MAINLINE() macro now needs to pay attention to the NMI handler (in_dyntick_nmi) as well as the interrupt handler (in_dyntick_irq) by checking the dyntick_nmi_done variable as follows:
1 #define EXECUTE_MAINLINE(label, stmt) \
2 label: skip; \
3 atomic { \
4 if \
5 :: in_dyntick_irq || \
6 in_dyntick_nmi -> goto label; \
7 :: else -> stmt; \
8 fi; \
9 } \
We will also need to introduce an EXECUTE_IRQ() macro that checks in_dyntick_nmi in order to allow dyntick_irq() to exclude dyntick_nmi():
1 #define EXECUTE_IRQ(label, stmt) \
2 label: skip; \
3 atomic { \
4 if \
5 :: in_dyntick_nmi -> goto label; \
6 :: else -> stmt; \
7 fi; \
8 } \
It is further necessary to convert dyntick_irq() to EXECUTE_IRQ() as follows:
1 proctype dyntick_irq()
2 {
3 byte tmp;
4 byte i = 0;
5 byte j = 0;
6 bit old_gp_idle;
7 bit outermost;
8
9 do
10 :: i >= MAX_DYNTICK_LOOP_IRQ &&
11 j >= MAX_DYNTICK_LOOP_IRQ -> break;
12 :: i < MAX_DYNTICK_LOOP_IRQ ->
13 atomic {
14 outermost = (in_dyntick_irq == 0);
15 in_dyntick_irq = 1;
16 }
17 stmt1: skip;
18 atomic {
19 if
20 :: in_dyntick_nmi -> goto stmt1;
21 :: !in_dyntick_nmi && rcu_update_flag ->
22 goto stmt1_then;
23 :: else -> goto stmt1_else;
24 fi;
25 }
26 stmt1_then: skip;
27 EXECUTE_IRQ(stmt1_1, tmp = rcu_update_flag)
28 EXECUTE_IRQ(stmt1_2, rcu_update_flag = tmp + 1)
29 stmt1_else: skip;
30 stmt2: skip; atomic {
31 if
32 :: in_dyntick_nmi -> goto stmt2;
33 :: !in_dyntick_nmi &&
34 !in_interrupt &&
35 (dynticks_progress_counter & 1) == 0 ->
36 goto stmt2_then;
37 :: else -> goto stmt2_else;
38 fi;
39 }
40 stmt2_then: skip;
41 EXECUTE_IRQ(stmt2_1, tmp = dynticks_progress_counter)
42 EXECUTE_IRQ(stmt2_2,
43 dynticks_progress_counter = tmp + 1)
44 EXECUTE_IRQ(stmt2_3, tmp = rcu_update_flag)
45 EXECUTE_IRQ(stmt2_4, rcu_update_flag = tmp + 1)
46 stmt2_else: skip;
47 EXECUTE_IRQ(stmt3, tmp = in_interrupt)
48 EXECUTE_IRQ(stmt4, in_interrupt = tmp + 1)
49 stmt5: skip;
50 atomic {
51 if
52 :: in_dyntick_nmi -> goto stmt4;
53 :: !in_dyntick_nmi && outermost ->
54 old_gp_idle = (grace_period_state == GP_IDLE);
55 :: else -> skip;
56 fi;
57 }
58 i++;
59 :: j < i ->
60 stmt6: skip;
61 atomic {
62 if
63 :: in_dyntick_nmi -> goto stmt6;
64 :: !in_dyntick_nmi && j + 1 == i ->
65 assert(!old_gp_idle ||
66 grace_period_state != GP_DONE);
67 :: else -> skip;
68 fi;
69 }
70 EXECUTE_IRQ(stmt7, tmp = in_interrupt);
71 EXECUTE_IRQ(stmt8, in_interrupt = tmp - 1);
72
73 stmt9: skip;
74 atomic {
75 if
76 :: in_dyntick_nmi -> goto stmt9;
77 :: !in_dyntick_nmi && rcu_update_flag != 0 ->
78 goto stmt9_then;
79 :: else -> goto stmt9_else;
80 fi;
81 }
82 stmt9_then: skip;
83 EXECUTE_IRQ(stmt9_1, tmp = rcu_update_flag)
84 EXECUTE_IRQ(stmt9_2, rcu_update_flag = tmp - 1)
85 stmt9_3: skip;
86 atomic {
87 if
88 :: in_dyntick_nmi -> goto stmt9_3;
89 :: !in_dyntick_nmi && rcu_update_flag == 0 ->
90 goto stmt9_3_then;
91 :: else -> goto stmt9_3_else;
92 fi;
93 }
94 stmt9_3_then: skip;
95 EXECUTE_IRQ(stmt9_3_1,
96 tmp = dynticks_progress_counter)
97 EXECUTE_IRQ(stmt9_3_2,
98 dynticks_progress_counter = tmp + 1)
99 stmt9_3_else:
100 stmt9_else: skip;
101 atomic {
102 j++;
103 in_dyntick_irq = (i != j);
104 }
105 od;
106 dyntick_irq_done = 1;
107 }
Note that we have open-coded the ``if'' statements (for example, lines 17-29). In addition, statements that process strictly local state (such as line 58) need not exclude dyntick_nmi().
Finally, grace_period() requires only a few changes:
1 proctype grace_period()
2 {
3 byte curr;
4 byte snap;
5 bit shouldexit;
6
7 grace_period_state = GP_IDLE;
8 atomic {
9 printf("MDLN = %d\n", MAX_DYNTICK_LOOP_NOHZ);
10 printf("MDLI = %d\n", MAX_DYNTICK_LOOP_IRQ);
11 printf("MDLN = %d\n", MAX_DYNTICK_LOOP_NMI);
12 shouldexit = 0;
13 snap = dynticks_progress_counter;
14 grace_period_state = GP_WAITING;
15 }
16 do
17 :: 1 ->
18 atomic {
19 assert(!shouldexit);
20 shouldexit = dyntick_nohz_done &&
21 dyntick_irq_done &&
22 dyntick_nmi_done;
23 curr = dynticks_progress_counter;
24 if
25 :: (curr - snap) >= 2 || (curr & 1) == 0 ->
26 break;
27 :: else -> skip;
28 fi;
29 }
30 od;
31 grace_period_state = GP_DONE;
32 grace_period_state = GP_IDLE;
33 atomic {
34 shouldexit = 0;
35 snap = dynticks_progress_counter;
36 grace_period_state = GP_WAITING;
37 }
38 do
39 :: 1 ->
40 atomic {
41 assert(!shouldexit);
42 shouldexit = dyntick_nohz_done &&
43 dyntick_irq_done &&
44 dyntick_nmi_done;
45 curr = dynticks_progress_counter;
46 if
47 :: (curr != snap) || ((curr & 1) == 0) ->
48 break;
49 :: else -> skip;
50 fi;
51 }
52 od;
53 grace_period_state = GP_DONE;
54 }
We have added the printf() for the new MAX_DYNTICK_LOOP_NMI parameter on line 11 and added dyntick_nmi_done to the shouldexit assignments on lines 22 and 44.
The model (dyntickRCU-irq-nmi-ssl.spin) results in a correct verification with several hundred million states, passing without errors.
Quick Quiz E.18: Does Paul always write his code in this painfully incremental manner? End Quick Quiz
Paul E. McKenney 2011-12-16