Formalizing Dynamic Software Updating

Abstract

Dynamic software updating (DSU) enables running programs to be updated with new code and data without interrupting their execution. A number of DSU systems have been designed, but there is still little rig- orous understanding of how to use DSU technology so that updates are safe. As a first step in this direction, we introduce a small update calculus with a precise mathematical semantics. The calculus is formulated as an extension of a typed lambda calculus, and supports updating technology similar to that of the programming language Erlang [2]. Our goal is to provide a simple yet expressive foundation for reasoning about dynam- ically updateable software. In this paper, we present the details of the calculus, give some examples of its expressive power, and discuss how it might be used or extended to guarantee safety properties