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
Paul E. McKenney 2011-12-16