Bounded loops in BPF programs

Fastabend started by noting that the lack of loops hurts; BPF developers are doing "crazy things" to work around their absence. He is working to enable the use of simple loops that can be modeled by the verifier. There is academic work on ways to verify more complex loops, but that is a problem for later. For now, the objective is to detect simple loops and verify that they will terminate; naturally, it's important that the verifier, too, is able to terminate in a reasonable amount of time.

The key to determining the behavior of a loop is to find the induction variable that controls it. For a simple loop like:

    for (i = 0; i < MAX; i++)
	/* loop body */

the induction variable is i. If the variable can be shown to be both monotonically increasing and bounded in value, then the verifier can conclude that the loop will terminate. Once the induction variable and its bounds have been identified, the verifier can also check that any memory references using that variable remain in range.

This kind of verification could be done relatively easily with knowledge of where the loops are. But BPF is an unstructured virtual machine language that doesn't contain information about loops, so the verifier has to figure out where they are itself. This is done by creating a dominator tree that describes the program to be examined; it will identify tests that control the execution of specific blocks of code. From there, it is possible to identify loops (by looking for reverse jumps to the dominator node) and the blocks of code that belong to each loop.

Doing so is not entirely easy. The use of a dominator tree requires that there be a single entry point into every loop; code that jumps into the middle of a loop cannot be verified. Identifying the looped-over code is also an expensive (O(n²)) algorithm.

Fastabend outlined a few approaches to this problem, describing the first as the "by the book" method. This algorithm builds the dominator tree, then works to detect (and abort on) loops that cannot be reduced to a verifiable case. For each loop, it finds the induction variable, and verifies that variable's bounds; the execution of the loop is then simulated with the induction variable's largest and smallest values. The problem here is that the induction variable must be found with pattern matching, and the LLVM optimizer creates a wide variety of patterns that change with every release. That makes the code fragile.

The next approach is to get the compiler to help by limiting the number of loop types that it generates. That makes the pattern-matching task easier, since the patterns that identify loops will be reduced in number and less prone to change. The verifier still has to do all of the work, but it becomes quite a bit more robust.

But the best solution, he said, would be to create a new set of BPF instructions specifically to implement loops. They would mark the beginning and end of each loop, and include the test of the induction variable; the verifier would replace those instructions with actual tests and jumps. With these markers to denote the loop blocks, there would be no need for the dominator tree, since the markers themselves would make it clear which code is controlled by the loop. That would keep the verifier code minimal which, he said, is the right tradeoff in the end.

The description of the session said that the goal "to come to a consensus on how to proceed to make progress on supporting bounded loops". That did not happen, but there was some discussion about the options and the development community is more aware of how this complex work is proceeding. In the end, real consensus is likely to come about in the usual way: through the posting of code that shows how the idea is implemented in the real world.

The slides from this talk [PDF] and a video recording [YouTube] are available. Curious readers can also see the implementation of the first alternative as it was posted in June.

[Thanks to the Linux Foundation, LWN's travel sponsor, for supporting my travel to the event.]