Many important applications must run continuously and without interruption, yet must be changed to fix bugs or upgrade functionality. To date, no existing dynamic updating system has achieved a practical balance between flexibility, correctness, ease-of-use, and low overhead.
We present a new approach that provides type-safe dynamic updating of native code in an extremely flexible manner (functions and types may be updated, and at any time) and permits the use of automated tools to aid the programmer in the updating process. Our system is based around dynamic patches made up of proof-carrying code that both contain the updated code and the code needed to transition from the old version to the new. We discuss how patches are generated using a semiautomatic tool, how they are applied using dynamic-linking technology, and how code is compiled to make it updateable.
To concretely illustrate our system, we have implemented a dynamically-updateable web server, FlashEd. We discuss our experience building and maintaining FlashEd. Performance experiments show that updateable FlashEd runs between 2% and 6% slower than a static one.
Host: Karl Crary
Appointments: Margaret Weigand, x82568