arXiv subjects

Edward A. Lee

Publications and source records attributed to Edward A. Lee.

At least 19 recordsLinked to original sources

arXiv2026

Deterministic Execution of ROS 2 Applications via Lingua Franca

The Robot Operating System 2 (ROS 2) is a widely used middleware for robotic systems, characterized by a publish-subscribe (pub-sub) communication mechanism in which computation is structured as callbacks dispatched by ROS 2 executors. Despite its popularity, the pub-sub pattern in ROS 2 is inherently nondeterministic: the order in which these callbacks run is nondeterministic even within a single executor, and distributed deployments add further nondeterminism from the interleaving of messages across nodes and from network latency. Such nondeterminism often leads to concurrency issues and makes it virtually impossible to analyze for safeness and provide guarantees. We present a framework that is able to convert an unmodified ROS 2 application and run it under Lingua Franca (LF), a coordination language for deterministic execution using logical time, so that the same input always produces the same deterministic execution order. We first describe which ROS 2 features can be executed deterministically under logical time. Such features enable the possibility to establish an automatic conversion framework to extract information from a ROS 2 application and directly convert it into an LF program. The rich features of LF, such as logical-time delays, federated execution across processes, and fault handling, can then be applied to make the ROS 2 application be executed in a deterministic and timing-predictable manner without changing the ROS 2 code. We evaluate the framework on a synthetic example and on the Autoware reference system. We show that the order in which callbacks are executed differs in default ROS 2, while also having end-to-end latencies that vary across executions. In contrast, our LF-controlled ROS 2 system produces a deterministic execution order and consistent end-to-end latencies.

cs.RO↗

arXiv2026

Maxwait: A Generalized Mechanism for Distributed Time-Sensitive Systems

Distributed time-sensitive systems must balance timing requirements (availability) and consistency in the presence of communication delays and synchronization uncertainty. This paper presents maxwait, a simple coordination mechanism with surprising generality that makes these tradeoffs explicit and configurable. We demonstrate that this mechanism subsumes classical distributed system methods such as PTIDES, Chandy-and-Misra with or without null messages, Jefferson's Time-Warp, and Lamport's time-based fault detection, while enabling real-time behavior in distributed cyber-physical applications. The mechanism can also realize many commonly used distributed system patterns, including logical execution time (LET), publish and subscribe, actors, conflict-free replicated data types (CRDTs), and remote procedure calls with futures. More importantly, it adds to these mechanisms better control over timing, bounded time fault detection, and the option of making them more deterministic, all within a single semantic framework. Implemented as an extension of the Lingua Franca coordination language, maxwait enforces logical-time consistency when communication latencies are bounded and provides structured fault handling when bounds are violated.

cs.DC↗

arXiv2025

It's Not the AI - It's Each of Us! Ten Commandments for the Wise & Responsible Use of AI

Artificial intelligence (AI) is no longer futuristic; it is a daily companion shaping our private and work lives. While AI simplifies our lives, its rise also invites us to rethink who we are - and who we wish to remain - as humans. Even if AI does not think, feel, or desire, it learns from our behavior, mirroring our collective values, biases, and aspirations. The question, then, is not what AI is, but what we are allowing it to become through data, computing power, and other parameters "teaching" it - and, even more importantly, who we are becoming through our relationship with AI. As the EU AI Act and the Vienna Manifesto on Digital Humanism emphasize, technology must serve human dignity,social well-being, and democratic accountability. In our opinion, responsible use of AI is not only a matter of code nor law, but also of conscientious practice: how each of us engages and teaches others to use AI at home and at work. We propose Ten Commandments for the Wise and Responsible Use of AI are meant as guideline for this very engagement. They closely align with Floridi and Cowls' five guiding principles for AI in society - beneficence, non-maleficence, autonomy, justice, and explicability.

cs.CY↗

arXiv2025

PolyVer: A Compositional Approach for Polyglot System Modeling and Verification

Several software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Verifiers that directly run on mainstream programming languages are currently customized for single languages. Thus, to verify polyglot systems, one usually translates them into a common verification language or formalism on which the verifier runs. In this paper, we present an alternative approach, PolyVer, which employs abstraction, compositional reasoning, and synthesis to directly perform polyglot verification. PolyVer constructs a formal model of the original polyglot system as a transition system where the update functions associated with transitions are implemented in target languages such as C or Rust. To perform verification, PolyVer then connects a model checker for transition systems with language-specific verifiers (e.g., for C or Rust) using pre/post-condition contracts for the update functions. These contracts are automatically generated by synthesis oracles based on syntax-guided synthesis or large language models (LLMs), and checked by the language-specific verifiers. The contracts form abstractions of the update functions using which the model checker verifies the overall system-level property on the polyglot system model. PolyVer iterates between counterexample-guided abstraction-refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS) until the property is verified or a true system-level counterexample is found. We demonstrate the utility of PolyVer for verifying programs in the Lingua Franca polyglot language using the UCLID5 model checker connected with the CBMC and Kani verifiers for C and Rust respectively.

