Clear, Correct, and Efficient Dynamic Software Updates

Abstract

Dynamic software updating (DSU) allows programs to be updated as they execute, enabling important changes (e.g., security fixes) to take effect immediately without losing active program state. Most DSU systems aim to add runtime updating support transparently to programs--that is, all updating behavior is orchestrated by the DSU system, while avoiding program code modifications. This philosophy of transparency also extends to existing notions of DSU correctness, which emphasize generic correctness properties that apply to all runtime updates, such as type safety. We claim that runtime updating support should be treated as a program feature, both for implementation and for establishing correctness. For implementing DSU, this means that the core updating behavior is made manifest in the program's code, exposing the programmer to the application-specific details they need to understand, while relying on the DSU system for everything else. We argue that this approach can provide several benefits: simplified developer reasoning about update behavior, modest effort to implement, support for arbitrary program changes, lightweight tool support, and negligible runtime overhead. For establishing correctness, treating updating support as a program feature means that developers should specify and check the specific behaviors that an updated program will exhibit as they do for other program features, rather than relying on overly general notions of correctness. We argue that developers can write DSU specifications with little work--usually by adapting single-version specifications--and check them using standard methods: testing and verification. To support this thesis, we present three pieces of work. First, we describe an empirical study of the techniques used by existing DSU systems to determine when an update can take place. We find that automatic techniques are unable to prevent erroneous behavior and conclude that placing update points in developer-chosen main loops is most effective. Next, we present an approach to specifying and checking the correctness of program features under DSU. We propose a specification strategy that can adapt single-version specifications to describe DSU behavior and a new tool that allows reasoning about DSU specifications using standard checking tools. We have implemented our approach for C, and applied it to updates to the Redis key-value store and several synthetic programs. Finally, we present Kitsune, a new DSU system for C programs, that supports the developer in implementing runtime updating as a program feature. We have used Kitsune to update five popular, open-source, single- and multi-threaded programs, and find that few program changes are required to use Kitsune, and that it incurs essentially no performance overhead.