Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PretVM: Predictable, Efficient Virtual Machine for Real-Time Concurrency

Shaokai Lin, Erling Jellum, Mirco Theile, Tassilo Tanneberger, Binqi Sun, Chadlia Jerad, Ruomu Xu, Guangyu Feng, Christian Menard, Marten Lohstroh, Jeronimo Castrillon, Sanjit Seshia, Edward Lee

TL;DR

PretVM delivers a predictable, intermediate virtual machine that executes quasi-static schedules derived from a subset of Lingua Franca programs, separating coordination from application logic to enable WCET-based timing analysis. It builds DAG- and SSD-based models of LF programs, converts them into per-worker bytecode through a dedicated virtual instruction set, and runs on a multi-core runtime to achieve time-accurate deterministic concurrency. The key contributions include a two-stage LF-to-static-schedule pipeline, a PretVM instruction set, and an evaluation showing improved timing precision over dynamic LF scheduling on real hardware. This approach significantly improves verifiability and portability of real-time LF implementations in CPS, enabling broader platform support while maintaining rigorous timing guarantees.

Abstract

This paper introduces the Precision-Timed Virtual Machine (PretVM), an intermediate platform facilitating the execution of quasi-static schedules compiled from a subset of programs written in the Lingua Franca (LF) coordination language. The subset consists of those programs that in principle should have statically verifiable and predictable timing behavior. The PretVM provides a schedule with well-defined worst-case timing bounds. The PretVM provides a clean separation between application logic and coordination logic, yielding more analyzable program executions. Experiments compare the PretVM against the default (more dynamic) LF scheduler and show that it delivers time-accurate deterministic execution.

PretVM: Predictable, Efficient Virtual Machine for Real-Time Concurrency

TL;DR

PretVM delivers a predictable, intermediate virtual machine that executes quasi-static schedules derived from a subset of Lingua Franca programs, separating coordination from application logic to enable WCET-based timing analysis. It builds DAG- and SSD-based models of LF programs, converts them into per-worker bytecode through a dedicated virtual instruction set, and runs on a multi-core runtime to achieve time-accurate deterministic concurrency. The key contributions include a two-stage LF-to-static-schedule pipeline, a PretVM instruction set, and an evaluation showing improved timing precision over dynamic LF scheduling on real hardware. This approach significantly improves verifiability and portability of real-time LF implementations in CPS, enabling broader platform support while maintaining rigorous timing guarantees.

Abstract

This paper introduces the Precision-Timed Virtual Machine (PretVM), an intermediate platform facilitating the execution of quasi-static schedules compiled from a subset of programs written in the Lingua Franca (LF) coordination language. The subset consists of those programs that in principle should have statically verifiable and predictable timing behavior. The PretVM provides a schedule with well-defined worst-case timing bounds. The PretVM provides a clean separation between application logic and coordination logic, yielding more analyzable program executions. Experiments compare the PretVM against the default (more dynamic) LF scheduler and show that it delivers time-accurate deterministic execution.
Paper Structure (27 sections, 2 theorems, 8 equations, 6 figures, 2 tables, 1 algorithm)

This paper contains 27 sections, 2 theorems, 8 equations, 6 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Running Example
  3. Reaction Wheel System
  4. Background
  5. Reactor Model and Lingua Franca
  6. Directed Acyclic Graphs (DAGs)
  7. Task Model
  8. Node-level Timing Attributes
  9. DAG Modeling for LF Programs
  10. From LF to Quasi-Static Schedules
  11. State Space Diagrams with Guarded Transitions
  12. Converting SSDs to DAGs
  13. Scheduling by Graph Partitioning
  14. From Quasi-Static Schedules to PretVM
  15. Virtual Instruction Set
  16. ...and 12 more sections

Key Result

Lemma 6.1

The WCET up to a node $n$, denoted recursively as $\bar{w}(n)$, is defined as where $U : \mathcal{V} \rightarrow \mathcal{P}(\mathcal{V})$ maps a DAG node $n$ to a set of its immediately upstream DAG nodes, and if $n$ is the tail node, $U(n)$ excludes virtual nodes from the returned set.

Figures (6)

  • Figure 1: A simple reaction wheel system
  • Figure 2: Methodology overview. Colored boxes are our work. Brown boxes denote external tools we build interface for. Blue and brown boxes are described in Sec. \ref{['sec:lf_to_static_schedules']}. Green boxes are described in Sec. \ref{['sec:static_schedules_to_pretvm']}.
  • Figure 3: Three separate SSDs connected by guarded transitions from the running example. Pending events are not rendered here to save space.
  • Figure 4: DAG generation and partitioned scheduling. The node names are the initial of the reactor name with the reaction number and optionally the invocation count as subscript. For example, $a_{1,1}$ is the first invocation of reaction 1 in . The numbers in the nodes indicated the WCET of each reaction and the nodes above the dashed line are the virtual path.
  • Figure 5: Generated bytecode for the blue worker in Figure \ref{['fig:dag_gen_red']}
  • ...and 1 more figures

Theorems & Definitions (6)

  • Definition 6.1: WCET of a node
  • Lemma 6.1: WCET up to node $n$
  • proof
  • Theorem 6.2: WCET of a DAG task set
  • proof
  • Example 1