REBLS 2023: Proceedings of the 10th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems

Full Citation in the ACM Digital Library


Thorium: A Language for Bounded Verification of Dynamic Reactive Objects

Developing reliable reactive software is notoriously difficult – particularly when that software reacts by changing its behavior. Some of this difficulty is inherent; software that must respond to external events as they arrive tends to end up in states that are dependent on the value of that input and its order of arrival. This results in complicated corner cases that can be challenging to recognize. However, we find that some of the complexity is an accident of the features of the programming languages widely used in industry. The loops and subroutines of structured programming are well-suited to data transformation, but poorly capture – and sometimes obscure – the flow of data through reactive programs developed using the inversion-of-control paradigm; an event handler that modifies the data flow tends to be declared closer to the definition of the event that activates it than to the initial definition of the data flow that it modifies. This paper approaches both challenges with a language inspired by the declarative modules of languages SIGNAL and Lustre and the semantics of the SodiumFRP Functional Reactive Programming library with a declarative mechanism for self modification through module substitution. These language features lead to software with a code structure that closely matches the flow of data through the running program and thus makes software easier to understand. Further, we demonstrate how those language features enable a bounded model checking approach that can verify that a reactor meets its requirements or present a counterexample trace, a series of states and inputs that lead to a violation. We analyze the runtime performance of the verifier as a function of model size and trace length.


The actor programming model supports the development of concurrent applications by encapsulating state and behavior into independent actors. Each actor is a computational entity with strictly private state and behavior. Actors communicate via asynchronous messaging and, in this way, require neither shared memory nor locking. This makes the actor model suitable not only for parallel programming but also for distributed applications engineering.

The Rust programming language is a statically-typed language that gained a lot of attention in the past years due to its efficient, economical and safe memory management. To ease the development of parallel applications, several actor model frameworks have been built for Rust. However, no actively maintained Rust actor framework provides the necessary features to write distributed applications. For this reason, we propose an extension for Rust’s Actix library, called Actix-Telepathy, that enables remote messaging and offers clustering support. It allows developers to setup remote actors that can communicate across a computer network with the help of a straight forward and easy to understand interface. Our evaluation demonstrates that Actix-Telepathy competes well in remote messaging performance and memory consumption with other actor libraries, such as Scala’s popular Akka library.

Realizing Persistent Signals in JavaScript

Reactive programming enables declarative descriptions of dependencies between and computations throughout signals, an abstraction of time-varying values. Signals have been extended to persistent signals (an abstraction of time-varying values with their execution histories) to enable them to go back in time with any given time. Currently, this feature is only supported by SignalJ, an extension to Java with signals. This limits the use of persistent signals only within the Java-based applications. This is an undesirable restriction, because mechanisms used in realizing persistent signals are actually language-independent. To tackle this problem, we propose an implementation of persistent signals in JavaScript, which makes application areas of persistent signals broader, including Web-frontend. To realize persistent signals in JavaScript, seamless connections between JavaScript programs that run on restricted environments such as browsers and time-series databases that serve histories of persistent signals are required. It is also desirable to reuse existing JavaScript ecosystem. To address these problems, we design a relay-server-based architecture and realize persistent signals in JavaScript as a DSL library.

ComPOS: A DSL for Composing IoT Systems with Weak Connectivity

Future Internet-of-Things (IoT) systems need to combine heterogeneous IoT components and support weak connectivity. This paper introduces ComPOS, a domain-specific language for composing IoT services into systems. ComPOS is a small language but supports powerful message mediation, using stateful reactions with nested and parallel message sequences and anonymous futures. To deal with weak connectivity, we introduce the notion of abort semantics, i.e., aborting old reactions when a newer message arrives. Alternatives to the abort semantics can be obtained by adding strategy services. We evaluated our approach by implementing seven home automation scenarios.

Periodic and Aperiodic Task Description Mechanisms in an FRP Language for Small-Scale Embedded Systems

This paper presents mechanisms for describing real-time tasks in functional reactive programming (FRP) languages for small-scale embedded systems. We have designed and implemented Emfrp, an FRP language for resource-constrained systems, and demonstrated its usefulness with several applications. However, the language requires using external clocks as time-varying values when describing time-dependent behaviors. In this work, we extend the types of time-varying values that express their update timings to describe periodic and aperiodic tasks. The extensions enable concise and precise descriptions of various timed behaviors. We evaluate prototype implementations of the extended language concerning program size, execution time, and power consumption.