Previous: Event ordering, Up: Event-driven Execution


6.2 Timing

The delays associated with each event are prefix delays, i.e. the delays are applied before the event is checked for the first time 1. In other words, every successor of an event that just executed is scheduled for future checking using the delay of each successor. When an event is checked for the first time, it is either blocked or executed immediately. When an event is blocked, it is subscribed to its dependencies (or some conservative superset thereof). When an event is unblocked, it is unsubscribed from its dependencies and placed into the immediate execution queue because it has already paid its delay up front, and thus should not be delayed further. The immediate execution queue contains only unblocked events that take precedence over the checking queue.


Footnotes

[1] One reason why a prefix-delay model was chosen was to facilitate the pseudo-atomic execution of send-receive event pairs. Pseudo-atomicity arises from the fact paired-events are still executed individually, but guaranteed to share the exact same timestamp. Had we chosen to use suffix or infix delays, delays would be applied after unblocking, resulting in potentially different timestamps.