Reactive Programming on the Bare Metal: A Formal Model for a Low-Level Reactive Virtual Machine.

Reactive programming has many applications for embedded devices in IoT and other application domains. For these constrained devices it is crucial to bound the overhead of the execution of non-functional concerns such as glitch freedom. Reactive programming languages with static dependency graphs can implement glitch freedom by topologically sorting the dependency graph ahead of time. However, for more traditional reactive programming languages that support a dependency graph that can dynamically change, glitch freedom is typically implemented using a priority queue in which signals are enqueued according to their location in the graph. This is undesirable for embedded devices, as dynamically updating this priority queue has an undesirable, and sometimes unbounded, overhead. In this paper, we present a small-step operational semantics of a virtual machine specialised for running reactive programs that combines static ahead-of-time compilation of reactive programs into topologically sorted dependancy graphs while maintaining support for dynamic modifications to those dependency graphs.