13-15 November 2018
America/Vancouver timezone

BPF control flow, supporting loops and other patterns

15 Nov 2018, 10:10
Pavillion-Ballroom-C (Sheraton Vancouver Wall Center)


Sheraton Vancouver Wall Center



John Fastabend (Cilium)


Currently, BPF can not support basic loops such as for, while, do/while, etc. Users work around this by forcing the compiler to "unroll" these control flow constructs in the LLVM backend. However, this only works up to a point. Unrolling increases instruction count and complexity on the verifier and further LLVM can not easily unroll all loops. The result is developers end up writing code that is unnatural, iterating until they find a version that LLVM will compile into a form the verifier backend will support.

We developed a verifier extension to detect bounded loops here,


This requires building a DOM tree (computationally expensive) and then matching loop patterns to find loop invariants to verify loops terminate. In this discussion we would like to cover the pros and cons of this approach. As well as discuss another proposal to use explicit control flow instructions to simplify this task.

The goal of this discussion would be to come to a consensus on how to proceed to make progress on supporting bounded loops.

Presentation Materials

Platinum sponsors

Gold sponsors

Silver sponsors

Catchbox sponsor
T-Shirt sponsor
Breakfast sponsor
Your browser is out of date!

Update your browser to view this website correctly. Update my browser now