Dynamic Structural Operational Semantics

TL;DR

This paper introduces Dynamic SOS, a formal framework for describing the semantics of programming languages with dynamic software upgrades, emphasizing modularity and formal verification.

Contribution

It extends Modular SOS to handle dynamic software upgrades, providing a formal, modular, and verifiable semantics framework for languages supporting runtime code updates.

Findings

Formal semantics for dynamic software upgrades

Application to Proteus and Creol languages

Encapsulation construction for Modular SOS

Abstract

We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades, for upgrading software code during run-time. Dynamic SOS (DSOS) is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The idea of Dynamic SOS is to bring out the essential differences between dynamic upgrade constructs and program execution constructs. The important feature of Modular SOS (MSOS) that we exploit in DSOS is the sharp separation of the program execution code from the additional (data) structures needed at run-time. In DSOS we aim to achieve the same modularity and decoupling for dynamic software upgrades. This is partly motivated by the long term goal of having machine-checkable proofs for general results like type safety. We exemplify Dynamic SOS on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus. As a side result we define of a general encapsulating construction on Modular SOS useful in situations where a form of encapsulation of the execution is needed. We use encapsulation in the Creol setting of concurrent object-oriented programming with active objects and asynchronous method calls.