E.7.2 Validating Preemptible RCU and dynticks
Keywords: perfbook_html

##
E.7.2 Validating Preemptible RCU and dynticks

This section develops a Promela model for the interface between dynticks and RCU step by step, with each of the following sections illustrating one step, starting with the process-level code, adding assertions, interrupts, and finally NMIs.

Subsections

- E.7.2.1 Basic Model
- E.7.2.2 Validating Safety
- E.7.2.3 Validating Liveness
- E.7.2.4 Interrupts
- E.7.2.5 Validating Interrupt Handlers
- E.7.2.6 Validating Nested Interrupt Handlers
- E.7.2.7 Validating NMI Handlers