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 evaluate
- Award ID(s):
- 1836601
- NSF-PAR ID:
- 10311561
- Date Published:
- Journal Name:
- Forum on Design Languages (FDL '20)
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
more » « less
Lingua 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
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 derived
automatically from 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 engineUclid5 using theZ3 SMT 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 Verifier and 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 Verifier correctly checks 21 out of 22 programs automatically. -
more » « less
Probabilistic hazard assessments for studying overland pyroclastic flows or atmospheric ash clouds under short timelines of an evolving crisis, require using the best science available unhampered by complicated and slow manual workflows. Although deterministic mathematical models are available, in most cases, parameters and initial conditions for the equations are usually only known within a prescribed range of uncertainty. For the construction of probabilistic hazard assessments, accurate outputs and propagation of the inherent input uncertainty to quantities of interest are needed to estimate necessary probabilities based on numerous runs of the underlying deterministic model. Characterizing the uncertainty in system states due to parametric and input uncertainty, simultaneously, requires using ensemble based methods to explore the full parameter and input spaces. Complex tasks, such as running thousands of instances of a deterministic model with parameter and input uncertainty require a High Performance Computing infrastructure and skilled personnel that may not be readily available to the policy makers responsible for making informed risk mitigation decisions. For efficiency, programming tasks required for executing ensemble simulations need to run in parallel, leading to twin computational challenges of managing large amounts of data and performing CPU intensive processing. The resulting flow of work requires complex sequences of tasks, interactions, and exchanges of data, hence the automatic management of these workflows are essential. Here we discuss a computer infrastructure, methodology and tools which enable scientists and other members of the volcanology research community to develop workflows for construction of probabilistic hazard maps using remotely accessed computing through a web portal.
-
This research paper describes the development of a critical incident-centered analysis methodology based on Schlossberg’s Transition Theory to explore transitions experienced by engineering education researchers as they begin new faculty positions. Understanding the transition experiences of scholars aiming to impact change within engineering education is important for identifying approaches to support the sustained success of these scholars at their institutions and within engineering education more broadly. To date, efforts to better prepare future faculty for academic roles have primarily focused on preparing them to be independent researchers, to teach undergraduate courses, and to support their ability to advance their career. Research of early career faculty is similarly limited in scope, focusing mostly on new faculty at research-exclusive universities or on faculty member’s teaching and research practices. To address this gap in the literature, our research team is examining the role of institutional context on the agency of early career engineering education faculty as it relates to facilitating change. As part of this larger project, the focus of this paper is on the integration of critical incident techniques and Schlossberg’s Transition Theory to create “incident timelines” that explore the transition of early career engineering education researchers into new faculty positions. Our paper will illustrate how this integration provided an effective methodology to: 1) explore a diverse set of transitions into faculty positions, 2) identify critical events that impact these transitions, 3) isolate strategies that supported the faculty members in different aspects of their transitions, and 4) examine connections between events and strategies over time and across faculty members’ transitions. Transition Theory provides a lens to explore how individuals identify and adapt based on transitions in their lives. An individual’s transition, according to Schlossberg, tends to include three phases: moving in, moving through, and moving out. Over the course of those phases, the individual’s experiences are influenced by the context of the transition, the characteristics of the individual such as their motivations and beliefs, the extent to which they have support, and the strategies they utilize. Given the complexity of a transition into a faculty position, it was necessary to determine the extent to which particular events and the relationship between events impacted a new faculty member’s experience. To accomplish this, we integrated a critical incident analysis to specifically investigate individual events that were considered significant to the overall transition leading to the development of an incident timeline. We applied our approach to monthly reflections of six new engineering faculty members from diverse institutional contexts who identify as engineering education researchers. The monthly reflections asked each participant to provide their impressions of the faculty role, in what ways they felt like a faculty member, and in what ways they did not. Through an iterative data analysis process, we developed initial incident timelines for each participant’s transition. Follow-up interviews with the participants allowed us to explore each event in more detail and provided an opportunity for reflection-on-action by the participant. These incidents were then further explored to distinguish strategies used and support received. Finally, we examined connections between events and strategies over time to identify overarching themes common to these types of faculty transitions. In this methods paper, we will demonstrate the usefulness of this variation of the critical incident approach for exploring complex professional transitions by highlighting the details of our incident timeline analysis.more » « less
-
This research paper describes the development of a critical incident-centered analysis methodology based on Schlossberg’s Transition Theory to explore transitions experienced by engineering education researchers as they begin new faculty positions. Understanding the transition experiences of scholars aiming to impact change within engineering education is important for identifying approaches to support the sustained success of these scholars at their institutions and within engineering education more broadly. To date, efforts to better prepare future faculty for academic roles have primarily focused on preparing them to be independent researchers, to teach undergraduate courses, and to support their ability to advance their career. Research of early career faculty is similarly limited in scope, focusing mostly on new faculty at research-exclusive universities or on faculty member’s teaching and research practices. To address this gap in the literature, our research team is examining the role of institutional context on the agency of early career engineering education faculty as it relates to facilitating change. As part of this larger project, the focus of this paper is on the integration of critical incident techniques and Schlossberg’s Transition Theory to create “incident timelines” that explore the transition of early career engineering education researchers into new faculty positions. Our paper will illustrate how this integration provided an effective methodology to: 1) explore a diverse set of transitions into faculty positions, 2) identify critical events that impact these transitions, 3) isolate strategies that supported the faculty members in different aspects of their transitions, and 4) examine connections between events and strategies over time and across faculty members’ transitions. Transition Theory provides a lens to explore how individuals identify and adapt based on transitions in their lives. An individual’s transition, according to Schlossberg, tends to include three phases: moving in, moving through, and moving out. Over the course of those phases, the individual’s experiences are influenced by the context of the transition, the characteristics of the individual such as their motivations and beliefs, the extent to which they have support, and the strategies they utilize. Given the complexity of a transition into a faculty position, it was necessary to determine the extent to which particular events and the relationship between events impacted a new faculty member’s experience. To accomplish this, we integrated a critical incident analysis to specifically investigate individual events that were considered significant to the overall transition leading to the development of an incident timeline. We applied our approach to monthly reflections of six new engineering faculty members from diverse institutional contexts who identify as engineering education researchers. The monthly reflections asked each participant to provide their impressions of the faculty role, in what ways they felt like a faculty member, and in what ways they did not. Through an iterative data analysis process, we developed initial incident timelines for each participant’s transition. Follow-up interviews with the participants allowed us to explore each event in more detail and provided an opportunity for reflection-on-action by the participant. These incidents were then further explored to distinguish strategies used and support received. Finally, we examined connections between events and strategies over time to identify overarching themes common to these types of faculty transitions. In this methods paper, we will demonstrate the usefulness of this variation of the critical incident approach for exploring complex professional transitions by highlighting the details of our incident timeline analysis.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/FDL50818.2020.9232939
