Nested interrupt handlers may be modeled by splitting the body of the loop in dyntick_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 if
18 :: rcu_update_flag > 0 ->
19 tmp = rcu_update_flag;
20 rcu_update_flag = tmp + 1;
21 :: else -> skip;
22 fi;
23 if
24 :: !in_interrupt &&
25 (dynticks_progress_counter & 1) == 0 ->
26 tmp = dynticks_progress_counter;
27 dynticks_progress_counter = tmp + 1;
28 tmp = rcu_update_flag;
29 rcu_update_flag = tmp + 1;
30 :: else -> skip;
31 fi;
32 tmp = in_interrupt;
33 in_interrupt = tmp + 1;
34 atomic {
35 if
36 :: outermost ->
37 old_gp_idle = (grace_period_state == GP_IDLE);
38 :: else -> skip;
39 fi;
40 }
41 i++;
42 :: j < i ->
43 atomic {
44 if
45 :: j + 1 == i ->
46 assert(!old_gp_idle ||
47 grace_period_state != GP_DONE);
48 :: else -> skip;
49 fi;
50 }
51 tmp = in_interrupt;
52 in_interrupt = tmp - 1;
53 if
54 :: rcu_update_flag != 0 ->
55 tmp = rcu_update_flag;
56 rcu_update_flag = tmp - 1;
57 if
58 :: rcu_update_flag == 0 ->
59 tmp = dynticks_progress_counter;
60 dynticks_progress_counter = tmp + 1;
61 :: else -> skip;
62 fi;
63 :: else -> skip;
64 fi;
65 atomic {
66 j++;
67 in_dyntick_irq = (i != j);
68 }
69 od;
70 dyntick_irq_done = 1;
71 }
This is similar to the earlier dynticks_irq() process. It adds a second counter variable j on line 5, so that i counts entries to interrupt handlers and j counts exits. The outermost variable on line 7 helps determine when the grace_period_state variable needs to be sampled for the safety checks. The loop-exit check on lines 10 and 11 is updated to require that the specified number of interrupt handlers are exited as well as entered, and the increment of i is moved to line 41, which is the end of the interrupt-entry model. Lines 13-16 set the outermost variable to indicate whether this is the outermost of a set of nested interrupts and to set the in_dyntick_irq variable that is used by the dyntick_nohz() process. Lines 34-40 capture the state of the grace_period_state variable, but only when in the outermost interrupt handler.
Line 42 has the do-loop conditional for interrupt-exit modeling: as long as we have exited fewer interrupts than we have entered, it is legal to exit another interrupt. Lines 43-50 check the safety criterion, but only if we are exiting from the outermost interrupt level. Finally, lines 65-68 increment the interrupt-exit count j and, if this is the outermost interrupt level, clears in_dyntick_irq.
This model (dyntickRCU-irq-ssl.spin) results in a correct verification with a bit more than half a million states, passing without errors. However, this version of the model does not handle NMIs, which are taken up in the nest section.
Paul E. McKenney 2011-12-16