Mimosa

Mimosa: A Language for Asynchronous Implementation of Embedded Systems Software

Nikolaus Huber ⁽¹⁾, Susanne Graf ^{(1, 2)}, Philipp Rümmer ^{(1, 3)}, Wang Yi ⁽¹⁾

⁽¹⁾ Uppsala University, Uppsala, Sweden
⁽²⁾ Université Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France
⁽³⁾ University of Regensburg, Regensburg, Germany

Motivation

Synchronous paradigm

Lustre/SCADE, Esterel, Signal, ...
safety-critical embedded control

Modern execution platforms

Multi- & many-core processors
distributed systems

(Safe) updates?

MIMOS

Kahn process networks (KPNs)
(Timed) release patterns
(Timed) read/write patterns

Our contribution

MIMOS Application language
Focus on formal semantics
Naturally divides into

Semantics for computation
Semantics for coordination

Prototype simulator


		step print_int (_ : int) --> ()
		step add (x, y) --> z { z = x + y }
		step split x --> (o1, o2, o3) { o1, o2, o3 = x, x, x }

		channel a : int = { 1 }
		channel b : int = { 0 }
		channel c : int
		channel d : int

		node add implements add (a, c) --> (b) every 10ms
		node split implements split (b) --> (a, d, c) every 10ms
		node print implements print_int (d) --> () every 10ms

$$\small \begin{align*} \begin{array}{rcll} e : \text{Expression} & ::= & x & \text{Variable} \\ {} & | & c & \text{Constant} \\ {} & | & e\bm{,}\, \ldots\bm{,}\, e & \text{Tuple} \\ {} & | & \textbf{pre}\, e & \text{Pre} \\ {} & | & e\, \bm{\rightarrow}\, e & \text{Initialized-by} \\ {} & | & e\, \textbf{fby}\, e & \text{Followed-by} \\ {} & | & e\, e & \text{Application} \\ {} & | & \textbf{if}\, e\, \textbf{then}\, e\, \textbf{else}\, e & \text{Conditional} \\ {} & | & \textbf{None} & \text{None} \\ {} & | & \textbf{Some}\, e & \text{Some} \\ {} & | & \textbf{either}\, e\, \textbf{or}\, e & \text{Option match} \\ {} & | & \bm{\lambda}_{p_{in}}^{p_{out}} \bm{.} [p_i = e_i]^n & \text{Abstraction} \\ p : \text{Pattern} & ::= & x & \text{Variable pattern} \\ {} & | & p\bm{,}\, \ldots\bm{,}\, p & \text{Tuple pattern} \end{array} \end{align*}$$

Environments

$$\Gamma \quad \subseteq \quad \textbf{Names} \times \textbf{Values}$$

Projection

\[\begin{align*}(x \mapsto 1, y \mapsto 2) \Downarrow_x\; &=\; 1 \\ (x \mapsto 1, y \mapsto 2) \Downarrow_{(x, y)}\; &=\; (1, 2)\end{align*}\]

Update

\[\begin{align*}(x \mapsto 1, y \mapsto 2) \Uparrow_z^3\; &=\; (x \mapsto 1, y \mapsto 2, z \mapsto 3) \\ (x \mapsto 1, y \mapsto 2) \Uparrow_{(x, y)}^{(3, 4)}\; &=\; (x \mapsto 3, y \mapsto 4)\end{align*}\]

Step semantics

How to model state?
Big-step + rewrite semantics

