Søk etter:

Started 21Feb2024. Updated 01Sep2024 (ForeC). This note is in group Technology. Observe Standard disclaimer.

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 :

«Overview
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 discussion of Lee‘s paper by the same name.

ForeC

A Lingua Franca processor (MultiPRET, a multicore version of FlexPRET (there also is another one called InterPRET)) that uses shared memory for inter-core communication may be programmed in a language called ForeC. (Was this the right way to write this?)

The ForeC language is supposed to compete with the synchronous language Esterel. It’s meant to be a deterministic language for parallel programming of Cyber-physical systems (CPSs). In the abstract of [6] I read:

«One of ForeC’s main innovation is its shared variable semantics that provides thread isolation and deterministic thread communication. Through benchmarking, we demonstrate that ForeC can achieve better parallel performance than Esterel, a widely used synchronous language for concurrent safety-critical systems, and OpenMP, a popular desktop solution for parallel programming. .. One of ForeC’s main innovation is its shared variable semantics that provides thread isolation and deterministic thread communication.»

And in the paper that:

«A statement (st) in ForeC can be a traditional C statement (c st), or a barrier (pause), fork/join (par), or preemption (abort) statement. Using the sequence operator ( ; ) a statement in ForeC can be an arbitrary composition of other statements. Like C, extra properties can be specified for variables using type qualifiers. A type qualifier (tq) in ForeC is a traditional C type qualifier (c tq), an environment interface (input and output), or a shared variable amongst threads (shared).»

Other keywords would be weak?, when immediate? and combine <new> <mod> <all> with. Plus the concept of the global tick is very important. The scheduler uses context-switching points caused by a pause etc., with no preemption.

Very interesting. In the synchronous language article on Wikipedia (1) synchronous languages are contrasted with (2) asynchronous languages and those that (3) interact synchronously (like occam, XC and Go). To me another interesting contrast is that while ForeC has made a system out of safe usage of shared variables and to use them for communication, the channels of CSP-like languages, especially when channel dimension is zero, ie. synchronous channels, may be considered as a system of keys around shared variables. CSP was, I think, kind of made to solve this very problem. Channels are about sharing and communication variables.

But admittedly, I think it’s timed CSP that would be needed in «my world» for time determinism or time predictability, and that occam does not have any direct guaranteed time deterministic properties. Even if CSPm (in FDR3, FDR4 or the like [7]) will, by refinement, formally verify properties like «traces, failures, failures / divergence and some other alternatives» to quote Wikipedia. However, XC on XCORE do, based more or less on the same model of concurrency, where hard real-time is piece of cake. Even in occam and perhaps all more-or-less real-time systems it is easy to detect a broken deadline.

In the ForeC article they have no reference to CSP, Hoare or Roscoe. Anyhow, thanks to a student’s Master’s which I was lucky enough to read for referencing to ForeC. The rest of this text chapter is on me, of course.

References

1. 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 
2. Rebeca Modeling Language, Actor-based Language with Formal Foundation, from Mälardalen University, see https://rebeca-lang.org/Rebeca
3. 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
4. ForSyDe, A Methodology for Formal System Design, Igor Sander (creator and main contributor), see https://forsyde.github.io
5. 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)
6. The ForeC Synchronous Deterministic Parallel Programming Language for Multicores by Yip, Girault, Roop and Biglari-Abhari. In 2016 IEEE 10th International Symposium on Embedded Multicore/Many-core Systems- on-Chip (MCSOC), 2016, pp. 297–304. Read at https://www.researchgate.net/publication/311530876_The_ForeC_Synchronous_Deterministic_Parallel_Programming_Language_for_Multicores
7. Cocotec, see https://cocotec.io (now handles FDR (Wikipedia), now FDR4 (© University of Oxford)