More Like this

1. Deterministic Coordination across Multiple Timelines

   https://doi.org/10.1145/3615357  

   Lohstroh, Marten; Bateni, Soroush; Menard, Christian; Schulz-Rosengarten, Alexander; Castrillon, Jeronimo; Lee, Edward A (September 2024, ACM Transactions on Embedded Computing Systems)

   We discuss a novel approach for constructing deterministic reactive systems that revolves around a temporal model that incorporates a multiplicity of timelines. This model is central toLingua 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. Our temporal model differs from existing models like the logical execution time (LET) paradigm and synchronous languages in that it reflects that there are always at least two distinct timelines involved in a reactive system; alogicalone and aphysicalone—and possibly multiple of each kind. This article explains how the relationship between events across timelines facilitates reasoning about consistency and availability across components in cyber-physical systems (CPSs). 

   more » « less
2. High-performance Deterministic Concurrency Using Lingua Franca

   https://doi.org/10.1145/3617687  

   Menard, Christian; Lohstroh, Marten; Bateni, Soroush; Chorlian, Matthew; Deng, Arthur; Donovan, Peter; Fournier, Clément; Lin, Shaokai; Suchert, Felix; Tanneberger, Tassilo; et al (December 2023, ACM Transactions on Architecture and Code Optimization)

   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
3. Toward Dynamism in Distributed Lingua Franca Programs

   https://doi.org/10.1109/LES.2024.3465408  

   Jerad, Chadlia; Lee, Edward A (September 2024, IEEE Embedded Systems Letters)

   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
4. Towards Building Verifiable CPS using Lingua Franca

   https://doi.org/10.1145/3609134  

   Lin, Shaokai; Manerkar, Yatin A.; Lohstroh, Marten; Polgreen, Elizabeth; Yu, Sheng-Jung; Jerad, Chadlia; Lee, Edward A.; Seshia, Sanjit A. (October 2023, ACM Transactions on Embedded Computing Systems)

   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
5. Lightning Geolocation and Flash Rates From LF Radio Observations During the RELAMPAGO Field Campaign

   https://doi.org/10.1029/2021EA001813  

   Antunes de Sá, A.; Marshall, R.; Deierling, W. (October 2021, Earth and Space Science)

   Abstract The lightning data products generated by the low‐frequency (LF) radio lightning locating system (LLS) deployed during the Remote sensing of Electrification, Lightning, and Mesoscale/Microscale Processes with Adaptive Ground Observation (RELAMPAGO) field campaign in Argentina provide a valuable data set to research the lightning evolution and characteristics of convective storms that produce high‐impact weather. LF LLS data sets offer a practical range for mesoscale studies, allowing for the observation of lightning characteristics of storms such as mesoscale convective systems or large convective lines that travel longer distances which are not necessarily staying in range of regional VHF‐based lightning detection systems throughout their lifetime. LF LLSs also provide different information than optical space‐borne lightning detectors. Lightning measurements exclusive to LF systems include discharge peak current, lightning polarity, and lightning type classification based on the lightning‐emitted radio waveform. Furthermore, these measurements can provide additional information on flash rates (e.g., positive cloud‐to‐ground flash rate) or narrow bipolar events which may often be associated with dynamically intense convection. In this article, the geolocation and data processing of the LF data set collected during RELAMPAGO is fully described and its performance characterized, with location accuracy better than 10 km. The detection efficiency (DE) of the data set is compared to that of the Geostationary Lightning Mapper, and spatiotemporal DE losses in the LF data set are discussed. Storm case studies on November 10, 2018, highlight the strengths of the data set, which include robust flash clustering and insightful flash rate and peak current measures, while illustrating how its limitations, including DE losses, can be managed. 

   more » « less