Mutatis Mutandis: Safe and Flexible Dynamic Software Updating. Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, and Iulian Neamtiu. In Proceedings of the ACM Conference on Principles of Programming Languages (POPL), pages 183-194, January 2005.

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 has been generated by bibtex2html 1.69