Title: JITSynth: Synthesizing JIT Compilers for In-Kernel DSLs
Advisors: Emina Torlak and Xi Wang
Abstract: Modern kernels must be powerful, easy to use, fast, and correct. User applications demand all four of these properties so that any user task can be accomplished using relatively simple code with a short execution time. Packet filtering is one facet of the kernel that aims to deliver these four properties to the user. Using packet filtering languages like BPF, user programs can submit filter programs to the kernel, asking the kernel to run the filtering code. The kernel will then check the filter program for illegal memory accesses and unbounded execution before running the filter. Ideally, this mechanism allows users to easily filter packets with an expressive language, relying on the kernel to correctly and efficiently execute filtering code.
Unfortunately, these ideals are rarely achieved in practice. Interpreters and compilers for languages like BPF are difficult to write, and kernel vulnerabilities may be exposed as a result. Previous work has addressed this issue by verifying the correctness of interpreters for languages like BPF. However, the process of interpretation is inherently slow. JIT compilers, on the other hand, achieve high performance by transforming filter programs into assembly programs, then running the generated machine code. The trade-off here is that compilers are often more complex and thus difficult to write correctly by hand.
In order to ensure both correctness and high performance of in-kernel DSLs like BPF, I propose JITSynth, a framework for synthesizing JIT compilers from verified interpreters. By ensuring that the synthesized compiler is equivalent to the verified interpreter, our technique guarantees the correctness of the generated compiler. In addition, due to the inherent performance benefits of JIT compilers, our generated compiler has greatly enhanced performance over the corresponding interpreter. During my talk, I'll describe the main ideas behind JITSynth, as well as discussing some preliminary results and future the project.