Does an LF program define a single global logical timeline?

[lsk567]

In the back of my head, I always have the understanding that "each LF program defines a single global logical timeline" and this single logical timeline is the source of (data-)determinism. However, after thinking about this further, this might not be the case. I am bringing up this topic here to make sure we are on the same page.

Consider the following example.

We often say that reactors have discrete-event (DE) semantics, which seems to involve a single global logical timeline/behavior (let's call this Interpretation A).
The DE semantics implies that the above program has the following logical behavior.

(Drawn using asciiflow.com)

     ^           ^           ^
     |           |           |
t1   |           |           |   Repeat...
     |           |           |
     +-------+---+---+-------+----------------->
     |       |       |       |
t2   |       |       |       |
     |       |       |       |
     v       v       v       v

     0       2   3   4       6

All the scheduling and formal analyses can be done w.r.t. this "correct" logical behavior defined by the program.

---

On the other hand, in CyPhy'19, TECS'21, and ISoLA'21, each reactor is said to "see events/inputs in timestamp order," which seems to define the logical timeline at a "local" level. In other words, the reactor semantics mandates that each reactor processes its inputs and locally generated events (firings of timers and actions) in timestamp order but says nothing about the "global" ordering of events across reactors (Interpretation B).

The CAL'21 paper seems to further strengthen this view by allowing unavailabilities to be -oo when two reactors do not have data dependencies between each other, suggesting that each of them can be independently executed.

Under this view, from t1's and t2's perspectives, each of them has a well-defined single logical timeline.

     ^           ^           ^
     |           |           |
t1   |           |           |   Repeat...
     |           |           |
     +-----------+-----------+----------------->

     0           3           6

     +-------+-------+-------+----------------->
     |       |       |       |
t2   |       |       |       |   Repeat...
     |       |       |       |
     v       v       v       v

     0       2       4       6

But from the view of the top-level reactor TimersInReactors, its logical timeline is undefined, which potentially means that any interleaving of t1's timeline and t2's timeline is valid, including the following.

   0@t1        3@t1        6@t1

     ^           ^           ^
     |           |           |
t1   |           |           |
     |           |           |
     +-----------+-----------+-----------------+-------+-------+-------+--------->
                                               |       |       |       |
t2                                             |       |       |       |
                                               |       |       |       |
                                               v       v       v       v

                                             0@t2    2@t2    4@t2    6@t2

---

Our runtime currently implements global barrier synchronization, which could be understood as either following Interpretation A precisely or choosing a very specific interleaving out of all interleavings allowed by Interpretation B.

Whether Interpretation A or Interpretation B is used has implications on runtime scheduling, formal analyses, and developer ergonomics.

If Interpretation A is used:

1. global barrier synchronization is here to stay;
2. the state space of an LF program is smaller, making scheduling and verification potentially easier;
3. existing results for DE models could apply well to reactors;
4. failing to advance time in a subsystem could block the whole system;
5. for developers, fairly easy to imagine and understand the state space at the system level.

If Interpretation B is used:

1. global barrier synchronization can be relaxed, potentially enabling more performance;
2. the state space of an LF program is larger, making scheduling and verification potentially harder;
3. reactors are much more expressive than typical DE models; many DE formalisms and analyses need to be redesigned;
4. more resilient toward failures in subsystems;
5. for developers, more difficult to imagine and understand the state space at the system level.

I think in general we are heading toward Interpretation B. Please leave comments below if there are alternative views to any of the points above. Thanks!

---

Update: there should be only one logical timeline (Interpretation A). A short summary is added below.

[ChadliaJerad]

Not sure I got your point clearly. But I am sharing my opinion about what I understood.

I think that Interpretation B makes room for (data) non-determinism, particularly if the reactions triggered by t1 and t2 modify the shared state variables.
Interpretation A, however, imposes (data) determinism. Using Logical Time projections in Physical Time () can help grasp the underlying ordering. Let's consider a function P that provides such projection. Having 'TimersInReactors` executing correctly means that the conjunction of the following constraints is observed:

• P(0L@t1) < P(0L@t2)
• P(2L@t2) < P(3L@t1)
• P(3L@t1) < P(4L@t2)
• P(6L@t1) < P(6L@t2), etc.
  Please note that the added L is just for overspecifying that it is about Logical Time.

These constraints are the source of determinism. They are, kind of omitted in Interpretation B, again, if my understanding is correct.

Reducing the lag between Logical Time and Physical Time, however, is kind of a measurable QoS metric, in the sense that:

• for every timer y, P(xL@ty) <= x + offset (assuming fast mode is not activated)
  where offset = P(0L@TimersInReactors)

If I succeed to come up with an illustrating diagram, I will share it.

[edwardalee]

This is a very subtle point, but I will make an argument for sticking with interpretation A.

Under the assumption that reactors do not share state, there is no observable difference between these interpretations. The unavailabilities in the CAL theorem are irrelevant, because they refer to physical time.

I think that in adopting interpretation B, you are trying to map each reactor's view of logical time onto a physical timeline. But whole point of separating logical from physical time is precisely to avoid doing this except exactly where it is needed (physical actions, deadlines, and safe-to-process offsets). In your above example, it is not needed anywhere, and therefore there is no need to have any relationship at all between logical time and physical time, except that the events each reactor sees that are ordered in logical time must also be ordered in the local physical time.

Semantically, an ordered set is ordered no matter how I examine it. The set of natural numbers is an ordered set even if I list its elements in a funny way, e.g., if you list the odd numbers and I list the even numbers. Each of us will see an ordered list, or, put another way, if we don't communicate, each of sees only an ordered list. The underlying set is still totally ordered.

Also, we don't have to relax barrier synchronization to allow any interleaving (in physical time) of t1 and t2's timelines. Federated execution already does this. But there should be no observable difference between any two interleavings.

When reactors interact with physical world through sensors and actuators, then, in effect, they share the state of the physical world. But the state of the physical world is an ill-defined concept (Bell's theorem tells us that if you insist that the physical world has a state, then either faster-than-light communication is possible or quantum theory is wrong). This is why the physical timeline has to be local to each federate. In practice, when you need reactors to interact through the physical world, then you need to synchronize clocks and you need to align the logical timeline with these synchronized clocks at the points where this interaction occurs. Even then, events will not have a well-defined order when mapped onto any one physical timeline unless they are causally related (communication occurs).

On the question of verification, if you insist on mapping events onto a single physical timeline, then yes, things will get enormously complex. So don't do that. Dispense with the notion of a single global system state and the problem goes away. Each observer sees events in the right order, but only if there is an observer who sees all events is there any need to list all of them in order (and that need is only for that one observer... other observers may still see things in random order on any single physical timeline). As soon as you insist that there is a single global system state, then you are stuck with the problem you cite. But then you also have a model that is not physically realizable (unless faster than light communication is possible or quantum mechanics is wrong).

Section 3.2 of my 2021 Determinism paper addresses this latter point and critiques Milner's introduction of the notion of "confluence" to attempt to deal with this problem by replacing the notion of determinism. That paper argues that confluence is not needed. Determinism in its original form is sufficient.

[lsk567]

Thanks, @edwardalee!

I think that in adopting interpretation B, you are trying to map each reactor's view of logical time onto a physical timeline.

Yes, indeed. I see that now. Perhaps the relationship between the logical and physical timeline can be described as "each LF program defines a single logical timeline, which could have multiple feasible manifestations in physical time."

So the example program defines a single logical timeline that looks like this.

     ^           ^           ^
     |           |           |
t1   |           |           |   Repeat...
     |           |           |
     +-------+---+---+-------+----------------->
     |       |       |       |
t2   |       |       |       |
     |       |       |       |
     v       v       v       v

     0       2   3   4       6

But it is perfectly okay for some observer to see a trace that looks like this in physical time. For example, each timer firing could blink an LED once, which is observed by a human observer.

   0@t1        3@t1        6@t1

     ^           ^           ^
     |           |           |
t1   |           |           |
     |           |           |
     +-----------+-----------+-----------------+-------+-------+-------+---------> Physical Time
                                               |       |       |       |
t2                                             |       |       |       |
                                               |       |       |       |
                                               v       v       v       v

                                             0@t2    2@t2    4@t2    6@t2

This physical time behavior is valid (which could appear surprising), and the federated execution currently could deliver this behavior.
A runtime relaxing global barrier synchronization could also deliver this behavior.

A verification model that describes the logical time behavior cannot be directly used to verify properties in the physical time unless these assumptions are stated:

1. to verify properties related to event order, the event ordering specified in the logical timeline needs to be delivered by the runtime in physical time (which seems to suggest non-federated execution with global barrier synchronization);
2. to verify physical timing properties, the physical invocation times of reactions need to correspond precisely to the logical time tags.

To verify properties for physical timelines that resemble the 2nd diagram above, a more fine-grained verification model is needed.

[ChadliaJerad]

Here are two possible executions, which follow LF semantics (Interpretation A).

[lsk567]

@ChadliaJerad, thanks for your insights and these illustrative diagrams! I certainly see your point here.

I also want to offer one view under which Interpretation B is deterministic. Determinism in @edwardalee's paper is defined as "A model is deterministic if, given all the inputs that are provided to the model, the model defines exactly one possible behavior."

If we define the "behavior" of a reactor as a sequence of snapshots of its internal state (including state variables, inputs, outputs, action/timer firings, etc.) and assume that reactors t1 and t2 do not share state, then the reactor model under Interpretation B is deterministic. In this definition, whether the model is deterministic does not depend on the interleaving of the state sequence of t1 and t2.

But we can easily define "behavior" in a way that does depend on the interleaving, which could render the model nondeterministic. I think this is the point you are making above. Please let me know if I misunderstand.

[ChadliaJerad]

I see your point @lsk567. And indeed, I had interleaving in mind, when thinking about the behavior.
Please have a look and the upcoming comment.

[lsk567]

I agree with @edwardalee's interpretation below...

[petervdonovan]

Given Edward's below comment, it seems like the mechanism that LF exposes for ordering physical events is to route the events to a reactor that acts as an "observer." So, as a concrete example, LF programmers should not be using printf or lf_print if they want their program to have deterministic outputs (on stdout); instead, they should instantiate a single stdout reactor and route all messages to that reactor. To keep prints from getting lost, they would have to pile the prints up in logical time or put them in different channels of a giant multiport whose size is constantly increasing as the programmer writes more message-producing modules.

[edwardalee]

Part of the art here is what we mean by "observer." If an observer has to be a reactor, and reactors do not share state, then every observer sees all events in timestamp order. Events it does not see are irrelevant.

[lsk567]

Here is a short summary of the points discussed:

1. An LF program should define a single global logical timeline, which could have multiple feasible manifestations in physical time.
2. Observers define the state space: reactor observers see events in logical time; human observers see events in physical time. Property specifications need to be given w.r.t. observer specifications.
3. Verification is easier for reactor observers since they see events in (logical) timestamp order. Verification for human observers is harder since mapping events onto a single physical timeline involves many possible interleavings.
4. For a human observer, events observed in physical time might NOT follow the exact logical timestamp order (as delivered by federated execution or non-federated execution without global barrier synchronization) unless communication (an act of establishing happened-before relations) is explicitly specified in the LF program or maintained additionally by the runtime.

[ChadliaJerad]

For a human observer, events observed in physical time might NOT follow the exact logical timestamp order (as delivered by federated execution or non-federated execution without global barrier synchronization) unless communication (an act of establishing happened-before relations) is explicitly specified in the LF program or maintained additionally by the runtime.

I still think that a federated version and a non-federated version of TimersInReactors, even when they do not share a global state, need to show a non-arbitrary pattern of execution. The reference for the pattern of execution is the logical time. It is already the case for the non-federated version.
Shouldn't there be something in common?

Recalling Determinism definition: "A model is deterministic if, given all the inputs that are provided to the model, the model defines exactly one possible behavior", in our case, time is one of the inputs. And that's the logical time.
If a federate logical time is kind of the observer, shouldn't we lean toward a consensus across the observers?
The consensus should also meet the non-federated observer observations.
I see this as a way to define what can be "one possible behavior".
If my understanding is correct, it is possible to set such an execution pattern in case of a federated execution (be it centralized or not).

Please criticize!

[edwardalee]

In theory, consensus among all observers is only possible if all events occur at exactly one point in space. If any two events occur at different points in space, then the order in which they occur can be different for different observers. This follows from relativity. Hence, the consensus you ask for is only (theoretically) possible if the entire execution is a single sequence occurring at one point in space.

Reducing this to a practical level, we can approximate a universal consensus by implementing a barrier synchronization for every tag advancement. In order to advance time, a federate would have to wait until it has heard from all other federates that they are ready to advance time too. This would still only be an approximation, because events that occur within a tag, such as actuating something the physical world, will still be distributed and therefore can occur in different orders for different observers. The only way to get rid of that ambiguity is to reduce the physical size of the implementation to a single point. Only then will all possible observers see everything in the same order.