E.8 Simplicity Avoids Formal Verification
Keywords: perfbook_html

#
E.8 Simplicity Avoids Formal Verification

The complexity of the dynticks interface for preemptible RCU is primarily due to the fact that both irqs and NMIs use the same code path and the same state variables. This leads to the notion of providing separate code paths and variables for irqs and NMIs, as has been done for hierarchical RCU [McK08a] as indirectly suggested by Manfred Spraul [Spr08b].

Subsections

- E.8.1 State Variables for Simplified Dynticks Interface
- E.8.2 Entering and Leaving Dynticks-Idle Mode
- E.8.3 NMIs From Dynticks-Idle Mode
- E.8.4 Interrupts From Dynticks-Idle Mode
- E.8.5 Checking For Dynticks Quiescent States
- E.8.6 Discussion