E.7.2.6 Validating Nested Interrupt Handlers
Keywords: perfbook_html

###
E.7.2.6 Validating Nested Interrupt Handlers

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.