Mutatis mutansdis: Safe and predictable dynamic software updating

Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, Iulian Neamtiu

Research output: Contribution to journalConference articlepeer-review

22 Scopus citations


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 named types and to data, allowing on-line evolution to match source-code evolution as we have observed it in practice. We ensure updates are type-safe by checking for a property we call "con-freeness" for updated types t at the point of update. This means that non-updated code will not use t concretely beyond that point (concrete usages are via explicit coercions) and thus t's representation can safely change. We show how con-freeness can be enforced dynamically for a particular program state. We additionally define a novel and efficient static updateability analysis to establish con-freeness statically, and can thus automatically infer program points at which all future (well-formed) updates will be type-safe. We have implemented our analysis for C and tested it on several well-known programs.

Original languageEnglish (US)
Pages (from-to)183-194
Number of pages12
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
StatePublished - 2005
Externally publishedYes
EventPOPL 2005: The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Long Beach, CA, United States
Duration: Jan 12 2005Jan 14 2005

All Science Journal Classification (ASJC) codes

  • Software


  • Capability
  • Dynamic software updating
  • Proteus
  • Type inference
  • Updateability analysis


Dive into the research topics of 'Mutatis mutansdis: Safe and predictable dynamic software updating'. Together they form a unique fingerprint.

Cite this