Merge pull request #87 from lf-lang/cal-examples

Added illustrations of the CAL theorem

examples/C/src/distributed/CAL.lf

@@ -0,0 +1,85 @@
+/**
+ * This program illustrates how relaxing consistency improves availability, as predicted by the CAL
+ * Theorem reported in the following paper:
+ *
+ * Edward A. Lee, Ravi Akella, Soroush Bateni, Shaokai Lin, Marten Lohstroh, Christian Menard.
+ * "Consistency vs. Availability in Distributed Cyber-Physical Systems". ACM Transactions on
+ * Embedded Computing Systems (TECS), September 2023. https://dl.acm.org/doi/10.1145/3609119
+ *
+ * This program has two `Sense` sources of events, `s1` and `s2` with identical periods of 1s. The
+ * `s1` output is processed by the `Process` reactor, which takes at least 35ms to process the data
+ * (emulated by sleeping). As a consequence of this processing latency, were it not for the 200ms
+ * `after` delay, the 30ms deadline of the `Actuate` reactor would be violated every time. The
+ * deadline is on the second reaction, which cannot be invoked before the first reaction when both
+ * reactions are enabled.
+ *
+ * The deadline is an availability requirement, the `after` delay is a tolerance for inconsistency,
+ * and the 35ms processing time is a latency (The C A L in CAL). As long as the actual latency is
+ * not greater than the 200ms tolerance for inconsistency plus the 30ms tolerance for
+ * unavailability, then availability requirement will be met.
+ *
+ * Removing or reducing the after delay strengthens consistency but causes deadline violations.
+ *
+ * This program uses centralized coordination, so if the processing latency plus communication
+ * latency exceeds the 200ms tolerance for inconsistency and the 30ms tolerance for unavailability
+ * (the deadline), then the coordinator will preserve consistency at the expense of availability.
+ * I.e., the deadline will be violated.
+ *
+ * @author Edward A. Lee
+ */
+target C {
+  timeout: 5 s
+}
+
+preamble {=
+  #include "platform.h"
+=}
+
+// Produce a counting sequence starting with 1.
+reactor Sense(period: time = 1 s) {
+  state count: int = 1
+  output out: int
+  timer t(0, period)
+
+  reaction(t) -> out {=
+    lf_set(out, self->count++);
+  =}
+}
+
+// Pass the input unchanged to the output, but take a long time to do it.
+reactor Process {
+  input in: int
+  output out: int
+
+  reaction(in) -> out {=
+    lf_sleep(MSEC(35));
+    lf_set(out, in->value);
+  =}
+}
+
+// Report the inputs.
+reactor Actuate {
+  input in1: int
+  input in2: int
+
+  reaction(in1) {=
+    lf_print(PRINTF_TIME ": Received on in1: %d", lf_time_logical_elapsed(), in1->value);
+  =}
+
+  reaction(in2) {=
+    lf_print(PRINTF_TIME ": Received on in2: %d", lf_time_logical_elapsed(), in2->value);
+  =} deadline(30 ms) {=
+    lf_print(PRINTF_TIME ": Received on in2: %d", lf_time_logical_elapsed(), in2->value);
+    lf_print("  *** PANIC! Deadline violated!");
+  =}
+}
+
+federated reactor {
+  s1 = new Sense()
+  s2 = new Sense()
+  c1 = new Process()
+  a = new Actuate()
+  s1.out -> c1.in
+  c1.out -> a.in1 after 200 ms
+  s2.out -> a.in2
+}

examples/C/src/distributed/CALDecentralized.lf

@@ -0,0 +1,67 @@
+/**
+ * This program illustrates how relaxing consistency improves availability, as predicted by the CAL
+ * Theorem reported in the following paper:
+ *
+ * Edward A. Lee, Ravi Akella, Soroush Bateni, Shaokai Lin, Marten Lohstroh, Christian Menard.
+ * "Consistency vs. Availability in Distributed Cyber-Physical Systems". ACM Transactions on
+ * Embedded Computing Systems (TECS), September 2023. https://dl.acm.org/doi/10.1145/3609119
+ *
+ * This program is just like CAL.lf except that it uses decentralized coordination.
+ *
+ * Removing or reducing the after delay strengthens consistency but causes deadline violations.
+ *
+ * This program uses decentralized coordination, so if the processing latency plus communication
+ * latency exceeds the 200ms tolerance for inconsistency plus the 30ms tolerance for unavailability
+ * (the deadline), then the system can only preserve availability at the expense of consistency.
+ * However, in order to do that, you need to adjust the STP offset, which corresponds to the
+ * processing offset in the CAL theorem. If you remove the 200ms `after` delay, you will need to
+ * increase the STP offset in the `Actuate` reactor to ensure that it does not prematurely assume
+ * the inputs are absent. Any number significantly larger than the 35ms processing latency should be
+ * sufficient to prevent STP violations, but such a number will result in a deadline violation.
+ * Setting a lower number prevents the deadline violation, but at the cost of getting consistency
+ * violations. It is also possible to get _both_ deadline and consistency violations.
+ *
+ * @author Edward A. Lee
+ */
+target C {
+  coordination: decentralized,
+  timeout: 5 s
+}
+
+import Sense, Process from "CAL.lf"
+
+// Override the base class to provide an STP offset.
+reactor ProcessFed(STP_offset: time = 10 ms) extends Process {
+}
+
+// Report inputs received.
+// STP_offset parameter is needed to ensure receiving the last input at time 5s.
+// This has to be less than the deadline or the deadline will always be violated.
+reactor Actuate(STP_offset: time = 20 ms) {
+  input in1: int
+  input in2: int
+
+  reaction(in1) {=
+    lf_print(PRINTF_TIME ": Received on in1: %d", lf_time_logical_elapsed(), in1->value);
+  =} STP(0) {=
+    // No _additional_ STP offset is needed here.
+    lf_print(PRINTF_TIME ": Consistency violation! Received %d", lf_time_logical_elapsed(), in1->value);
+  =}
+
+  reaction(in2) {=
+    lf_print(PRINTF_TIME ": Received on in2: %d", lf_time_logical_elapsed(), in2->value);
+  =} deadline(30 ms) {=
+    lf_print(PRINTF_TIME ": Received on in2: %d", lf_time_logical_elapsed(), in2->value);
+    lf_print("  *** PANIC! Deadline violated!");
+  =}
+}
+
+federated reactor {
+  s1 = new Sense()
+  s2 = new Sense()
+  c1 = new ProcessFed()
+  a = new Actuate()
+  s1.out -> c1.in
+  c1.out -> a.in1 after 200 ms
+  s2.out -> a.in2
+}

