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.

[ .pdf ]

@inproceedings{StoyleHBSN05,
  author = {Gareth Stoyle and Michael Hicks and Gavin Bierman and Peter Sewell and Iulian Neamtiu},
  title = {\emph{Mutatis Mutandis}: Safe and Flexible Dynamic Software Updating},
  booktitle = {Proceedings of the {ACM} Conference on Principles of Programming Languages (POPL)},
  pages = {183--194},
  month = {January},
  year = {2005},
  where = {Long Beach, California}
}

This file was generated by bibtex2html 1.99.