Semantic Patches

Device drivers form the glue code between an operating system and its devices. In Linux, device drivers are highly reliant for this on the various Linux internal libraries, which encapsulate generic functionalities related to the various busses and device types. In recent years, these libraries have been evolving rapidly, to address new requirements and improve performance. In response to each evolution, collateral evolutions are often required in driver code, to bring the drivers up to date with the new library API. Currently, collateral evolutions are mostly done manually. The large number of drivers, however, implies that this approach is time-consuming and unreliable, leading to subtle errors when modifications are not done consistently.

To address this problem, we propose a scripting language for specifying and automating collateral evolutions. This language offers a WYSIWYG approach to program transformation. In the spirit of Linux development practice, this language is based on the patch syntax. As opposed to traditional patches, our patches are not line-oriented but semantics-oriented, and hence we give them the name semantic patches.

This paper gives a tutorial on our semantic patch language, SmPL, and its associated transformation tool, spatch. We first give an idea of the kind of program transformations we target, collateral evolutions, and then present SmPL using an example based on Linux driver code. We then present some further examples of evolutions and collateral evolutions that illustrate other issues in semantic patch development. Finally, we describe the current status of our project and propose some future work. Our work is directed mainly to device driver maintainers, library developers, and kernel janitors, but anyone who has ever performed a repetitive editing task on C code can benefit from it.


Download PDF.