The Upon language#

Upon is the language you write algorithms in. It follows the event-driven notation of Cachin, Guerraoui and Rodrigues closely enough that most textbook algorithms can be copied line by line, and it is strict enough to be checked and executed.

This page is the complete reference. If you have never written Upon, start with Getting started and come back here when you need a detail. The full grammar is in section 5.2 of the specification.

A first program#

interface Greeting
  request Greet(name)
  indication Greeted(from, name)
end

algorithm Hello
  implements Greeting as g
  uses Net as net

  upon event ⟨g, Greet | name⟩ do
    forall q in neighbors do
      trigger ⟨net, Send | q, [HELLO, name]⟩
    end
  end

  upon event ⟨net, Deliver | p, [HELLO, name]⟩ do
    trigger ⟨g, Greeted | p, name⟩
  end
end

Read it from the top:

• Greeting is an interface: it says what the algorithm accepts from above (Greet) and what it reports upwards (Greeted).
• Hello implements it under the local name g, and uses the network under the name net.
• The first handler reacts to a Greet request and sends a message to every neighbor.
• The second reacts to a message from the network. The pattern [HELLO, name] matches a tuple whose first element is the atom HELLO and binds the second to name.
• trigger sends an event: down to net, or up through g.

With the input line 0ms 1 Greet | "world", the neighbors of p1 report Greeted | 1, "world".

Lexical rules#

• Comments start with // and run to the end of the line, or sit between /* and */.
• Identifiers are letters, digits and underscores, starting with a letter or underscore. Case matters.
• Atoms are identifiers written in capital letters, at least two characters long, that are not declared as variables or parameters: HELLO, ACK, HEARTBEAT_REQUEST. They are symbolic constants, used mostly as message tags.
• Numbers are decimal: 3, 0.25, 1e-4.
• Durations are numbers followed by us, ms or s, with no space: 300us, 50ms, 2s. They become plain numbers of microseconds, so 50ms equals 50000.
• Strings are written between double quotes. A backslash takes the next character literally: "say \"hi\"".
• Line breaks do not matter. Statements are recognized by their first word. A semicolon between statements is allowed and ignored.

Keywords:

interface request indication algorithm implements as uses via params state stable
upon event where condition exists do end function return call
trigger if then elif else forall in while starttimer canceltimer assert log skip
and or not notin union inter minus subseteq true false nil

Interfaces#

interface Name
  request   EventName(param, param)
  indication EventName(param)
end

• A request travels from a module to the module below it.
• An indication travels from a module to the module above it.
• The parameter names are for documentation; only their number matters.
• An event with no parameters can be written Start() or Start.

Two interfaces, Net and Rounds, are predefined (see Provided modules). You cannot redefine or implement them.

Algorithms#

algorithm Name
  implements Interface as alias
  uses OtherInterface as other          // zero or more
  uses PerfectLinks as pl via AckLinks  // "via" picks the implementation
  params
    f := 1                              // evaluated once per process
  state
    seen := ∅                           // one copy per process
    stable total := 0                   // survives a crash and recovery
  function helper(x) … end              // zero or more, anywhere after state
  upon event ⟨alias, Init⟩ do … end     // handlers
end

implements names the interface this algorithm provides and the local name under which it receives requests and emits indications.

uses names an interface this algorithm relies on and the local name to talk to it. Each uses creates its own instance of the chosen algorithm.

params are constants. Their initial expressions can use built-in names and earlier parameters. They cannot be assigned.

state variables belong to each process. Their initial expressions can use built-in names and parameters. stable variables keep their value across a crash and a recovery; the others are reset (see Faults).

Every name in params and state must differ from the built-in names and from each other.

Handlers#

A handler runs when its trigger matches. There are three kinds.

Event handlers#

upon event ⟨instance, Event | pattern, pattern⟩ do … end
upon event ⟨instance, Event | pattern⟩ where condition do … end

instance is one of:

• the implements alias: the handler receives requests from above, or Init and Recovery;
• a uses alias: the handler receives indications from below;
• timer: the handler receives Timeout (see Timers).

When an event arrives, handlers are tried in the order they appear in the code. The first one whose patterns match and whose where condition is true runs; the others are skipped. If none matches, the event is ignored and a warning is logged once. Init, Recovery, RoundStart and RoundEnd without a handler are ignored silently.

A common idiom uses two handlers with opposite conditions:

