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 has been used for many years.  Perhaps surprisingly, there is little high-level understanding or language support to help programmers write dynamic updates effectively. 

To bridge this gap, we present Proteus, a core calculus for dynamic software updating in C-like languages that is flexible, safe, and predictable.  Proteus supports dynamic updates to functions (even active ones), to types and to data, 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. This simplifies reasoning and avoids unintuitive copy-based semantics. Finally, Proteus's novel and efficient static updatability analysis allows a programmer to automatically prove that an update is independent of the on-line program state, and thus guarantee that it will succeed at runtime.  Proteus admits a straightforward implementation, and we sketch how it could be extended to more advanced language features including threads. 

Joint work with Gareth Stoyle (Cambridge), Gavin Bierman (MSR Cambridge), Peter Sewell (Cambridge), and Lulian Neamtiu (University of Maryland, College Park).

Principles of Programming Seminars