Merge pull request #269 from lf-lang/mixed-microsteps-and-time

Mixed microsteps and time

core/federated/RTI/enclave.c

@@ -72,7 +72,10 @@ tag_advance_grant_t tag_advance_grant_if_safe(enclave_t* e) {
         // Ignore this enclave if it no longer connected.
         if (upstream->state == NOT_CONNECTED) continue;
 
-        tag_t candidate = lf_delay_tag(upstream->completed, e->upstream_delay[j]);
+        // Adjust by the "after" delay.
+        // Note that "no delay" is encoded as NEVER,
+        // whereas one microstep delay is encoded as 0LL.
+        tag_t candidate = lf_delay_strict(upstream->completed, e->upstream_delay[j]);
 
         if (lf_tag_compare(candidate, min_upstream_completed) < 0) {
             min_upstream_completed = candidate;
@@ -102,12 +105,13 @@ tag_advance_grant_t tag_advance_grant_if_safe(enclave_t* e) {
 
     // Find the tag of the earliest possible incoming message from
     // upstream enclaves.
-    tag_t t_d = FOREVER_TAG;
+    tag_t t_d_nonzero_delay = FOREVER_TAG;
     // The tag of the earliest possible incoming message from a zero-delay connection.
     // Delayed connections are not guarded from STP violations by the MLAA; this property is
     // acceptable because delayed connections impose no deadlock risk and in some cases (startup)
     // this property is necessary to avoid deadlocks. However, it requires some special care here
-    // when potentially sending a PTAG.
+    // when potentially sending a PTAG because we must not send a PTAG for a tag at which data may
+    // still be received over nonzero-delay connections.
     tag_t t_d_zero_delay = FOREVER_TAG;
     LF_PRINT_DEBUG("NOTE: FOREVER is displayed as " PRINTF_TAG " and NEVER as " PRINTF_TAG,
                    FOREVER_TAG.time - start_time, FOREVER_TAG.microstep,
@@ -131,16 +135,20 @@ tag_advance_grant_t tag_advance_grant_if_safe(enclave_t* e) {
         // Adjust by the "after" delay.
         // Note that "no delay" is encoded as NEVER,
         // whereas one microstep delay is encoded as 0LL.
-        tag_t candidate = lf_delay_tag(upstream_next_event, e->upstream_delay[j]);
+        tag_t candidate = lf_delay_strict(upstream_next_event, e->upstream_delay[j]);
 
-        if (lf_tag_compare(candidate, t_d) < 0) {
-            t_d = candidate;
-        }
-        if (lf_tag_compare(candidate, t_d_zero_delay) < 0 && e->upstream_delay[j] == NEVER) {
-            t_d_zero_delay = candidate;
+        if (e->upstream_delay[j] == NEVER) {
+            if (lf_tag_compare(candidate, t_d_zero_delay) < 0) {
+                t_d_zero_delay = candidate;
+            }
+        } else {
+            if (lf_tag_compare(candidate, t_d_nonzero_delay) < 0) {
+                t_d_nonzero_delay = candidate;
+            }
         }
     }
     free(visited);
+    tag_t t_d = (lf_tag_compare(t_d_zero_delay, t_d_nonzero_delay) < 0) ? t_d_zero_delay : t_d_nonzero_delay;
 
     LF_PRINT_LOG("Earliest next event upstream has tag " PRINTF_TAG ".",
             t_d.time - start_time, t_d.microstep);
@@ -162,6 +170,7 @@ tag_advance_grant_t tag_advance_grant_if_safe(enclave_t* e) {
         result.tag = e->next_event;
     } else if (
         lf_tag_compare(t_d_zero_delay, e->next_event) == 0      // The enclave has something to do.
+        && lf_tag_compare(t_d_zero_delay, t_d_nonzero_delay) < 0  // The statuses of nonzero-delay connections are known at tag t_d_zero_delay
         && lf_tag_compare(t_d_zero_delay, e->last_provisionally_granted) > 0  // The grant is not redundant.
         && lf_tag_compare(t_d_zero_delay, e->last_granted) > 0  // The grant is not redundant.
     ) {

core/federated/federate.c

@@ -1406,8 +1406,11 @@ void send_port_absent_to_federate(environment_t* env, interval_t additional_dela
     unsigned char buffer[message_length];
 
     // Apply the additional delay to the current tag and use that as the intended
-    // tag of the outgoing message
-    tag_t current_message_intended_tag = lf_delay_tag(env->current_tag,
+    // tag of the outgoing message. Note that if there is delay on the connection,
+    // then we cannot promise no message with tag = current_tag + delay because a
+    // subsequent reaction might produce such a message. But we can promise no
+    // message with a tag strictly less than current_tag + delay.
+    tag_t current_message_intended_tag = lf_delay_strict(env->current_tag,
                                                     additional_delay);
 
     LF_PRINT_LOG("Sending port "

core/tag.c

@@ -133,7 +133,7 @@ int lf_tag_compare(tag_t tag1, tag_t tag2) {
 }
 
 tag_t lf_delay_tag(tag_t tag, interval_t interval) {
-    if (tag.time == NEVER || interval == NEVER) return tag;
+    if (tag.time == NEVER || interval < 0LL) return tag;
     tag_t result = tag;
     if (interval == 0LL) {
         // Note that unsigned variables will wrap on overflow.
@@ -152,6 +152,16 @@ tag_t lf_delay_tag(tag_t tag, interval_t interval) {
     return result;
 }
 
+tag_t lf_delay_strict(tag_t tag, interval_t interval) {
+    tag_t result = lf_delay_tag(tag, interval);
+    if (interval != 0 && interval != NEVER && interval != FOREVER && result.time != NEVER && result.time != FOREVER) {
+        LF_PRINT_DEBUG("interval=%lld, result time=%lld", (long long) interval, (long long) result.time);
+        result.time -= 1;
+        result.microstep = UINT_MAX;
+    }
+    return result;
+}
+
 instant_t lf_time_logical(void *env) {
     assert(env != GLOBAL_ENVIRONMENT);
     return ((environment_t *) env)->current_tag.time;

include/core/tag.h

@@ -94,22 +94,41 @@ int lf_tag_compare(tag_t tag1, tag_t tag2);
 
 /**
  * Delay a tag by the specified time interval to realize the "after" keyword.
- * If either the time interval or the time field of the tag is NEVER,
- * return the unmodified tag.
- * If the time interval is 0LL, add one to the microstep, leave
- * the time field alone, and return the result.
+ * Any interval less than 0 (including NEVER) is interpreted as "no delay",
+ * whereas an interval equal to 0 is interpreted as one microstep delay.
+ * If the time field of the tag is NEVER or the interval is negative,
+ * return the unmodified tag. If the time interval is 0LL, add one to
+ * the microstep, leave the time field alone, and return the result.
  * Otherwise, add the interval to the time field of the tag and reset
- * the microstep to 0.
- * If the sum overflows, saturate the time value at FOREVER.
- *
- * Note that normally it makes no sense to call this with a negative
- * interval (except NEVER), but this is not checked.
+ * the microstep to 0. If the sum overflows, saturate the time value at
+ * FOREVER. For example:
+ * - if tag = (t, 0) and interval = 10, return (t + 10, 0)
+ * - if tag = (t, 0) and interval = 0, return (t, 1)
+ * - if tag = (t, 0) and interval = NEVER, return (t, 0)
+ * - if tag = (FOREVER, 0) and interval = 10, return (FOREVER, 0)
  *
  * @param tag The tag to increment.
  * @param interval The time interval.
  */
 tag_t lf_delay_tag(tag_t tag, interval_t interval);
 
+/**
+ * Return the latest tag strictly less than the specified tag plus the
+ * interval, unless tag is NEVER or interval is negative (including NEVER),
+ * in which case return the tag unmodified.  Any interval less than 0
+ * (including NEVER) is interpreted as "no delay", whereas an interval
+ * equal to 0 is interpreted as one microstep delay. If the time sum
+ * overflows, saturate the time value at FOREVER.  For example:
+ * - if tag = (t, 0) and interval = 10, return (t + 10 - 1, UINT_MAX)
+ * - if tag = (t, 0) and interval = 0, return (t, 0)
+ * - if tag = (t, 0) and interval = NEVER, return (t, 0)
+ * - if tag = (FOREVER, 0) and interval = 10, return (FOREVER, 0)
+ *
+ * @param tag The tag to increment.
+ * @param interval The time interval.
+ */
+tag_t lf_delay_strict(tag_t tag, interval_t interval);
+
 /**
  * Return the current logical time in nanoseconds.
  * On many platforms, this is the number of nanoseconds