cs.PL↗

arXiv2025

AI-Assisted Modeling: DSL-Driven AI Interactions

AI-assisted programming greatly increases software development performance. We enhance this potential by integrating transparency through domain-specific modeling techniques and providing instantaneous, graphical visualizations that accurately represent the semantics of AI-generated code. This approach facilitates visual inspection and formal verification, such as model checking. Formal models can be developed using programming, natural language prompts, voice commands, and stage-wise refinement, with immediate feedback after each transformation step. This support can be tailored to specific domains or intended purposes, improving both code generation and subsequent validation processes. To demonstrate the effectiveness of this approach, we have developed a prototype as a Visual Studio Code extension for the Lingua Franca language. This prototype showcases the potential for novel domain-specific modeling practices, offering an advancement in how models are created, visualized, and verified.

cs.PL↗

arXiv2025

Exploration of Approaches for Robustness and Safety in a Low Code Open Environment for Factory Automation

This report is a compilation of technical knowledge and concepts that were produced by the authors and additional contributors in the context of the collaboration projects "Abstraction Requirements for Language of Choice in Industrial Automation" (FY21-22) and "Approaches for Robust and Safe Low-Code" (FY23-24) from Siemens Technology and the University of California, Berkeley. The primary objective of these projects was to assess Siemens Open Industrial Edge (OIE) engineering capabilities by defining a concept that ensures the satisfaction of coordination and safety requirements when using disparate OIE modules. The objective was to use the Lingua Franca (LF) coordination language to demonstrate how to address challenges in: 1. engineering modular, distributed, and flexible automation solutions that ensure, by design, robust and safe operation1; 2. the use of IEC 61499, the event driven execution model for specifying the execution order of OIE modules (defined as function blocks); 3. support large-scale distributed OIE automation solutions, and eventually 4. define optimal solutions with synchronization and time-optimal mechanisms.

cs.SE↗

arXiv2025

A Preliminary Model of Coordination-free Consistency

Building consistent distributed systems has largely depended on complex coordination strategies that are not only tricky to implement, but also take a toll on performance as they require nodes to wait for coordination messages. In this paper, we explore the conditions under which no coordination is required to guarantee consistency. We present a simple and succinct theoretical model for distributed computation that separates coordination from computation. The main contribution of this work is mathematically defining concepts in distributed computing such as strong eventual consistency, consistency, consistent under partition, confluence, coordination-free, and monotonicity. Based on these definitions, we prove necessary and sufficient conditions for strong eventual consistency and give a proof of the CALM theorem from a distributed computation perspective.

cs.DC↗

arXiv2024

HPRM: High-Performance Robotic Middleware for Intelligent Autonomous Systems

The rise of intelligent autonomous systems, especially in robotics and autonomous agents, has created a critical need for robust communication middleware that can ensure real-time processing of extensive sensor data. Current robotics middleware like Robot Operating System (ROS) 2 faces challenges with nondeterminism and high communication latency when dealing with large data across multiple subscribers on a multi-core compute platform. To address these issues, we present High-Performance Robotic Middleware (HPRM), built on top of the deterministic coordination language Lingua Franca (LF). HPRM employs optimizations including an in-memory object store for efficient zero-copy transfer of large payloads, adaptive serialization to minimize serialization overhead, and an eager protocol with real-time sockets to reduce handshake latency. Benchmarks show HPRM achieves up to 173x lower latency than ROS2 when broadcasting large messages to multiple nodes. We then demonstrate the benefits of HPRM by integrating it with the CARLA simulator and running reinforcement learning agents along with object detection workloads. In the CARLA autonomous driving application, HPRM attains 91.1% lower latency than ROS2. The deterministic coordination semantics of HPRM, combined with its optimized IPC mechanisms, enable efficient and predictable real-time communication for intelligent autonomous systems.

cs.RO↗

arXiv2024

Efficient Coordination for Distributed Discrete-Event Systems