examples/C/src/distributed/README.md

@@ -1,6 +1,6 @@
 # Distributed Lingua Franca
 
-When intead of a **main reactor** you defined a **federated reactor**, a Lingua Franca program gets divided into multiple programs that execute as separate processes and can execute on different machines. The coordination and communication is automatically generated to preserve LF semantics so that the programs will logically the same as a non-federated program. See [Distributed Execution documentation](https://www.lf-lang.org/docs/handbook/distributed-execution?target=c) for more details.
+When intead of a **main reactor** you defined a **federated reactor**, a Lingua Franca program gets divided into multiple programs that execute as separate processes and can execute on different machines. The coordination and communication is automatically generated to preserve LF semantics so that the programs will logically behave the same as a non-federated program. See [Distributed Execution documentation](https://www.lf-lang.org/docs/handbook/distributed-execution?target=c) for more details.
 
 This directory includes a series of very simple "Hello World" examples.
 
@@ -15,23 +15,32 @@ To run these programs, you are required to first [install the RTI](https://www.l
 <td> <img src="img/HelloWorld.png" alt="HelloWorld" width="100%"> </td>
 <td> <a href="HelloWorld.lf"> HelloWorld.lf </a>: A MessageGenerator produces a string and sends it over a network connection to a PrintMessage reactor that prints the message.</td>
 </tr>
+<tr>
 <td> <img src="img/HelloWorldAfter.png" alt="HelloWorldAfter" width="100%"> </td>
 <td> <a href="HelloWorldAfter.lf"> HelloWorldAfter.lf </a>: A variant with a logical time delay on the connection.</td>
 </tr>
-</tr>
+<tr>
 <td> <img src="img/HelloWorldDecentralized.png" alt="HelloWorldDecentralized" width="100%"> </td>
 <td> <a href="HelloWorldDecentralized.lf"> HelloWorldDecentralized.lf </a>: A variant that uses decentralized coordination, which relies and clock synchronization. This version uses an **after** delay.</td>
 </tr>
-</tr>
+<tr>
 <td> <img src="img/HelloWorldDecentralizedSTP.png" alt="HelloWorldDecentralizedSTP" width="100%"> </td>
 <td> <a href="HelloWorldDecentralizedSTP.lf"> HelloWorldDecentralizedSTP.lf </a>: A decentralized variant that uses a safe-to-process (STP) offset instead of an **after** delay.</td>
 </tr>
-</tr>
+<tr>
 <td> <img src="img/HelloWorldPhysical.png" alt="HelloWorldPhysical" width="100%"> </td>
 <td> <a href="HelloWorldPhysical.lf"> HelloWorldPhysical.lf </a>: A variant with physical connection.</td>
 </tr>
-</tr>
+<tr>
 <td> <img src="img/HelloWorldPhysicalAfter.png" alt="HelloWorldPhysicalAfter" width="100%"> </td>
 <td> <a href="HelloWorldPhysicalAfter.lf"> HelloWorldPhysicalAfter.lf </a>: A variant with a physical connection and an **after** delay.</td>
 </tr>
+<tr>
+<td> <img src="img/CAL.png" alt="CAL" width="100%"> </td>
+<td> <a href="CAL.lf"> CAL.lf </a>: An illustration of the fundamental tradeoff between consistency, availability, and latency, using centralized coordination.</td>
+</tr>
+<tr>
+<td> <img src="img/CALDecentralized.png" alt="CALDecentralized" width="100%"> </td>
+<td> <a href="CALDecentralized.lf"> CALDecentralized.lf </a>: An illustration of the fundamental tradeoff between consistency, availability, and latency, using decentralized coordination.</td>
+</tr>
 </table>