upon event ⟨net, Deliver | p, [DATA, m]⟩ where m ∉ seen do … end
upon event ⟨net, Deliver | p, [DATA, m]⟩ where m ∈ seen do skip end

Condition handlers#

upon condition expression do … end

The handler runs whenever the expression is true, checked after every step of the process. Its body must make the condition false, directly or indirectly; a condition that stays true forever stops the run with an error.

Exists handlers#

upon exists x in collection where condition do … end

The handler runs for the first element of the collection, in sorted order, that satisfies the condition, with that element bound to x. It is checked after every step, like a condition handler, and is the natural way to write "when some pending message can be delivered":

upon exists e in pending where e[1] = next do
  pending := pending \ {e}
  next := next + 1
  trigger ⟨app, Deliver | e[0], e[2]⟩
end

When several condition or exists handlers of a module are enabled, they take turns.

Patterns#

Patterns appear in event handlers, one per event parameter.

The same new name used twice must match equal values: ⟨net, Deliver | p, [ECHO, p]⟩ only matches when the message echoes its own sender.

In ⟨timer, Timeout | t⟩, t is the name of a timer, not a variable (see Timers).

Statements#

Local variables. Assigning a name that is not a state variable creates a local variable, visible until the end of the handler or function. Reading it before the assignment is a runtime error. Loop variables and pattern variables are local too.

Triggers are asynchronous within the process. trigger puts the event in a queue; it is handled after the current handler finishes, within the same step. Code after a trigger does not see the effects of the event.

forall evaluates the collection once, before the loop starts. Assigning the collection inside the loop does not change the iteration.

assert does not stop the run unless Stop at the first failed assertion is checked in the Scenario tab.

log prints strings as they are and other values in their written form, separated by spaces.

Expressions#

From lowest to highest precedence:

Comparisons do not chain: write a < b and b < c, not a < b < c. To compare the result of a membership test, use parentheses: (x ∈ S) = false.

and and or are short-circuit and require booleans. if, while, where and conditions also require booleans; there is no truthiness.

Literals:

Values#

All values are immutable. m[k] := v builds a new map and assigns it to m, so a copy taken earlier (old := m) does not change.

Values of different kinds are ordered as in the table: nil before booleans, booleans before numbers, and so on. Within a kind the order is the natural one; tuples, sets and maps compare element by element. This total order is what makes min, max, sort, choose and set iteration deterministic.

Process identifiers are numbers: self is 3 on process p3.

Built-in names#

Π contains every process, including those without a link to this one. Sending to a process that is not a neighbor drops the message.

Built-in functions#

Collections

Sequences (a set is treated as its sorted tuple)

Numbers

Other

The logarithm is ln, because log is the statement that writes to the event log.

Functions#

interface Stats
  request Add(x)
  indication Summary(count, average, spread)
end

algorithm Collector
  implements Stats as s
  uses Net as net
  state
    samples := []

  function average()
    return mean(samples)
  end

  // standard deviation; mean() divides exactly, while "/" between
  // two whole numbers would truncate
  function spread()
    a := average()
    squares := []
    forall x in samples do
      squares := append(squares, pow(x - a, 2))
    end
    return sqrt(mean(squares))
  end

  function record(x)
    samples := append(samples, x)
    trigger ⟨s, Summary | #samples, average(), spread()⟩
  end

  upon event ⟨s, Add | x⟩ do
    call record(x)
  end
end

A function:

• belongs to one algorithm and can be called only from that algorithm;
• sees the algorithm's state, parameters and built-in names, but not the local variables of its caller;
• has its own local variables, starting with its parameters;
• may assign state, trigger events and start timers, exactly like a handler;
• returns the value of the first return it executes, or nil if it reaches the end;
• may call itself and other functions, up to 200 nested calls.

Use a function in an expression, x := average(), or as a statement with call record(x). call is only for your own functions; built-in functions are used in expressions.

A function name cannot be the name of a built-in function.

Timers#

starttimer(retry, 200ms)       // start, or restart, the timer named "retry"
canceltimer(retry)             // cancel it
upon event ⟨timer, Timeout | retry⟩ do … end

• Timer names are plain identifiers, local to the module. They are not variables.
• Starting a timer that is already running restarts it; only the latest start fires.
• The duration is measured on the process's local clock, so drift changes the real duration slightly.
• In the Timeout handler, the pattern is the timer's name. ⟨timer, Timeout | _⟩ catches every timer of the module.
• A recovery cancels every timer.
• Timers are not available with lockstep rounds; use RoundStart and RoundEnd there.

