The first step is to convert dyntick_nohz() to EXECUTE_MAINLINE() form, as follows:
1 proctype dyntick_nohz()
2 {
3 byte tmp;
4 byte i = 0;
5 bit old_gp_idle;
6
7 do
8 :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
9 :: i < MAX_DYNTICK_LOOP_NOHZ ->
10 EXECUTE_MAINLINE(stmt1,
11 tmp = dynticks_progress_counter)
12 EXECUTE_MAINLINE(stmt2,
13 dynticks_progress_counter = tmp + 1;
14 old_gp_idle = (grace_period_state == GP_IDLE);
15 assert((dynticks_progress_counter & 1) == 1))
16 EXECUTE_MAINLINE(stmt3,
17 tmp = dynticks_progress_counter;
18 assert(!old_gp_idle ||
19 grace_period_state != GP_DONE))
20 EXECUTE_MAINLINE(stmt4,
21 dynticks_progress_counter = tmp + 1;
22 assert((dynticks_progress_counter & 1) == 0))
23 i++;
24 od;
25 dyntick_nohz_done = 1;
26 }
It is important to note that when a group of statements is passed to EXECUTE_MAINLINE(), as in lines 11-14, all statements in that group execute atomically.
Quick Quiz E.14: But what would you do if you needed the statements in a single EXECUTE_MAINLINE() group to execute non-atomically? End Quick Quiz
Quick Quiz E.15: But what if the dynticks_nohz() process had ``if'' or ``do'' statements with conditions, where the statement bodies of these constructs needed to execute non-atomically? End Quick Quiz
The next step is to write a dyntick_irq() process to model an interrupt handler:
1 proctype dyntick_irq()
2 {
3 byte tmp;
4 byte i = 0;
5 bit old_gp_idle;
6
7 do
8 :: i >= MAX_DYNTICK_LOOP_IRQ -> break;
9 :: i < MAX_DYNTICK_LOOP_IRQ ->
10 in_dyntick_irq = 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 in_dyntick_irq = 0;
46 i++;
47 }
48 od;
49 dyntick_irq_done = 1;
50 }
The loop from line 7-48 models up to MAX_DYNTICK_LOOP_IRQ interrupts, with lines 8 and 9 forming the loop condition and line 45 incrementing the control variable. Line 10 tells dyntick_nohz() that an interrupt handler is running, and line 45 tells dyntick_nohz() that this handler has completed. Line 49 is used for liveness verification, much as is the corresponding line of dyntick_nohz().
Quick Quiz E.16: Why are lines 45 and 46 (the in_dyntick_irq = 0; and the i++;) executed atomically? End Quick Quiz
Lines 11-25 model rcu_irq_enter(), and lines 26 and 27 model the relevant snippet of __irq_enter(). Lines 28 and 29 verifies safety in much the same manner as do the corresponding lines of dynticks_nohz(). Lines 30 and 31 model the relevant snippet of __irq_exit(), and finally lines 32-43 model rcu_irq_exit().
Quick Quiz E.17: What property of interrupts is this dynticks_irq() process unable to model? End Quick Quiz
The grace_period process then becomes as follows:
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 shouldexit = 0;
12 snap = dynticks_progress_counter;
13 grace_period_state = GP_WAITING;
14 }
15 do
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 grace_period_state = GP_DONE;
29 grace_period_state = GP_IDLE;
30 atomic {
31 shouldexit = 0;
32 snap = dynticks_progress_counter;
33 grace_period_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 grace_period_state = GP_DONE;
49 }
The implementation of 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 add the new dyntick_irq_done variable to the liveness checks, and of course the optimizations on lines 22 and 42.
This model (dyntickRCU-irqnn-ssl.spin) results in a correct verification with roughly half a million states, passing without errors. However, this version of the model does not handle nested interrupts. This topic is taken up in the nest section.
Paul E. McKenney 2011-12-16