Dynamic software update for message passing programs

Abstract

Global Session Types are typically used to express communication protocols between a number of participating entities. Analyses on these types can be used to prove that message passing programs have a variety of desirable properties such as communications safety and deadlock freedom. In this paper we provide a Global Session Type analysis for queued channel message passing programs whose code may be updated during runtime (Dynamic Software Update). In particular, we prove safety and liveness properties for well-typed programs by identifying suitable restrictions on the runtime points at which dynamic updates may occur. This includes the possibility of updating several threads without requiring global thread synchronisation. © Springer-Verlag Berlin Heidelberg 2012.