Timing control while preserving determinism is often a key requirement for ensuring the safety and correctness of distributed cyber-physical systems (CPS). Discrete-event (DE) systems provide a suitable model of computation (MoC) for time-sensitive distributed CPS. The high-level architecture (HLA) is a useful tool for the distributed simulation of DE systems, but its techniques can be adapted for implementing distributed CPS. However, HLA incurs considerable overhead in network messages conveying timing information between the distributed nodes and the centralized run-time infrastructure (RTI). This paper gives a novel approach and implementation that reduces such network messages while preserving DE semantics. An evaluation of our runtime demonstrates that our approach significantly reduces the volume of messages for timing information in HLA.

cs.DC↗

arXiv2024

Strongly-Consistent Distributed Discrete-event Systems

Discrete-event (DE) systems are concurrent programs where components communicate via tagged events, where tags are drawn from a totally ordered set. Reactors are an emerging model of computation based on DE and realized in the open-source coordination language Lingua Franca. Distributed DE (DDE) systems are DE systems where the components (reactors) communicate over networks. The prior art has required that for DDE systems with cycles, each cycle must contain at least one logical delay, where the tag of events is incremented. Such delays, however, are not required by the elegant fixed-point semantics of DE. The only requirement is that the program be constructive, meaning it is free of causality cycles. This paper gives a way to coordinate the execution of DDE systems that can execute any constructive program, even one with zero-delay cycles. It provides a formal model that exposes exactly the information that must be shared across networks for such execution to be possible. Furthermore, it describes a concrete implementation that is an extension of the coordination mechanisms in Lingua Franca.

cs.DC↗

arXiv2024

Efficient Parallel Reinforcement Learning Framework using the Reactor Model

Parallel Reinforcement Learning (RL) frameworks are essential for mapping RL workloads to multiple computational resources, allowing for faster generation of samples, estimation of values, and policy improvement. These computational paradigms require a seamless integration of training, serving, and simulation workloads. Existing frameworks, such as Ray, are not managing this orchestration efficiently, especially in RL tasks that demand intensive input/output and synchronization between actors on a single node. In this study, we have proposed a solution implementing the reactor model, which enforces a set of actors to have a fixed communication pattern. This allows the scheduler to eliminate work needed for synchronization, such as acquiring and releasing locks for each actor or sending and processing coordination-related messages. Our framework, Lingua Franca (LF), a coordination language based on the reactor model, also supports true parallelism in Python and provides a unified interface that allows users to automatically generate dataflow graphs for RL tasks. In comparison to Ray on a single-node multi-core compute platform, LF achieves 1.21x and 11.62x higher simulation throughput in OpenAI Gym and Atari environments, reduces the average training time of synchronized parallel Q-learning by 31.2%, and accelerates multi-agent RL inference by 5.12x.

cs.DC↗

arXiv2024

Behavior Trees with Dataflow: Coordinating Reactive Tasks in Lingua Franca

Behavior Trees (BTs) provide a lean set of control flow elements that are easily composable in a modular tree structure. They are well established for modeling the high-level behavior of non-player characters in computer games and recently gained popularity in other areas such as industrial automation. While BTs nicely express control, data handling aspects so far must be provided separately, e. g. in the form of blackboards. This may hamper reusability and can be a source of nondeterminism. We here present a dataflow extension to BTs that explicitly models data relations and communication. We provide a combined textual/graphical approach in line with modern, productivity-enhancing pragmatics-aware modeling techniques. We realized and validated that approach in the recently introduced polyglot coordination language Lingua Franca (LF).

cs.PL↗

arXiv2023

Modal Reactors

Complex software systems often feature distinct modes of operation, each designed to handle a particular scenario that may require the system to respond in a certain way. Breaking down system behavior into mutually exclusive modes and discrete transitions between modes is a commonly used strategy to reduce implementation complexity and promote code readability. However, such capabilities often come in the form of self-contained domain specific languages or language-specific frameworks. The work in this paper aims to bring the advantages of modal models to mainstream programming languages, by following the polyglot coordination approach of Lingua Franca (LF), in which verbatim target code (e.g., C, C++, Python, Typescript, or Rust) is encapsulated in composable reactive components called reactors. Reactors can form a dataflow network, are triggered by timed as well as sporadic events, execute concurrently, and can be distributed across nodes on a network. With modal models in LF, we introduce a lean extension to the concept of reactors that enables the coordination of reactive tasks based on modes of operation. The implementation of modal reactors outlined in this paper generalizes to any LF-supported language with only modest modifications to the generic runtime system.

cs.PL↗

arXiv2023

Consistency vs. Availability in Distributed Real-Time Systems