\[\Gamma \vdash e \Rightarrow v, e'\]

\[ \begin{gather*} \begin{aligned} \frac{}{\Gamma \vdash x \Rightarrow \Gamma \Downarrow_x, x}\; \texttt{\small (Var)} & \; & \frac{}{\Gamma \vdash c \Rightarrow c, c}\; \texttt{\small (Const)} & \; & \frac{\Gamma \vdash e \Rightarrow v, e'}{\Gamma \vdash \textbf{pre}\, e \Rightarrow \bot, (v \rightarrow \textbf{pre}\, e')}\; \texttt{\small (Pre)} \end{aligned} \\[4mm] \begin{aligned} \frac{\Gamma \vdash e_1 \Rightarrow v_1, \text{\textunderscore}}{\Gamma \vdash e_1\, \textbf{fby}\, e_2 \Rightarrow v_1, e_2}\; \texttt{\small (Fby)} & \; & \frac{\Gamma \vdash e_1 \Rightarrow v_1, \text{\textunderscore} \qquad \Gamma \vdash e_2 \Rightarrow \text{\textunderscore}, e_2'}{\Gamma \vdash (e_1 \bm{\rightarrow} e_2) \Rightarrow v_1, e_2'}\; \texttt{\small (Init)} \end{aligned} \\[4mm] \frac{\Gamma \vdash e_1 \Rightarrow v_1, e_1' \qquad \ldots \qquad \Gamma \vdash e_n \Rightarrow v_n, e_n'}{\Gamma \vdash (e_1, \ldots, e_n) \Rightarrow (v_1, \ldots, v_n), (e_1', \ldots, e_n')}\; \texttt{\small (Tuple)} \\[4mm] \frac{\Gamma \vdash e_1 \Rightarrow \textbf{True}, e_1' \qquad \Gamma \vdash e_2 \Rightarrow v, e_2'}{\Gamma \vdash \textbf{if}\, e_1\, \textbf{then}\, e_2\, \textbf{else}\, e_3 \Rightarrow v, \textbf{if}\, e_1'\, \textbf{then}\, e_2'\, \textbf{else}\, e_3}\; \texttt{\small (IfTrue)} \\[4mm] \frac{\Gamma \vdash e_1 \Rightarrow \textbf{False}, e_1' \qquad \Gamma \vdash e_3 \Rightarrow v, e_3'}{\Gamma \vdash \textbf{if}\, e_1\, \textbf{then}\, e_2\, \textbf{else}\, e_3 \Rightarrow v, \textbf{if}\, e_1'\, \textbf{then}\, e_2\, \textbf{else}\, e_3'}\; \texttt{\small (IfFalse)} \\[4mm] \begin{aligned} \frac{}{\Gamma \vdash \textbf{None} \Rightarrow \textbf{None}, \textbf{None}}\; \texttt{\small (None)} & \; & \frac{\Gamma \vdash e \Rightarrow v, e'}{\Gamma \vdash \textbf{Some}\, e \Rightarrow \textbf{Some}\, v, \textbf{Some}\, e'}\; \texttt{\small (Some)} \end{aligned} \\[4mm] \begin{aligned} \frac{\Gamma \vdash e_1 \Rightarrow \textbf{Some}\, v, e_1'}{\Gamma \vdash (\textbf{either}\, e_1\, \textbf{or}\, e_2) \Rightarrow v, (\textbf{either}\, e_1'\, \textbf{or}\, e_2)}\; \texttt{\small (EthrSome)} & \; & \frac{\Gamma \vdash e_1 \Rightarrow \textbf{None}, e_1' \qquad \Gamma \vdash e_2 \Rightarrow v, e_2'}{\Gamma \vdash (\textbf{either}\, e_1\, \textbf{or}\, e_2) \Rightarrow v, (\textbf{either}\, e_1'\, \textbf{or}\, e_2')}\; \texttt{\small (EthrNone)} \end{aligned} \\[4mm] \frac{\Gamma \vdash e_1 \Rightarrow \bm{\lambda}_{p_{in}}^{p_{out}} \bm{.} [p_i = e_i]^n, \text{\textunderscore} \qquad \Gamma \vdash e_2 \Rightarrow v_2, e_2' \qquad \Gamma \Uparrow_{p_{in}}^{v_2} \vdash [p_i = e_i]^n \hookrightarrow [p_i = e_i']^n, \Gamma'}{\Gamma \vdash e_1\; e_2 \Rightarrow \Gamma' \Downarrow_{p_{out}}, (\bm{\lambda}_{p_{in}}^{p_{out}} \bm{.} [p_i = e_i']^n)\; e_2'}\; \texttt{\small (App)} \\[4mm] \frac{\Gamma' \vdash e_1 \Rightarrow v_1, e_1' \qquad \ldots \qquad \Gamma' \vdash e_n \Rightarrow v_n, e_n'}{\Gamma \vdash [p_i = e_i]^n \hookrightarrow [p_i = e_i']^n, \Gamma' = \Gamma \Uparrow_{p_1}^{v_1} \cdots \Uparrow_{p_n}^{v_n}}\; \texttt{\small (Eqs)} \end{gather*} \]

\[ \begin{gather*} \frac{}{\Gamma \vdash x \Rightarrow \Gamma \Downarrow_x, x}\; \texttt{\small (Var)} \\[0.6cm] \frac{}{\Gamma \vdash c \Rightarrow c, c}\; \texttt{\small (Const)} \end{gather*} \]

\[ \begin{gather*} \frac{\Gamma \vdash e \Rightarrow v, e'}{\Gamma \vdash \textbf{pre}\, e \Rightarrow \bot, (v \rightarrow \textbf{pre}\, e')}\; \texttt{\small (Pre)} \\[0.6cm] \frac{\Gamma \vdash e_1 \Rightarrow v_1, \text{\textunderscore}}{\Gamma \vdash e_1\, \textbf{fby}\, e_2 \Rightarrow v_1, e_2}\; \texttt{\small (Fby)} \\[0.6cm] \frac{\Gamma \vdash e_1 \Rightarrow v_1, \text{\textunderscore} \qquad \Gamma \vdash e_2 \Rightarrow \text{\textunderscore}, e_2'}{\Gamma \vdash (e_1 \bm{\rightarrow} e_2) \Rightarrow v_1, e_2'}\; \texttt{\small (Init)} \end{gather*} \]

\[ \begin{gather*} \frac{\Gamma \vdash e_1 \Rightarrow \bm{\lambda}_{p_{in}}^{p_{out}} \bm{.} [p_i = e_i]^n, \text{\textunderscore} \qquad \Gamma \vdash e_2 \Rightarrow v_2, e_2' \qquad \Gamma \Uparrow_{p_{in}}^{v_2} \vdash [p_i = e_i]^n \hookrightarrow [p_i = e_i']^n, \Gamma'}{\Gamma \vdash e_1\; e_2 \Rightarrow \Gamma' \Downarrow_{p_{out}}, (\bm{\lambda}_{p_{in}}^{p_{out}} \bm{.} [p_i = e_i']^n)\; e_2'}\; \texttt{\small (App)} \\[0.8cm] \frac{\Gamma' \vdash e_1 \Rightarrow v_1, e_1' \qquad \ldots \qquad \Gamma' \vdash e_n \Rightarrow v_n, e_n'}{\Gamma \vdash [p_i = e_i]^n \hookrightarrow [p_i = e_i']^n, \Gamma' = \Gamma \Uparrow_{p_1}^{v_1} \cdots \Uparrow_{p_n}^{v_n}}\; \texttt{\small (Eqs)} \end{gather*} \]

Simulation

Deep embedding into OCaml
Step evaluation → direct translation
Node execution → discrete-event simulation
Step prototypes → OCaml functor

Conclusion

Mimosa as an implementation of MIMOS MoC
Formal semantics

Computation → steps
Coordination → nodes & channels

Prototype simulator

Future work

Compiler
Additional read/write strategies

Registers
Sequences
Upto-k

Effect-type system

Thank you!

Questions?