E.7.2.7 Validating NMI Handlers
Keywords: perfbook_html

###
E.7.2.7 Validating NMI Handlers

We take the same general approach for NMIs as we do for interrupts, keeping in mind that NMIs do not nest. This results in a dyntick_nmi() process as follows:

      1 proctype dyntick_nmi()
      2 {
      3   byte tmp;
      4   byte i = 0;
      5   bit old_gp_idle;
      6
      7   do
      8   :: i >= MAX_DYNTICK_LOOP_NMI -> break;
      9   :: i < MAX_DYNTICK_LOOP_NMI ->
     10     in_dyntick_nmi = 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       i++;
     46       in_dyntick_nmi = 0;
     47     }
     48   od;
     49   dyntick_nmi_done = 1;
     50 }

Of course, the fact that we have NMIs requires adjustments in the other components. For example, the EXECUTE_MAINLINE() macro now needs to pay attention to the NMI handler (in_dyntick_nmi) as well as the interrupt handler (in_dyntick_irq) by checking the dyntick_nmi_done variable as follows:

      1 #define EXECUTE_MAINLINE(label, stmt) \
      2 label: skip; \
      3     atomic { \
      4       if \
      5       :: in_dyntick_irq || \
      6          in_dyntick_nmi -> goto label; \
      7       :: else -> stmt; \
      8       fi; \
      9     } \

We will also need to introduce an EXECUTE_IRQ() macro that checks in_dyntick_nmi in order to allow dyntick_irq() to exclude dyntick_nmi():

      1 #define EXECUTE_IRQ(label, stmt) \
      2 label: skip; \
      3     atomic { \
      4       if \
      5       :: in_dyntick_nmi -> goto label; \
      6       :: else -> stmt; \
      7       fi; \
      8     } \

It is further necessary to convert dyntick_irq() to EXECUTE_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 stmt1: skip;
     18     atomic {
     19       if
     20       :: in_dyntick_nmi -> goto stmt1;
     21       :: !in_dyntick_nmi && rcu_update_flag ->
     22         goto stmt1_then;
     23       :: else -> goto stmt1_else;
     24       fi;
     25     }
     26 stmt1_then: skip;
     27     EXECUTE_IRQ(stmt1_1, tmp = rcu_update_flag)
     28     EXECUTE_IRQ(stmt1_2, rcu_update_flag = tmp + 1)
     29 stmt1_else: skip;
     30 stmt2: skip;  atomic {
     31       if
     32       :: in_dyntick_nmi -> goto stmt2;
     33       :: !in_dyntick_nmi &&
     34          !in_interrupt &&
     35          (dynticks_progress_counter & 1) == 0 ->
     36            goto stmt2_then;
     37       :: else -> goto stmt2_else;
     38       fi;
     39     }
     40 stmt2_then: skip;
     41     EXECUTE_IRQ(stmt2_1, tmp = dynticks_progress_counter)
     42     EXECUTE_IRQ(stmt2_2,
     43       dynticks_progress_counter = tmp + 1)
     44     EXECUTE_IRQ(stmt2_3, tmp = rcu_update_flag)
     45     EXECUTE_IRQ(stmt2_4, rcu_update_flag = tmp + 1)
     46 stmt2_else: skip;
     47     EXECUTE_IRQ(stmt3, tmp = in_interrupt)
     48     EXECUTE_IRQ(stmt4, in_interrupt = tmp + 1)
     49 stmt5: skip;
     50     atomic {
     51       if
     52       :: in_dyntick_nmi -> goto stmt4;
     53       :: !in_dyntick_nmi && outermost ->
     54         old_gp_idle = (grace_period_state == GP_IDLE);
     55       :: else -> skip;
     56       fi;
     57     }
     58     i++;
     59   :: j < i ->
     60 stmt6: skip;
     61     atomic {
     62       if
     63       :: in_dyntick_nmi -> goto stmt6;
     64       :: !in_dyntick_nmi && j + 1 == i ->
     65         assert(!old_gp_idle ||
     66                grace_period_state != GP_DONE);
     67       :: else -> skip;
     68       fi;
     69     }
     70     EXECUTE_IRQ(stmt7, tmp = in_interrupt);
     71     EXECUTE_IRQ(stmt8, in_interrupt = tmp - 1);
     72
     73 stmt9: skip;
     74     atomic {
     75       if
     76       :: in_dyntick_nmi -> goto stmt9;
     77       :: !in_dyntick_nmi && rcu_update_flag != 0 ->
     78         goto stmt9_then;
     79       :: else -> goto stmt9_else;
     80       fi;
     81     }
     82 stmt9_then: skip;
     83     EXECUTE_IRQ(stmt9_1, tmp = rcu_update_flag)
     84     EXECUTE_IRQ(stmt9_2, rcu_update_flag = tmp - 1)
     85 stmt9_3: skip;
     86     atomic {
     87       if
     88       :: in_dyntick_nmi -> goto stmt9_3;
     89       :: !in_dyntick_nmi && rcu_update_flag == 0 ->
     90         goto stmt9_3_then;
     91       :: else -> goto stmt9_3_else;
     92       fi;
     93     }
     94 stmt9_3_then: skip;
     95     EXECUTE_IRQ(stmt9_3_1,
     96       tmp = dynticks_progress_counter)
     97     EXECUTE_IRQ(stmt9_3_2,
     98       dynticks_progress_counter = tmp + 1)
     99 stmt9_3_else:
    100 stmt9_else: skip;
    101     atomic {
    102       j++;
    103       in_dyntick_irq = (i != j);
    104     }
    105   od;
    106   dyntick_irq_done = 1;
    107 }

Note that we have open-coded the ``if'' statements (for example, lines 17-29). In addition, statements that process strictly local state (such as line 58) need not exclude dyntick_nmi().

Finally, grace_period() requires only a few changes:

      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     printf("MDLN = %d\n", MAX_DYNTICK_LOOP_NMI);
     12     shouldexit = 0;
     13     snap = dynticks_progress_counter;
     14     grace_period_state = GP_WAITING;
     15   }
     16   do
     17   :: 1 ->
     18     atomic {
     19       assert(!shouldexit);
     20       shouldexit = dyntick_nohz_done &&
     21              dyntick_irq_done &&
     22              dyntick_nmi_done;
     23       curr = dynticks_progress_counter;
     24       if
     25       :: (curr - snap) >= 2 || (curr & 1) == 0 ->
     26         break;
     27       :: else -> skip;
     28       fi;
     29     }
     30   od;
     31   grace_period_state = GP_DONE;
     32   grace_period_state = GP_IDLE;
     33   atomic {
     34     shouldexit = 0;
     35     snap = dynticks_progress_counter;
     36     grace_period_state = GP_WAITING;
     37   }
     38   do
     39   :: 1 ->
     40     atomic {
     41       assert(!shouldexit);
     42       shouldexit = dyntick_nohz_done &&
     43              dyntick_irq_done &&
     44              dyntick_nmi_done;
     45       curr = dynticks_progress_counter;
     46       if
     47       :: (curr != snap) || ((curr & 1) == 0) ->
     48         break;
     49       :: else -> skip;
     50       fi;
     51     }
     52   od;
     53   grace_period_state = GP_DONE;
     54 }

We have added the printf() for the new MAX_DYNTICK_LOOP_NMI parameter on line 11 and added dyntick_nmi_done to the shouldexit assignments on lines 22 and 44.

The model (`dyntickRCU-irq-nmi-ssl.spin`) results in a correct verification with several hundred million states, passing without errors.

Quick Quiz E.18: Does Paul always write his code in this painfully incremental manner? End Quick Quiz