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 rigorous 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 dynamically 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.