An official website of the United States government
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 deterministic concurrency. In this article, we present an efficient, parallel implementation of reactors and demonstrate that the determinacy of reactors does not imply a loss in performance. To show this, we evaluateLingua Franca(LF), a reactor-oriented coordination language. LF equips mainstream programming languages with a deterministic concurrency model that automatically takes advantage of opportunities to exploit parallelism. 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.86× and 1.42×, respectively.
more »
« less
Toward Dynamism in Distributed Lingua Franca Programs
Distributed systems often require dynamic capabilities to ensure adaptability, efficiency, and fault-tolerance. In applications where determinism and timing are crucial, a clear and well-defined approach to deterministic dynamism is much needed, but inherently difficult to define. This work gives dynamism deterministic semantics, thus enabling precise and repeatable behavior. To this end, we select the Lingua Franca (LF) coordination language that is based on the reactor model, and introduce dynamism to the distributed LF programs, referred to as federations. This paper outlines the challenges associated with incorporating transient federates, which are capable of joining and leaving the federation at arbitrary times, and proposes solutions to the identified problems. A realistic example of an online auction system is used to illustrate the approach. Furthermore, the potential applications of this mechanism are discussed, along with the challenges that need to be addressed.
more »
« less
- Award ID(s):
- 2233769
- PAR ID:
- 10554369
- Publisher / Repository:
- IEEE
- Date Published:
- Journal Name:
- IEEE Embedded Systems Letters
- ISSN:
- 1943-0663
- Page Range / eLocation ID:
- 1 to 1
- Subject(s) / Keyword(s):
- Reactor Model Distributed Systems Determinism Dynamism
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We discuss a novel approach for constructing deterministic reactive systems that evolves around a temporal model which incorporates a multiplicity of timelines. This model is central to LINGUA FRANCA (LF), a polyglot coordination language and compiler toolchain we are developing for the definition and composition of concurrent components called Reactors, which are objects that react to and emit discrete events. What sets LF apart from other languages that treat time as a first-class citizen is that it confronts the issue that in any reactive system there are at least two distinct timelines involved; a logical one and a physical one-and possibly multiple of each kind. LF provides a mechanism for relating events across timelines, and guarantees deterministic program behavior under quantifiable assumptions.more » « less
-
Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derivedautomaticallyfrom its implementation. Our approach requires that the system implementation is specified inLingua Franca(LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engineUclid5using theZ3SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifierand evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifiercorrectly checks 21 out of 22 programs automatically.more » « less
-
AUTOSAR Adaptive Platform (AP) is an emerging industry standard that tackles the challenges of modern auto- motive software design, but does not provide adequate mech- anisms to enforce deterministic execution. This poses profound challenges to testing and maintenance of the application software, which is particularly problematic for safety-critical applications. In this paper, we analyze the problem of nondeterminism in AP and propose a framework for the design of deterministic automotive software that transparently integrates with the AP communication mechanisms. We illustrate our approach in a case study based on the brake assistant demonstrator application that is provided by the AUTOSAR consortium. We show that the original implementation is nondeterministic and discuss a deterministic solution based on our framework.more » « less
-
Spatial interpolation techniques play an important role in hydrology, as many point observations need to be interpolated to create continuous surfaces. Despite the availability of several tools and methods for interpolating data, not all of them work consistently for hydrologic applications. One of the techniques, the Laplace Equation, which is used in hydrology for creating flownets, has rarely been used for data interpolation. The objective of this study is to examine the efficiency of Laplace formulation (LF) in interpolating data used in hydrologic applications (hydrologic data) and compare it with other widely used methods such as inverse distance weighting (IDW), natural neighbor, and ordinary kriging. The performance of LF interpolation with other methods is evaluated using quantitative measures, including root mean squared error (RMSE) and coefficient of determination (R2) for accuracy, visual assessment for surface quality, and computational cost for operational efficiency and speed. Data related to surface elevation, river bathymetry, precipitation, temperature, and soil moisture are used for different areas in the United States. RMSE and R2 results show that LF is comparable to other methods for accuracy. LF is easy to use as it requires fewer input parameters compared to inverse distance weighting (IDW) and Kriging. Computationally, LF is faster than other methods in terms of speed when the datasets are not large. Overall, LF offers a robust alternative to existing methods for interpolating various hydrologic data. Further work is required to improve its computational efficiency.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1109/LES.2024.3465408
