Contents
Intro: ..should not have been here
These aside digressions are here because I don’t know where else to put them. They are all worthy of their own blog notes. But since their contents is not my speciality I won’t pretend. I have zero point zero hands-on experience with these tools. Therefore this is more like a list reflecting the fact that it doesn’t hurt (me), to some extent, to read more than I think I need to read about (*). Asynchronous-based systems (whatever that might mean) certainly have their place. As I see it, especially at the edges of the embedded processors, where the basically asynchronous outside world is met. But not necessarily any assumed «safe by design» (*) embedded software, where I personally relate to a synchronous inside (as CSP). But then Turing would have agreed: I can make the one with the other, or the other way around. And I would add: and the other way around. Then I have at least two tools for my toolbox. Because, yes, the embedded systems also do communicate with each other. Externally. And internally.
(*) Whatever that might mean, I have tried to reason about in nearly all my technological notes. The XCHAN paper at CPA-2012 probably is what I am most proud of, especially in the lack of any academic career. Plus the three timer types (for select/ALT: ALTTIMER, EGGTIMER and REPTIMER) in the CPA-2009 paper. (Both are here.) I worked in industry all my professional life (Notes from the vaults).
| (*) “Conception cannot precede execution.” —Maurice Merleau-Ponty, Sense and Non-Sense Comment (29) in Kit White’s 101 Things to Learn in Art School (© MiT / Kit White (2011, here)): «Art is a process of discovery through making, and our ability to discover is generally greater than our ability to invent. Think of your work process as a form of travel. Look for the things you don’t know, the things that are revealed or inadvertently uncovered. It is easier to find a world than to make one.» |
Credit: For the fact that the small chapters on Lingua Franca, Rebeca and ForSyDe appear here. Thanks to Erling Rennemo Jellum for his sharing of thoughts in a literature group I was lucky enough to be part of. On the way to, and arrival on, his PhD dissertation [5].
Lingua Franca (LF)
Running it in C, Java or Javascript rather than designing new languages seems to be discussed also by others. See [1] which introduces «Lingua Franca» (LF) – which introduces «Reactors», a means to control determinism (fully deterministic or nondeterministic when wanted).
However, the «reactors in C» is built on a translator to C plus libraries and a run-time, so there really is a «Reactor language» per se, as far as I understand it. Even if they have blocks inside the «LF code» framed by {= =} where the target language may be added, not parsed by the LF compiler. At page 36:9 the «LF code» starts with
target C;
reactor X {
More from [3]:
«An LF program with the C target is compiled into a standalone C program that includes the LF runtime system.»
«The C runtime consists of about 2,000 lines of extensively commented code and occupies only tens of kilobytes for a minimal application, making it suitable for deeply embedded platforms. We have tested it on Linux, Windows, and Mac operating systems, on both x86-64 and arm64 architectures, as well as on a precision-timed bare-iron platform called Patmos [61]. On platforms that support pthreads (POSIX threads), our multi-threaded runtime environment (approximately 3,000 lines of code) transparently exploits multiple cores while preserving determinism.»
The reason I quote all this is because I think there may be similarities in the way this theme and the XMOS people may be reasoning about the tools. Plus, the goal of LF and the goal of the XMOS solutions I guess coincide rather well.
Even if CSP or Hoare is not mentioned in [3], its main ref [43] has them referenced. In LF messages flow over typed ports (not untyped channels (Go and occam do have typed channels)). However, port and chan seem to have quite different semantics (page 36:24).
Rebeca Modeling Language
The Rebeca Modeling Language has been in development since 2001. I think its continuous development is now exclusively handled by people at the Mälardalen University in Sweden.
There is Rebeca, plus the extensions Time(ed?) Rebeca and Probabilistic Timed Rebeca. In [2] we read that :
(from [3])
Rebeca is an actor-based language for modeling concurrent and reactive systems with asynchronous message passing. The actor model was originally introduced by Hewitt as an agent-based language, and is a mathematical model of concurrent computation that treats as the universal primitives of concurrent computation. A Rebeca model is similar to the actor model as it has reactive objects with no shared variables, asynchronous message passing with no blocking send and no explicit receive, and unbounded buffers for messages. Objects in Rebeca are reactive, self-contained, and each of them is called a rebec (reactive object). Communication takes place by message passing among rebecs. Each rebec has an unbounded buffer, called message queue, for its arriving messages. Computation is event-driven, meaning that each rebec takes a message that can be considered as an event from the top of its message queue and execute the corresponding message server (also called a method). The execution of a message server is atomic execution (non-preemptive execution) of its body that is not interleaved with any other method execution.»
I attended an interesting lecture by Marjan Sirjani about Rebeca [3]. The above figure is also from [3]; it shows the rationale for going in a somewhat another direction than the tools available at the time: («Different approaches for Modeling and Verification. Abstract and Mathematical. Modeling languages, CCS, CSP, Petri net, RML, Timed Automata, FDR, UPPAAL, SMV, NuSMV, Promela, Spin. Programming languages, Too heavy. Not always formal. Java, Java Pathfinder, Bandera, C, SLAM. Verification techniques: Deduction needs high expertise. Model checking causes state explosion«).
ForSyDe
ForSyDe (Formal System Design), a design methodology for embedded systems, which has a formal foundation in form of models of computation (MoCs) and covers the whole design process from specification to the final implementation [4].
The Reactive Manifesto
I wrote this comment to The Reactive Manifesto some years ago: 077:[A reactive manifest], which discusses the «The Reactive Manifesto». Even before that: 021:[The problem with threads]. It’s a discusseion of Lee‘s paper by the same name.
References
- Writing Reactors in C. See https://github.com/lf-lang/lingua-franca/wiki/Writing-Reactors-in-C#inputs-and-outputs. This is in the Lingua Franca project, see https://github.com/lf-lang/lingua-franca introduced in Toward a Lingua Franca for Deterministic Concurrent System, by Marten Lohstroh, Christian Menard, Soroush Bateni and Edward A. Lee (July 2021). See https://dl.acm.org/doi/10.1145/3448128
- Rebeca Modeling Language, Actor-based Language with Formal Foundation, from Mälardalen University, see https://rebeca-lang.org/Rebeca
- Formal Verification of Cyber-Physical Systems, Marjan Sirjani, Cyber-Physical Systems Analysis Group Mälardalen University, Västerås, Sweden. 19Feb2024 at NTNU: Norwegian University of Science and Technology
Trondheim, Norway, see http://rebeca-lang.org/assets/documents/Sirjani-TrondheimFeb2024.pdf - ForSyDe, A Methodology for Formal System Design, Igor Sander (creator and main contributor), see https://forsyde.github.io
- Predictable Computing for Cyber-Physical Systems by Erling Rennemo Jellum. PhD Thesis, NTNU, Trondheim, February 2024. ISBN 978-82-326-7699-6 (electronic version). See https://hdl.handle.net/11250/3120111 to NTNU Open (for the abstract, at least)
Thank you, Øyvind, for the nice note!
It was a pleasure to give a talk at NTNU in Trondheim, and I certainly enjoyed the discussions and questions after my talk.
takk fyrir síðast!
(in Icelandic)