There are a couple of ways to model interrupts in Promela:
A bit of thought indicated that the second approach would have a smaller state space, though it requires that the interrupt handler somehow run atomically with respect to the dynticks_nohz() process, but not with respect to the grace_period() process.
Fortunately, it turns out that Promela permits you to branch out of atomic statements. This trick allows us to have the interrupt handler set a flag, and recode dynticks_nohz() to atomically check this flag and execute only when the flag is not set. This can be accomplished with a C-preprocessor macro that takes a label and a Promela statement as follows:
1 #define EXECUTE_MAINLINE(label, stmt) \ 2 label: skip; \ 3 atomic { \ 4 if \ 5 :: in_dyntick_irq -> goto label; \ 6 :: else -> stmt; \ 7 fi; \ 8 } \
One might use this macro as follows:
EXECUTE_MAINLINE(stmt1, tmp = dynticks_progress_counter) |
Line 2 of the macro creates the specified statement label. Lines 3-8 are an atomic block that tests the in_dyntick_irq variable, and if this variable is set (indicating that the interrupt handler is active), branches out of the atomic block back to the label. Otherwise, line 6 executes the specified statement. The overall effect is that mainline execution stalls any time an interrupt is active, as required.
Paul E. McKenney 2011-12-16