At the recent Linux Storage, Filesystems, MM, and BPF Summit, Alan Jowett from Microsoft, and a member of the eBPF Steering Committee, presented a discussion on improving LLVM for better verification (video follows below). Here are the key points and insights from his session:
1. Proposal for Enhancements to LLVM
The eBPF Steering Committee has proposed several improvements to LLVM aimed at addressing current verification challenges. These enhancements are intended to make LLVM more robust and user-friendly, particularly for BPF program developers. The goal of this initiative is to inform the community, share existing knowledge, and gather feedback on the proposed changes.
2. Current Verification Challenges
One of the primary issues highlighted is that LLVM optimizations sometimes produce code that the verifier cannot validate, despite being correct. This forces developers to write extensive inline assembly code as a workaround. Such practices are evident in projects like Tetragon, which contain large amounts of inline assembly to address verifier-related issues.
3. Code Coverage in BPF Programs
Jowett emphasized the need for better code coverage tools for BPF programs. Currently, there’s no effective way to determine how well BPF programs are tested, especially as they grow in complexity. He suggested that adding support for code coverage, potentially requiring kernel support or a method to transmit code coverage information from LLVM to profiling tools, would be highly beneficial.
4. Improving Feedback and Optimizations
Jowett proposed several strategies to enhance feedback during the verification process. These include:
- Allowing developers to write explicit assertions in the code, which the verifier could check against.
- Integrating a test verification stage within LLVM’s compilation process to provide immediate feedback on potential verification failures.
- Using hints like ‘likely’ and ‘unlikely’ to optimize code paths more effectively, which could also be useful for the JIT compiler.
5. Abstract Interpretation and Control Flow
He discussed the workings of the Prevail verifier, which several projects, including eBPF for Windows, utilize. The Prevail verifier relies on abstract interpretation, a method for static analysis that creates a control flow graph from BPF programs. However, certain LLVM optimizations, like folding paths to create correlated branches, complicate this process. Potential solutions include providing finer control over LLVM optimizations or leveraging abstract interpretation techniques.
6. Future Directions and Community Feedback
The session concluded with a call for community input on the proposed improvements. Jowett stressed the importance of finding a balance between disabling specific optimizations that hinder verification and maintaining overall code performance. He also highlighted the potential for collaboration on creating a more generic mechanism for code coverage and verification, ensuring consistency across various BPF implementations.