How does the past() function work?

[Andrew Helwer]

The "It's About Time" slide had to be skipped due to time constraints during the talk at CoreOS Fest, but if you pause the video you can read some stuff about the past() function - it's some way of accessing a global clock? I can't find anything about it in the language guide.

The past() function is used in a bunch of places in the Raft spec. What's going on with this function? Is it some way of introducing temporal logic statements into Runway?

Thanks!

[Diego Ongaro]

Hey Andrew,

Yes, past() is a conditional way of accessing the global clock in simulations. You can run the simulator in two modes of operation: synchronous, which generates events over time, and asynchronous, which generates only an ordered sequence of events. Too Many Bananas is asynchronous (doesn't use the clock at all), the Elevators are pretty much only interesting synchronously (to measure timing delays). The Raft model can be run in either mode.

If I may quote an article I've been writing:

Many algorithms are designed to maintain safety properties under asynchronous assumptions, making them robust to erroneous clocks and unexpected delays (typically, even a "small" race condition is not acceptable). With Runway, it's possible to check these properties asynchronously with the model checker, and still run timing-based simulations on the same model. For example, we can check that Raft always keeps committed log entries no matter how long communication steps take, then use the same model in synchronous mode to estimate leader election times on a datacenter network.

In Runway, a timer is typically modeled by storing the time when an action should be taken, then guarding a transition rule for the action with an if-statement: 

 

rule fireTimer {
  if past(timeoutAt) {
    /* take action, reset timeoutAt */
  }
}

When running in synchronous mode, Runway keeps a global clock for the simulation, and past() evaluates to true if the given timestamp is earlier than the simulation's clock. In asynchronous mode, however, past() always returns true. This has the effect of making all timers fireable immediately after they are scheduled, allowing unlikely schedules to be explored.

This worked pretty well for the Raft model, though I'm a bit worried it may be too simplistic for modeling other systems. I guess we'll find out over time.

So, past() is just about accessing the clock, not about temporal logic. It's a bit special in the language to allow the simulator to easily skip clock ticks that aren't interesting. If the next rule will become active past(2000), and the current clock is at 10, Runway can skip over 11, 12, 13, ..., and jump the clock right to 2000.

There's a related function later(delta) that returns `clock + delta`. It's just there so you don't get used to accessing clock directly for conditional checks where you should be using past(). That's a bit ugly, and I'm certainly open to ideas.

Best,

Diego

--
You received this message because you are subscribed to the Google Groups "runway-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to runway-dev+...@googlegroups.com.
To post to this group, send email to runwa...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/runway-dev/a8ea5a1d-7eab-4c1a-b8e6-e10f0a8d6fd1%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.