In distributed applications, Brewer's CAP theorem tells us that when networks become partitioned (P), one must give up either consistency (C) or availability (A). Consistency is agreement on the values of shared variables; availability is the ability to respond to reads and writes accessing those shared variables. Availability is a real-time property whereas consistency is a logical property. We have extended the CAP theorem to relate quantitative measures of these two properties to quantitative measures of communication and computation latency (L), obtaining a relation called the CAL theorem that is linear in a max-plus algebra. This paper shows how to use the CAL theorem in various ways to help design real-time systems. We develop a methodology for systematically trading off availability and consistency in application-specific ways and to guide the system designer when putting functionality in end devices, in edge computers, or in the cloud. We build on the Lingua Franca coordination language to provide system designers with concrete analysis and design tools to make the required tradeoffs in deployable software.

cs.DC↗

arXiv2023

High-Performance Deterministic Concurrency using Lingua Franca

Actor frameworks and similar reactive programming techniques are widely used for building concurrent systems. They promise to be efficient and scale well to a large number of cores or nodes in a distributed system. However, they also expose programmers to nondeterminism, which often makes implementations hard to understand, debug, and test. The recently proposed reactor model is a promising alternative that enables efficient deterministic concurrency. In this paper, we show that determinacy does neither imply a loss in expressivity nor in performance. To show this, we evaluate Lingua Franca (LF), a reactor-oriented coordination language that equips mainstream programming languages with a concurrency model that automatically takes advantage of opportunities to exploit parallelism that do not introduce nondeterminism. Our implementation of the Savina benchmark suite demonstrates that, in terms of execution time, the runtime performance of LF programs even exceeds popular and highly optimized actor frameworks. We compare against Akka and CAF, which LF outperforms by 1.86x and 1.42x, respectively.

cs.PL↗

arXiv2022

Xronos: Predictable Coordination for Safety-Critical Distributed Embedded Systems

Asynchronous frameworks for distributed embedded systems, like ROS and MQTT, are increasingly used in safety-critical applications such as autonomous driving, where the cost of unintended behavior is high. The coordination mechanism between the components in these frameworks, however, gives rise to nondeterminism, where factors such as communication timing can lead to arbitrary ordering in the handling of messages. In this paper, we demonstrate the significance of this problem in an open-source full-stack autonomous driving software, Autoware.Auto 1.0, which relies on ROS 2. We give an alternative: Xronos, an open-source framework for distributed embedded systems that has a novel coordination strategy with predictable properties under clearly stated assumptions. If these assumptions are violated, Xronos provides for application-specific fault handlers to be invoked. We port Autoware.Auto to Xronos and show that it avoids the identified problems with manageable cost in end-to-end latency. Furthermore, we compare the maximum throughput of Xronos to ROS 2 and MQTT using microbenchmarks under different settings, including on three different hardware configurations, and find that it can match or exceed those frameworks in terms of throughput.

cs.DC↗

arXiv2021

Quantifying and Generalizing the CAP Theorem

In distributed applications, Brewer's CAP theorem tells us that when networks become partitioned, there is a tradeoff between consistency and availability. Consistency is agreement on the values of shared variables across a system, and availability is the ability to respond to reads and writes accessing those shared variables. We quantify these concepts, giving numerical values to inconsistency and unavailability. Recognizing that network partitioning is not an all-or-nothing proposition, we replace the P in CAP with L, a numerical measure of apparent latency, and derive the CAL theorem, an algebraic relation between inconsistency, unavailability, and apparent latency. This relation shows that if latency becomes unbounded (e.g., the network becomes partitioned), then one of inconsistency and unavailability must also become unbounded, and hence the CAP theorem is a special case of the CAL theorem. We describe two distributed coordination mechanisms, which we have implemented as an extension of the Lingua Franca coordination language, that support arbitrary tradeoffs between consistency and availability as apparent latency varies. With centralized coordination, inconsistency remains bounded by a chosen numerical value at the cost that unavailability becomes unbounded under network partitioning. With decentralized coordination, unavailability remains bounded by a chosen numerical quantity at the cost that inconsistency becomes unbounded under network partitioning. Our centralized coordination mechanism is an extension of techniques that have historically been used for distributed simulation, an application where consistency is paramount. Our decentralized coordination mechanism is an extension of techniques that have been used in distributed databases when availability is paramount.

cs.DC↗

arXiv2019

Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning

We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking search algorithm, which can already solve formulas of impressive size - up to hundreds of thousands of variables. The main challenge is to find a representation of these formulas that lends itself to making predictions in a scalable way. For a family of challenging problems, we learned a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.

cs.LO↗