Watchdogs don't work well with modes

[edwardalee]

It should be possible for a watchdog to be defined and used within a mode, but this does not currently work. The validator cannot resolve references to the watchdog, although I suspect this is only the first level problem. Test case:

/**
 * Test watchdog with modes.
 * @author Edward A. Lee
 */
target C

reactor Watcher(timeout: time = 1500 ms) {
  output d: int
  state count: int = 0

  initial mode NORMAL {    
    // Period has to be smaller than watchdog timeout. Produced if the watchdog triggers.
    timer t(1 s, 1 s)
    watchdog poodle(timeout) -> SILENT {=
      instant_t p = lf_time_physical_elapsed();
      lf_print("******** Watchdog timed out at elapsed physical time: " PRINTF_TIME, p);
      self->count++;
      lf_set_mode(SILENT);
    =}
    reaction(t) -> poodle, d {=
      lf_watchdog_start(poodle, 0);
      lf_print("Watchdog started at physical time " PRINTF_TIME, lf_time_physical_elapsed());
      lf_print("Will expire at " PRINTF_TIME, lf_time_logical_elapsed() + self->timeout);
      lf_set(d, 42);
    =}
    reaction(poodle) -> d {==}
  }

  mode SILENT { }
}

main reactor {
  state count: int = 0
  w = new Watcher()
  reaction(w.d) {=
    lf_print("Watcher reactor produced an output. %d", self->count % 2);
    self->count++;
    if (self->count % 4 == 0) {
      lf_print(">>>>>> Taking a long time to process that output!");
      lf_sleep(MSEC(1600));
    }
  =}

  reaction(shutdown) {=
    if (self->count > 4) {
      lf_print_error_and_exit("Watchdog produced output %d times. Expected no more than 4.", self->count);
    }
  =}
}

It should also be possible for a watchdog that is defined at reactor scope to have a handler that changes modes, but this also fails validation:

/**
 * Test watchdog with modes.
 * @author Edward A. Lee
 */
target C

reactor Watcher(timeout: time = 1500 ms) {
  output d: int
  state count: int = 0

  watchdog poodle(timeout) -> SILENT {=
    instant_t p = lf_time_physical_elapsed();
    lf_print("******** Watchdog timed out at elapsed physical time: " PRINTF_TIME, p);
    self->count++;
    lf_set_mode(SILENT);
  =}

  initial mode NORMAL {    
    // Period has to be smaller than watchdog timeout. Produced if the watchdog triggers.
    timer t(1 s, 1 s)
    reaction(t) -> poodle, d {=
      lf_watchdog_start(poodle, 0);
      lf_print("Watchdog started at physical time " PRINTF_TIME, lf_time_physical_elapsed());
      lf_print("Will expire at " PRINTF_TIME, lf_time_logical_elapsed() + self->timeout);
      lf_set(d, 42);
    =}
  }

  mode SILENT { }
}

main reactor {
  state count: int = 0
  w = new Watcher()
  reaction(w.d) {=
    lf_print("Watcher reactor produced an output. %d", self->count % 2);
    self->count++;
    if (self->count % 4 == 0) {
      lf_print(">>>>>> Taking a long time to process that output!");
      lf_sleep(MSEC(1600));
    }
  =}

  reaction(shutdown) {=
    if (self->count > 4) {
      lf_print_error_and_exit("Watchdog produced output %d times. Expected no more than 4.", self->count);
    }
  =}
}

[erlingrj]

How should watchdogs in modes behave? I think they have to follow the semantics of modal reactors. Consider a mode switch from First -> Second. Any watchdog in First will have to be "freezed". What happens in Second depends on the transition. A reset transition is easy, then the watchdog is not started, this will have to be done in a reaction within the mode. But a history transition is more tricky, should the watchdog consider the global logical time, or the local time in the mode? If we consider local time, then we might immediately get a watchdog timeout when we enable the watchdog again since local time is freezed when not in the mode. Also, I think it will be quite tricky to access this "local time" from our watchdog implementation.

If we consider global time then it is a little easier, but I am not sure it makes that much sense. The watchdog will then basically "guard" how much time is spent in another mode, but it will not trigger until finally the mode is entered again. Then it is too late to do anything anyway.

We could reject programs with history transitions to a mode with watchdogs. Or are there other use cases for it?

[edwardalee]

I have come to the (tentative) conclusion that we don't actually need watchdogs if we have enclaves. I think the watchdog can be effectively implemented using an enclave. So maybe we shouldn't worry too much about this.