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