Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, and Iulian Neamtiu, Mutatis Mutandis: Safe and Predictable Dynamic Software Updating
Dynamic software updates can be used to fix bugs or add features to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating support has been used for many years. However, there is little high-level understanding that would support programmers in writing dynamic updates effectively.
In an effort to bridge this gap, we present a formal calculus called Proteus for modeling dynamic software updating in C-like languages that is flexible, safe, and predictable. Proteus supports dynamic updates to functions (even those that are active) and types, allowing on-line evolution to match source-code evolution as we have observed it in practice. All updates are provably type-safe and *representation-consistent*, meaning that only one version of a given type may exist in the program at any time, simplifying reasoning and avoiding unintuitive copy-based semantics. Finally, Proteus's novel and efficient static *updateability analysis* allows a programmer to automatically prove that an update is independent of the on-line program state, and thus predict it will not fail dynamically. Proteus admits a straightforward implementation, and we sketch how it could be extended to more advanced language features including threads.