Added illustrations of the CAL theorem

examples/C/src/distributed/CAL.lf

@@ -0,0 +1,81 @@
+/**
+ * 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 periods 500ms and 1s
+ * respectively. 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. 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.
+ *
+ * @author Edward A. Lee
+ */
+target C {
+  coordination: centralized
+}
+
+preamble {=
+  #include "platform.h"
+=}
+
+reactor Sense(period: time = 500 ms) {
+  state count: int = 1
+  output out: int
+  timer t(period, period)
+
+  reaction(t) -> out {=
+    lf_set(out, self->count++);
+  =}
+}
+
+reactor Process {
+  input in: int
+  output out: int
+
+  reaction(in) -> out {=
+    lf_sleep(MSEC(35));
+    lf_set(out, in->value * 2);
+  =}
+}
+
+reactor Actuate {
+  input in1: int
+  input in2: int
+
+  reaction(in1) {=
+    printf(PRINTF_TIME ": Received %d\n", lf_time_logical_elapsed(), in1->value);
+  =}
+
+  reaction(in2) {=
+    printf(PRINTF_TIME ": Second input: %d\n", lf_time_logical_elapsed(), in2->value);
+  =} deadline(30 ms) {=
+    printf(PRINTF_TIME ": Second input: %d    ", lf_time_logical_elapsed(), in2->value);
+    printf("PANIC! Deadline violated!\n");
+  =}
+}
+
+federated reactor {
+  s1 = new Sense(period = 500 ms)
+  s2 = new Sense(period = 1 s)
+  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,86 @@
+/**
+ * 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 periods 500ms and 1s
+ * respectively. 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 delay, 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. 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 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 coordinator will preserve availability at the expense of consistency. If
+ * you remove the 200ms `after` delay, however, then you will need to increase the STP offset in the
+ * `Actuate` reactor to get proper decentralized control. Any number significantly larger than the
+ * 35ms processing latency should be sufficient to prevent STP violations.
+ *
+ * @author Edward A. Lee
+ */
+target C {
+  coordination: decentralized
+}
+
+preamble {=
+  #include "platform.h"
+=}
+
+reactor Sense(period: time = 500 ms) {
+  state count: int = 1
+  output out: int
+  timer t(period, period)
+
+  reaction(t) -> out {=
+    lf_set(out, self->count++);
+  =}
+}
+
+reactor Process {
+  input in: int
+  output out: int
+
+  reaction(in) -> out {=
+    lf_sleep(MSEC(35));
+    lf_set(out, in->value * 2);
+  =}
+}
+
+reactor Actuate {
+  input in1: int
+  input in2: int
+
+  reaction(in1) {=
+    printf(PRINTF_TIME ": Received %d\n", lf_time_logical_elapsed(), in1->value);
+  =} STP(10 ms) {=
+    printf(PRINTF_TIME ": STP violation! Received %d\n", lf_time_logical_elapsed(), in1->value);
+  =}
+
+  reaction(in2) {=
+    printf(PRINTF_TIME ": Second input: %d\n", lf_time_logical_elapsed(), in2->value);
+  =} deadline(30 ms) {=
+    printf(PRINTF_TIME ": Second input: %d    ", lf_time_logical_elapsed(), in2->value);
+    printf("PANIC! Deadline violated!\n");
+  =}
+}
+
+federated reactor {
+  s1 = new Sense(period = 500 ms)
+  s2 = new Sense(period = 1 s)
+  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/README.md

@@ -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 control.</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 control.</td>
+</tr>
 </table>