E.7.2.4 Interrupts
Keywords: perfbook_html

###
E.7.2.4 Interrupts

There are a couple of ways to model interrupts in Promela:

1. using C-preprocessor tricks to insert the interrupt handler between each and every statement of the dynticks_nohz() process, or
2. modeling the interrupt handler with a separate process.

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.