E.7 Promela Parable: dynticks and Preemptible RCU
Keywords: perfbook_html

#
E.7 Promela Parable: dynticks and Preemptible RCU

In early 2008, a preemptible variant of RCU was accepted into mainline Linux in support of real-time workloads, a variant similar to the RCU implementations in the -rt patchset [Mol05] since August 2005. Preemptible RCU is needed for real-time workloads because older RCU implementations disable preemption across RCU read-side critical sections, resulting in excessive real-time latencies.

However, one disadvantage of the older -rt implementation (described in Appendix ) was that each grace period requires work to be done on each CPU, even if that CPU is in a low-power ``dynticks-idle'' state, and thus incapable of executing RCU read-side critical sections. The idea behind the dynticks-idle state is that idle CPUs should be physically powered down in order to conserve energy. In short, preemptible RCU can disable a valuable energy-conservation feature of recent Linux kernels. Although Josh Triplett and Paul McKenney had discussed some approaches for allowing CPUs to remain in low-power state throughout an RCU grace period (thus preserving the Linux kernel's ability to conserve energy), matters did not come to a head until Steve Rostedt integrated a new dyntick implementation with preemptible RCU in the -rt patchset.

This combination caused one of Steve's systems to hang on boot, so in October, Paul coded up a dynticks-friendly modification to preemptible RCU's grace-period processing. Steve coded up rcu_irq_enter() and rcu_irq_exit() interfaces called from the irq_enter() and irq_exit() interrupt entry/exit functions. These rcu_irq_enter() and rcu_irq_exit() functions are needed to allow RCU to reliably handle situations where a dynticks-idle CPUs is momentarily powered up for an interrupt handler containing RCU read-side critical sections. With these changes in place, Steve's system booted reliably, but Paul continued inspecting the code periodically on the assumption that we could not possibly have gotten the code right on the first try.

Paul reviewed the code repeatedly from October 2007 to February 2008, and almost always found at least one bug. In one case, Paul even coded and tested a fix before realizing that the bug was illusory, and in fact in all cases, the ``bug'' turned out to be illusory.

Near the end of February, Paul grew tired of this game. He therefore decided to enlist the aid of Promela and spin [Hol03], as described in Appendix . The following presents a series of seven increasingly realistic Promela models, the last of which passes, consuming about 40GB of main memory for the state space.

More important, Promela and Spin did find a very subtle bug for me!

Quick Quiz E.6: Yeah, that's just great! Now, just what am I supposed to do if I don't happen to have a machine with 40GB of main memory??? End Quick Quiz

Still better would be to come up with a simpler and faster algorithm that has a smaller state space. Even better would be an algorithm so simple that its correctness was obvious to the casual observer!

Section gives an overview of preemptible RCU's dynticks interface, Section , and Section lists lessons (re)learned during this effort.

Subsections

- E.7.1 Introduction to Preemptible RCU and dynticks
  - E.7.1.1 Task Interface
  - E.7.1.2 Interrupt Interface
  - E.7.1.3 Grace-Period Interface
- E.7.2 Validating Preemptible RCU and dynticks
  - 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
- E.7.3 Lessons (Re)Learned