The checker warns about a Timeout handler for a timer the module never starts.

Writing help#

The editor knows the program you are writing, so it can offer what exists rather than what might:

• Completion. Inside ⟨ … ⟩ it offers the instances of the algorithm you are in, then the events of that instance's interface, with their number of arguments. Elsewhere it offers state variables, parameters, functions, built-ins and keywords. It appears as you type a name, or on Ctrl + Space; ↑ ↓ choose, Enter or Tab accept, Esc closes. While an algorithm is half-written and does not parse yet, the instances are read from the header you have already typed.
• Quick fixes. A diagnostic that has an obvious repair offers it as a button: declare it in state for an undeclared variable, add the handler for an indication nobody handles, with the right arguments filled in, and add a module that implements it for an interface with an implementation in the library. The fix edits the code and runs the checker again, so nothing is applied that the checker would reject.

Properties#

A property is a global invariant: one boolean expression over the state of every process, checked by the engine. It lives at the top level of the program, next to interfaces and algorithms.

interface Consensus
  request Propose(v)
  indication Decide(v)
end

algorithm Simple
  implements Consensus as c
  uses Net as net
  state
    proposal := nil
    decision := nil

  upon event ⟨c, Propose | v⟩ do
    proposal := v
    decision := v
    trigger ⟨c, Decide | v⟩
  end
end

property Agreement always
  #toset(values(defined(decision))) ≤ 1
end

property Validity always
  #{p in keys(defined(decision)) where decision[p] ≠ proposal[p]} = 0
end

property Termination eventually
  keys(defined(decision)) = correct
end

Inside a property, a state variable is a map from process to its value on that process, taken from the main algorithm. decision above is {1 ↦ 7, 2 ↦ nil, 3 ↦ 7}, so values(decision) are the values across the system and defined(decision) keeps only the processes where the variable is not nil. Everything else is the ordinary expression language.

Besides state variables, a property can use:

A property cannot use self, neighbors, round, DELTA, PHI, RHO, now(), random or pick: it looks at the whole system from outside, at one moment, and must not depend on chance. Only built-in functions are available; the functions of an algorithm are not.

What the engine reports. Each property ends the run as held or broken, with the instant and the process whose step made it fail. Broken properties appear in the event log under the Properties filter, are counted next to the other chips, and are listed by the command line tool. Setting haltOnProperty in the scenario stops the run at the first violation.

Limits worth knowing.

• Properties see the state of the main algorithm only. To observe a module further down the stack, expose what you need in the main algorithm.
• eventually can only say "it did not happen before the run ended". A longer simulated duration may change the answer; this is a check, not a proof. See Assumptions and simplifications.
• A property is evaluated after every step, so a long run with several properties costs noticeably more than the same run without them.
• A property that is not a boolean, or that fails with a runtime error, is reported as broken with its error, and the run continues.

Provided modules#

Net#

interface Net
  request Send(q, m)
  indication Deliver(p, m)
end

Send(q, m) sends m to process q over the link between them. Deliver(p, m) reports a message m from p. The network behaves as the actual model says: it can lose, duplicate, delay and reorder messages. See The timing model.

Net is available with every synchrony model except synchronous rounds.

Rounds#

interface Rounds
  request Send(q, m)
  indication RoundStart(r)
  indication Deliver(p, m)
  indication RoundEnd(r)
end

In each round, a module that uses Rounds receives RoundStart(r), then the messages of that round, then RoundEnd(r). Send in RoundStart, collect in Deliver, decide in RoundEnd. The built-in round holds the current round number.

Rounds is available only with synchronous rounds. How rounds are executed is described in The timing model.

timer#

timer is not declared with uses: every module has it. It produces only Timeout(t).

Composing modules#

A program can contain several algorithms. The Main algorithm selector in the Code tab chooses the top one; its interface defines the inputs you can send and the outputs you see.

For each uses X as a, the playground creates an instance of an algorithm that implements X:

• with via Y, the algorithm Y, which must implement X;
• otherwise, the first algorithm in the code that implements X. If there are several, a warning tells you which one was chosen.

Instances form a tree, one per process. Every uses creates its own instance, so two modules that use PerfectLinks get two independent copies with separate state.

A module talks only to its direct neighbors in the tree: it sends requests to the modules it uses and indications to the module that uses it. It never sees their state.

