Timers

Timers#

Many protocols react to time passing: a client sends a request again if no reply arrives within a few seconds, a peer sends a keepalive after a period of silence, and a session expires after some minutes. To test such interactions, a Fandango spec can start and cancel timers and react to them expiring.

Added in version 1.2: Timers are available in Fandango 1.2 and later.

Timer Parties#

Fandango models timers as two predefined parties:

  • TimerControl receives the commands from Fandango to start and cancel timers.

  • TimerEvent reports that a timer has expired. Like a remote party, it is not controlled by Fandango; its messages arrive on their own.

Both classes are predefined within .fan files; they need not be imported.

The messages are defined in the standard library:

Message

Party

Symbol

Format

Start a timer

TimerControl

<timer_start>

start: ID (SECONDS)\n

Cancel a timer

TimerControl

<timer_cancel>

cancel: ID\n

A timer expired

TimerEvent

<timer_expired>

expired: ID\n

ID (<timer_id>) is a number that identifies the timer. SECONDS (<timer_timeout>) is the duration of the timer in seconds, such as 5 or 0.25.

A First Timer#

Here is a spec that starts a timer, waits for it to expire, and then prints a message:

<start> ::= <TimerControl:wait_start> <TimerEvent:wait_expired> <StdOut:done>
<wait_start> ::= <timer_start>
<wait_expired> ::= <timer_expired>
<done> ::= 'Timer expired\n'

where str(<wait_start>..<timer_id>) == '1'
where str(<wait_start>..<timer_timeout>) == '0.5'
where str(<wait_expired>..<timer_id>) == '1'

The rules <wait_start> and <wait_expired> give the timer messages names of their own, so that the constraints can set them to timer 1 and half a second. Running this spec with the talk command prints the message after half a second:

$ fandango talk -f timer.fan -n 1

Timer expired

Waiting for a Reply#

The typical use of a timer is to limit how long to wait for a reply. The following spec sends PING to a program and starts a timer of one second. If the program answers in time, Fandango cancels the timer; otherwise, the timer expires:

<start> ::= <In:request> <TimerControl:reply_start> <reply>
<reply> ::= <Out:response> <TimerControl:reply_cancel> | <TimerEvent:reply_expired>
<request> ::= 'PING\n'
<response> ::= 'PING\n'

<reply_start> ::= <timer_start>
<reply_cancel> ::= <timer_cancel>
<reply_expired> ::= <timer_expired>

where all(str(<t>..<timer_timeout>) == '1' for <t> in *<reply_start>)
where all(str(<s>..<timer_id>) == '1' for <s> in *<reply_start>)
where all(str(<c>..<timer_id>) == '1' for <c> in *<reply_cancel>)
where all(str(<e>..<timer_id>) == '1' for <e> in *<reply_expired>)

The constraints use all(...) since a symbol such as <reply_cancel> need not occur in a run, or may occur several times.

Against cat, which echoes its input, the reply arrives and the timer is cancelled. With -v, Fandango logs the messages exchanged:

$ fandango -v talk -f timer-reply.fan -n 1 cat

fandango:INFO: In: <request> 'PING\n'

Against a program that never answers, the timer expires:

$ fandango -v talk -f timer-reply.fan -n 1 sh -c 'sleep 3'

fandango:INFO: In: <request> 'PING\n'
fandango:INFO: TimerControl: <reply_start> 'start: 1 (1)\n'
fandango:INFO: TimerEvent: <reply_expired> 'expired: 1\n'

To try again after a timeout, let the expiry lead back to the request, as in

<exchange> ::= <In:request> <TimerControl:reply_start> <reply>
<reply> ::= <Out:response> <TimerControl:reply_cancel> | <TimerEvent:reply_expired> <exchange>

How Timers Behave#

  • Starting a timer whose ID is running restarts it with the new duration.

  • A cancelled timer does not expire. If it has already expired but its expiry has not been handled yet, cancelling drops the expiry.

  • An expiry is handled only where the grammar allows a TimerEvent message next. Until then, it waits.

  • While Fandango waits for a message and the grammar allows an expiry next, there is no time limit. Hence, a spec should only expect expiries of timers it has started.

  • At the end of a run, all timers are stopped.

Tip

Use one ID per timer of the protocol, and constants in the spec for the IDs and durations. The WireGuard spec runs six timers this way, for handshakes, keepalives, and rekeying.