E.7.2.5 Validating Interrupt Handlers
Keywords: perfbook_html

###
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.