interface PerfectLinks
  request Send(q, m)
  indication Deliver(p, m)
end

interface Echo
  request Ping(q)
  indication Pong(p)
end

algorithm DirectLinks
  implements PerfectLinks as pl
  uses Net as net
  upon event ⟨pl, Send | q, m⟩ do
    trigger ⟨net, Send | q, m⟩
  end
  upon event ⟨net, Deliver | p, m⟩ do
    trigger ⟨pl, Deliver | p, m⟩
  end
end

algorithm Pinger
  implements Echo as e
  uses PerfectLinks as pl via DirectLinks
  upon event ⟨e, Ping | q⟩ do
    trigger ⟨pl, Send | q, [PING]⟩
  end
  upon event ⟨pl, Deliver | p, [PING]⟩ do
    trigger ⟨pl, Send | p, [PONG]⟩
  end
  upon event ⟨pl, Deliver | p, [PONG]⟩ do
    trigger ⟨e, Pong | p⟩
  end
end

Ready-made modules for links and broadcast are in the module library.

What the checker verifies#

The checker runs while you type and again before every run. Errors stop the run; warnings do not.

Errors

• Syntax errors, with line and column.
• An interface used or implemented but not declared; implementing Net or Rounds; two algorithms or interfaces with the same name.
• Rounds without the synchronous rounds model, or Net with it.
• DELTA, PHI or RHO when unknown in the assumed model; round outside the rounds model; now() or starttimer in lockstep rounds.
• A variable that is not declared, not a parameter, not a built-in and not an atom.
• An assignment to a parameter or a built-in name; a state variable or parameter named like a built-in.
• A trigger to an unknown instance, an indication sent downwards, a request sent upwards, or the wrong number of arguments.
• A handler for an event that the instance cannot produce, or with the wrong number of patterns; Init or Recovery with patterns; a timer handler for anything but Timeout(t).
• An unknown function, a call with the wrong number of arguments, call with a built-in function, return outside a function, a function with a built-in's name or a repeated parameter.
• In a property: two properties with the same name, a name that is not a state variable of any algorithm, and the names and functions that a property may not use.
• uses … via Y where Y does not exist or implements another interface; via with Net or Rounds.

Warnings

• An indication of a used module that no handler receives (its events will be ignored).
• A Timeout handler for a timer the module never starts.
• Timers in lockstep rounds.
• Several algorithms implementing an interface used without via.

Runtime errors#

Some problems can only be found while running. The run stops, keeps everything up to that point, and shows the line in the editor.

• A value of the wrong kind: Expected a boolean, found number (3).
• An index outside a tuple, an indexed assignment on something that is not a map or tuple.
• Division by zero.
• min, max, choose, pick, head, last, mean, argmin or argmax of an empty collection.
• sqrt of a negative number, ln of a number that is not positive.
• A local variable read on a path where it was never assigned (Variable "x" is not defined).
• More than 200 nested function calls, more than 100,000 iterations of a while loop, more than 200,000 statements or 20,000 internal events in one step, a guard that stays true.

ASCII syntax#

Every symbol has a plain-text spelling, and you can mix both.

With ASCII angle brackets, > inside a trigger would close the event. Wrap comparisons in parentheses there:

trigger <app, Result | (x > 3)>

The symbol buttons above the editor insert the Unicode characters at the cursor.

Common mistakes#

A handler never runs. Handlers are tried in order and only the first match runs. An earlier, more general handler may be catching the event. Put the specific one first, or add where clauses.

"Variable is not declared" for a message tag. Atoms need at least two capital letters: A is a variable name, AB is an atom.

A tag matches a variable instead. If a state variable is called DATA, the pattern [DATA, m] compares with its value instead of the atom. Use lower-case names for variables.

5 / 2 gives 2. Division between two whole numbers truncates, and a value such as 4.0 counts as whole. Use mean for averages, or multiply first (100 * a / b) when you need a percentage.

Nothing arrives. The recipient may not be a neighbor; check the topology, or look for no link in the event log.

A broadcast reaches only some processes. Library broadcast modules send to every process in Π, which requires a complete graph.

A guard stops the run. An upon condition handler must make its condition false. If it only sends a message, it will fire again at once.

An algorithm works but depends on the order of a set. Sets are iterated in sorted order and choose is deterministic here. Real systems give no such guarantee; try pick to see whether the algorithm still works.