E.7.2.5 Validating Interrupt Handlers

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