THE DISSERTATION DEFENSE FOR THE DEGREE OF Ph.D. IN COMPUTER SCIENCE FOR

                                      Christopher M. Hayden

Dynamic software updating (DSU) allows programs to be updated as they execute, enabling important changes (e.g., security fixes) to take effect immediately without losing active program state.  Most DSU systems aim to add runtime updating support transparently to programs--that is, all updating behavior is orchestrated by the DSU system, while avoiding program code modifications.  This philosophy of transparency also extends to existing notions of DSU correctness, which emphasize generic correctness properties that apply to all runtime updates, such as type safety.

We claim that runtime updating support should be treated as a program feature, both for establishing correctness and for implementation. For establishing correctness, this means that developers should specify and check the specific behaviors that an updated program will exhibit as they do for other program features, rather than relying on overly general notions of correctness.  We argue that developers can write DSU specifications with little work--usually by adapting single-version specifications--and check them using standard methods: testing and verification.  For implementing DSU, treating updating support as a program feature means that the updating behavior is made manifest in the program's code, exposing the programmer to the details they need to understand, while relying on the DSU system for everything else.  We argue that this approach provides several benefits: simplified developer reasoning about update behavior, little developer effort to implement, support for arbitrary program changes, lightweight tool support, and negligible runtime overhead.

To support this thesis, we present three pieces of work. First, we describe an empirical study of the techniques used by existing DSU systems to determine when an update can take place.  We find that automatic techniques are unable to prevent erroneous behavior and conclude that placing update points in developer-chosen main loops is most effective.  Next, we present an approach to specifying and checking the correctness of program features under DSU.  We propose a specification strategy that can adapt single-version specifications to describe DSU behavior and a new tool that allows reasoning about DSU specifications using standard checking tools.  We have implemented our approach for C, and applied it to updates to the Redis key-value store and several synthetic programs.  Finally, we present Kitsune, a new DSU system for C programs, that supports the developer in implementing runtime updating as a program feature.  We have used Kitsune to update five popular, open-source, single- and multi-threaded programs, and find that few program changes are required to use Kitsune, and that it incurs essentially no performance overhead.

Examining Committee:

Committee Chair:                                Dr. Michael Hicks

CO-Chair                                               Dr. Jeffrey S. Foster           

Dean’s Representative:                      Dr. Shuvra Bhattacharyya

Committee Members:                        Dr. Amol Deshpande

                                                                Dr. Peter Keleher

EVERYONE IS INVITED TO ATTEND THE PRESENTATIVE PORTION OF THIS DEFENSE