Skip to main content
PRL Project

3 Simple examples

We guide the reader through the features of this new programming/specification language with a series of examples.

3.1 Ping-pong


specification ping_pong 
 
(* ------ Imported Nuprl definitions ------  *) 
import bag-map 
 
(* ------ Protocol parameters ------ *) 
parameter p : Loc 
parameter locs : Loc Bag 
 
(* ------ Interface ------ *) 
input    start : Loc 
internal ping  : Loc 
internal pong  : Loc 
output   out   : Loc 
 
(* ------ Classes ------ *) 
class ReplyToPong (client,loc) = 
  let F _ l = if l = loc then {out’send client loc} else {} 
  in Once(F o pong’base) ;; 
class SendPing (_,loc) = Output(\l.{ping’send loc l}) ;; 
class Handler (c,l) = (SendPing (c,l) || ReplyToPong (c,l)) ;; 
 
class Delegate = (\_.\client.bag-map (\l.(client,l)) locs) o start’base;; 
class P = Delegate >>= Handler;; 
 
class ReplyToPing = (\loc.\l.{pong’send l loc}) o ping’base ;; 
 
(* ------ Main class ------ *) 
main P @ {p} || ReplyToPing @ locs

Figure 1: Ping-pong protocol


Consider the following problem: a client wants to run some computation that involves a certain collection of nodes, but first wants to know which of them are still alive. To learn that, the client initiates the (trivial) ping-pong protocol, which will “ping” the nodes and tell the client which nodes respond to the ping. (This simple protocol does not deal with the fact that nodes can fail after responding.)

An EventML specification requires only that the declaration of an identifier precede its use. For readability, however, a specification is typically presented in the following order: name; imports (from a library); parameters; messages; variables; class declarations. Most of these parts are optional. Fig.1 presents the full EventML specification of the protocol.

Specification name

The keyword specification marks a specification’s name:

specification ping_pong

Imports

EventML provides a library file that is a snapshot of Nuprl’s library. The types in EventML are a subset of the types in Nuprl. Accordingly, any library function whose type is an EventML type can be used in EventML program. An import declaration makes library functions visible:

import bag-map

The bag-map operation applies a function, pointwise, to all elements of a bag:

bag- map f {a,b,... } = {(f a),(f b),... }

Parameters

To avoid hardwiring the locations of any participants into the specification, we declare two parameters: p is the location to which clients send their requests; locs is a (non-repeating) bag containing the locations of the nodes to be checked. To execute the protocol we will instantiate those parameters as real physical machine addresses. 1As a logical matter, an EventML program may have parameters of any type definable in EventML. To compile an EventML specification, a developer must supply a configuration file that instantiates the parameters. See section 8. A client will identify will include its location in the request it sends, as a return address for replies.

parameter p : Loc 
parameter locs : Loc Bag

Messages and directed messages

The ping-pong protocol uses four kinds of messages:

input    start : Loc 
internal ping  : Loc 
internal pong  : Loc 
output   out   : Loc

Each of these lines declares a message kind. The elements of a message declaration

  • identify its category, using one of the keywords input, output, internal

    input messages are generated by sources outside the protocol; output messages are generated by the protocol and consumed by outside sources; internal messages are produced and consumed (only) by the protocol.

  • provide a (user-chosen) name for the message kind (in this case, start, ping, pong, or out)
  • specify the type of the message body (in this case, the contents of every message exchanged in the protocol is a location).

The body of a ping or pong message will not, in fact, be an arbitrary location; it must be one of the locations in locs. However, we cannot formulate that more precise declaration of these message kinds because EventML does not allow subtype definitions (though Nuprl does).

Our discussions will use the notation [start : x] to denote a start message with body x, etc. 2For technical reasons, the Nuprl model represents a message as a triple: a list of tokens acting as a message header, the message body, and the type.

A directed message is a pair consisting of a location (the addressee) and a message. Our discussions will use the notation (loc,msg) to denote the directed message that addresses message msg to location loc. Directed messages have a special semantics. When a main class (see below) produces a bag of directed messages, a messaging system attempts to deliver them—i.e., given the directed message (loc,msg), the messaging system attempts to deliver msg to location loc. We reason about the effect of a protocol under assumptions about message delivery. For present purposes, we assume that all messages are eventually delivered at least once, but make no assumption about transit times or the order in which messages are delivered.

Message declarations automatically introduce certain operations and event classes:

  • Every declaration of an input or internal message kind foo automatically introduces a base class, denoted foo’base, an event class that recognizes the arrival of a foo message and observes its body (and recognizes messages of no other kind).

    More precisely, the arrival of a message [foo : msg ] at location l, causes an event e to happen at l; and when e occurs, foo’base observes the content of that message. (Equivalently, we say that foo’base returns {msg}; or we say that v foo’base (e) if and only if v = msg .)

  • Every declaration of an output or internal message kind foo automatically introduces functions foo’send and foo’broadcast that are used to construct directed messages or bags of them. (These are the only way to construct such messages—thus, we assume that the messages they construct cannot be forged.)

    If l is a location and msg is of the appropriate type

    (foo’send l msg ) = (l,[foo : m])

    the directed message for sending [ foo : m] to l.

    If the li are locations and msg is of the appropriate type

    foo’broadcast {l1,...,ln} msg = {(l1,[foo : msg]),...,(ln,[foo : msg ])}

    a bag of directed messages containing a [ foo : msg ] message for each location li .

Ultimately, all EventML programs are defined by applying combinators to base classes, which are the only primitive classes.3Technically, this is not quite true: It would be possible to define an event class in the Nuprl library and import it into an EventML program. We assume that any computing system on which we wish to implement EventML provides the means to implement base classes.

The protocol

The ping-pong protocol proceeds as follows:

  1. It begins when a message of the form [ start : client ] arrives at location p . (Replies to this message will be sent to client.)
  2. A supervisory class, P, will then spawn several classes at location p. For each l in locs, it spawns the class Handler(client,l), which will handle communications with node l.
  3. Handler(client,l) sends a [ ping :p ] message to the node at location l and waits for a response.
  4. On receipt of a [ ping :p ] message, the ReplyToPing class at node l sends a [ pong : l] message back to p.
  5. On receipt of this [ pong : l] message, Handler (client ,l) sends an [ out : l] message to client and terminates.

Intuitively, Handler is a parameterized class—but, because EventML is a higher-order language, we need no special generic or template construct in order to express that. An event class parameterized by values of type T is simply a function that inputs values of type T and outputs event classes.

Class combinators

Our specification uses the following class combinators, all of them provided in the standard library:

  • Output(f): If f : Loc Bag (T), Output(f) is the class that, in response to the first event it sees at location l, returns the bag of values ( f  l); it then terminates.
  • X || Y: This event class is the parallel composition of classes X and Y. It recognizes events in either X or Y, and observes a value iff either X or Y observes it. The parallel combinator is a primitive.
  • X >>= Y: This is the delegation, or bind, combinator.4The class type forms a monad and delegation is the bind operator of that monad. If X is an event class and Y is a function that returns event classes, X >>= Y is the event class that, whenever it recognizes an event, acts as follows: For each v X (e), it “spawns” the class (Y v). (Events in this spawned class will occur at the same location as e and causally after it. We temporarily defer a more precise discussion of its meaning.) Delegation is primitive.
  • f o X: This is well typed if f is a function that takes as arguments a location and a value, and returns a bag. It acts as follows (for the case of a single-valued class): when v X (e)and NUPRLevent has location loc, f o X returns ( f  loc  v). This simple composition combinator is “almost primitive.” It is defined in terms of a primitive combinator that is somewhat more expressive but rarely, if ever, used. (This combinator is described in more detail in the discussion, below, of class ReplyToPong.)
  • Once(X): This class responds only to the first X-event at any location and, at such an event, behaves like X. That is, v ( Once(X) )(e) iff v X (e) and there was no X -event prior at location loc (e) prior to e. Once is a defined combinator that our compiler treats specially, because it knows that the process Once(X) can be killed and cleaned up after it has recognized one event.
  • X@b: This is the restriction of X to the locations in the bag b: v (X@b) (e) iff e occurs at a location in b and v X (e). Operationally, it means “run the program for X at each location in b .”

The “main” class

The keyword main identifies the event class that compilation of an EventML specification will actually implement (given appropriate instantiations of its parameters). The main program of the ping-pong program is the parallel composition of the supervisory class P running at location p and ReplyToPing running at all the locations in locs:

main P @ {p} || ReplyToPing @ locs

Spawning of handlers (delegation to sub-processes)

The supervisory class P uses the delegation combinator to spawn a handler for each request.

class P = Delegate >>= Handler;;

We will define Delegate so that, in response to [ start : x], returns the bag {(x,l1),(x,l2),...} , where the li are the elements of locs. Each element of this bag is the initial data needed by one of the spawned classes. The effect of Delegate >>= Handler is therefore to spawn a class (Handler (client,li)) for each i. Notice how the types match up: Delegate is an event class of type Loc * Loc; Handler will be a function mapping values of type Loc * Loc to event classes of type directed message. Therefore Delegate >>= Handler is an event class that returns (bags of) directed messages.

Consider the definition of Delegate, which we’ve rewritten by introducing the locally defined function f.

class Delegate = 
   let f = \client.bag-map (\l.(client,l)) locs in 
      (\_.f) o start’base ;;

The “_” is used, as in ML, as the name of a variable whose value is ignored.

When a [ start : x] message arrives, we want Delegate to return the bag

f x = {⟨x,l1⟩,⟨x,l2⟩,...}

where locs = {l1,l2,}. Intuitively, the simple composition operator transforms observed values by applying a function. However, the function we use is not f but \_.f. The reason is that the location of an event is also observable; accordingly, we define “g o X” so that that g takes two arguments: the location of the event and a value observed by X. It so happens that in this case, the location is ignored. We give a precise definition of this combinator at the end of this section.

Handler

Interactions betwen the Handler classes spawned by P and the nodes carry out steps (3)–(5) of the protocol. The input to the higher-type function Handler is a pair of locations: the client location and the location to ping. The resulting handler is the parallel composition of two other parameterized classes: SendPing, which executes step (3) of the protocol, and ReplyToPong, which executes step (5).

class Handler (c,l) = (SendPing (c,l) || ReplyToPong (c,l)) ;;

By the definition of the parallel combinator, Handler (c,l) computes everything that either SendPing (c,l) or ReplyToPong (c,l) does.

SendPing (c,l) is in charge of only one task: send a ping message to l.

class SendPing (_,loc) = Output(\l.{ping’send loc l}) ;;

By the definitions of Output and ping’send given above, an instance of SendPing(client,loc) running at location l will respond to the first event it sees at l by directing a ping message with body l to location loc; it will then terminate. The recipient will interpret l as a return address.

ReplyToPong (client,loc) waits for a pong message from the node at location loc and, on receiving one, sends [ out : l] to location client . It therefore responds to a subset of the events recognized by the base class pong’base: not every pong message, but only those sent from loc, i.e., those whose message body is loc. If v pong’base (e), ReplyToPong generates an output by applying the following function to v:

    \l.if l = loc then {out’send client loc} else {}

and then terminates. This is the essence of the locally defined function F in

class ReplyToPong (client,loc) = 
  let F _ l = if l = loc then {out’send client loc} else {} 
  in Once(F o pong’base) ;;

Once again, because the response doesn’t depend on the location at which the input event occurred, the first argument to F is a dummy.

ReplyToPing

ReplyToPing defines a program that must run at each node that will be pinged.

class ReplyToPing = (\loc.\l.{pong’send l loc}) o ping’base ;;

This time the transformation function makes use of the initial location argument. When the class ((\loc.\l.{pong’send l loc}) o ping’base), running at location s, receives [ ping : l] it sends [ pong : s] to location l.

Programmable classes

No base class can be a main program. For example, start’base recognizes the arrival of every start message at any node whatsoever; but this abstraction cannot be implemented: we cannot install the necessary code on every node that exists (whatever that may mean). However, start’base is locally programmable in the sense that we can implement any class that results from restricting it to a finite set of locations. All base classes are locally programmable and all primitive class combinators preserve the property of being locally programmable, so every class definable in an EventML program is locally programmable.5This needs a qualification: One could define a class in Nuprl that is not locally programmable and then import it from the Nuprl library; one could similarly introduce a pathological combinator. If that is done, the first step of compilation—verifying that the main program is programmable—would fail.

A class is programmable if it is equivalent to the restriction of a locally programmable class to a finite set of locations. Declaring a class as a main program incurs the obligation to prove that it is programmable. Using the “__@__” combinator, and the fact that primitive combinators also preserve the property of being programmable, we can automatically prove that any idiomatically defined main program is programmable.

Simple composition, in detail

One can apply simple composition to any number of classes. Given n classes X1, …, Xn, of types T1, …, Tn respectively, and given a function F of type Loc T1 ⋅⋅⋅ Tn Bag(T), one can define a class C : Class(T) by C = F o (X1,⋅⋅⋅,Xn).

Intuitively, C processes an event e as follows. The first argument supplied to F is the location at which e occurs; the successive arguments are, in order, the values observed by the classes Xi at e; and C returns the bag that F computes from these inputs. That description leaves it unclear what to do if, for some i, e is not an Xi-event, or what to do if for some i, Xi produces a bag with more than one element.

Here is a more precise formulation. C produces (observes) the element v of type T iff each class Xi observes an element vi of type Ti at event e and v = f  loc(e) v1 ⋅⋅⋅ vn. Therefore, a C-event must be an Xi-event for all i ∈{1,,n}. If for some i ∈{1,,n}, Xi does not observe anything at event e, then neither does C.

3.2 Ping-pong with memory

We now make our ping-pong protocol a bit more interesting by adding some memory to the main process. We introduce a new integer parameter, threshold; instead of sending an [ out : l] message to the client whenever node l responds to a pong, we wait until a total of threshold responses have been received, and then notify the client by sending a message [ out : [l1 ; l2 ; ; lthreshold ] ], whose body is the list of all responders. We modify the design of ping-pong by adding one more (parameterized) class, a memory module: Instead of sending an out message directly to a client, ReplyToPong will send an alive message to an appropriate memory module, which will accumulate responses and send an out message to the client once it has received enough of them.

And we add one more twist. A client who sends multiple start messages will receive multiple out messages in reply and may need to know what request any out message is replying to. So the client will attach an integer id (we will call it a request number) to its start messages; that request number will be included in the out message it receives. The request numbers need not be globally unique identifiers, so we will also arrange for the supervisory class P to attach a global id (which we will call a round) to each request that it receives. The protocol proceeds as follows:

  1. P receives a [ start : client, req_ num] message from the location client .
  2. P generates a unique id, round, for the request and spawns the following:
    • for each node l in locs, a class Handler(l,round)
    • a memory module ( Mem  client  req_ num  round )
  3. Handler(l,round) sends a [ ping : p , round] message to the node at location l and waits for a reply.
  4. On receipt of [ ping : p , round] the ReplyToPing class at node l sends a [ pong : l , round] message to p . Handler classes respond to pong messages.
  5. On receipt of [ pong :l, round], the class Handler (l, round ) sends an [ alive :l, round] message to itself (location p). Mem classes respond to alive messages.
  6. When (Mem client req_num round) has seen alive messages from threshold distinct locations, it sends to location client an appropriate out message tagged with req_num.

Fig. 2 provides the full specification of this protocol. Most of it is a routine adaptation of the ping-pong specification. The novelty lies in the introduction of the event classes PState and Mem that act like state machines. We will describe these in detail.


specification m_ping_pong 
 
(* ------ Imported Nuprl declarations ------ *) 
import bag-map deq-member length 
 
(* ------ Parameters ------ *) 
parameter p         : Loc 
parameter locs      : Loc Bag 
parameter threshold : Int 
 
(* ------ Interface ------ *) 
input    start : Loc * Int 
internal ping  : Loc * Int 
internal pong  : Loc * Int 
internal alive : Loc * Int 
output   out   : Loc List * Int 
 
(* ------ Classes ------ *) 
class ReplyToPong p = 
  let F slf q = if p = q then {alive’send slf p} else {} 
  in F o pong’base ;; 
class SendPing (loc,round) = Output(\l.{ping’send loc (l,round)}) ;; 
class Handler p = SendPing p || ReplyToPong p ;; 
 
class MemState round = 
  let F _ (loc:Loc,r:Int) L = 
    if r = round & !(deq-member (op =) loc L) then {loc.L} else {L} 
  in F o (alive’base,Prior(self)?{[]});; 
class Mem client req_num round = 
  let F _ L = if length L >= threshold then {out’send client (L,req_num)} else {} 
  in F o (MemState round);; 
 
class Round (client, req_num, round) = 
     (Output(\_.locs) >>= \l.Handler (l,round)) 
  || Once(Mem client req_num round);; 
 
class PState = 
  let F loc (client,req_num) (_,_,n) = {(client, req_num, n + 1)} 
  in F o (start’base,Prior(self)?(\l.{(l,0,0)}));; 
class P = PState >>= Round;; 
 
class ReplyToPing = (\loc.\(l,round).{pong’send l (loc,round)}) o ping’base ;; 
 
(* ------ Main class ------ *) 
main P @ {p} || ReplyToPing @ locs

Figure 2: Ping-pong protocol with memory


Imported library functions

The specification imports two Nuprl functions.

  • length, which computes the length of a list
  • deq-member, which checks whether an element belongs to a list

    To apply this to lists of type T we must also supply an operation that decides equality for elements of T. That operation is a parameter to the membership test; thus, we write (deq-member eq y lst) to compute the value of the boolean “y is a member of list lst, based on the equality test eq.”

Class combinators

The specification uses the three remaining primitive combinators:

  • Prior(X): Event e belongs to Prior(X) if some X-event has occurred at loc(e) strictly before event e; if so, its value is the value returned by X for the most recent such X-event. Once an X-event has occurred at location l, all subsequent events at l are Prior(X)-events.
  • X?f: For any class X of type T, and any function f : Loc Bag ( T ), X?f has the following meaning:
                        {
v ∈ (X?f)(e)   iff      v ∈ X(e)     if e is an X- event
                      v ∈ f(loc(e)) otherwise

    If ( f  l) is nonempty, then all events at location l are (X?f )-events.

  • self: The underlying semantic model of EventML has powerful operators for defining event classes by recursion, including mutual recursion. However, EventML itself currently provides only a simple recursion scheme, which has been adequate for all the practical examples we have considered. The keyword self can occur only in contexts such as
        class X = G (Prior(self)?f)

    where, instead of being simply an argument to a function, Prior(self)?f could be a subterm of a more general expression. As a result of this definition X satisfies the fix-point equation

        X = G (Prior(X)?f)

    that specifies the value of X at any event e in terms of its value at the immediately prior X-events; or, if there is no prior X-event, in terms of f (loc (e)). Examples will make this clear.

P and PState

Class P uses PState to generate a unique round number for each request, and passes that to Round, which in turn performs step 2 of the protocol. The definition of PState is recursive.

class PState = 
  let F loc (client,req_num) (_,_,n) = {(client, req_num, n + 1)} 
  in F o (start’base,Prior(self)?(\l.{(l,0,0)}));;

This defines a state machine as follows:

  • start’base-events trigger change of state.
  • The state type of PState is (Loc * int * int). The state components represent, respectively: the client whose request has caused the state change, the request number assigned by the client, and the most recent round number generated by PState.
  • For any start’base-event e, v PState (e) iff v is the state of PState after it has processed event e.
  • The initial value of the state at location l is (l,0,0).

    The first two components of this initial state are dummy values.

  • The transition function at location l is ( F  l). If [ start :client, req_ num] arrives in state (l, r, n), the new state is (client , req_ num , n + 1).

As an exercise, we unroll some instances of the definition. By definition, PState satisfies the recursion equation:

   PState = 
    let F loc (client,req_num) (_,_,n) = {(client, req_num, n + 1)} 
    in F o (start’base,Prior(PState)?(\l.{(l,0,0)}));;

Note first that, because the return value of

    \l.{(l,0,0)}

is always nonempty, every event belongs to the class

    Prior(PState)?(\l.{(l,0,0)})

It follows from this that the PState-events are precisely the start’base-events. (The locally defined function F always returns a nonempty result; therefore, for any A and B, the events in F o (A,B) will be those events that are both A-events and B-events.)

Suppose that event e1, the arrival of the message [ start :c1 , r1 ], is the first PStart -event occurring at location l. Call it event e1. At e1, PState returns

F l (c1,r1) (l,0,0) = {(c1,r1,1)}

Suppose e2, the arrival of the message [ start :c2 , r2 ], is the next PStart -event occurring at location l. At e2 , PState returns

F l (c2,r2) (cl,r1,1) = {(c2,r2,2)}

The key point is that the argument supplied to F by

    Prior(PState)?(\l.{(l,0,0)})

is the value of the state when the incoming message arrives—which is the value returned as a result of the previous start message—or, if there hasn’t been one, (l,0,0).

Mem and MemState

The state machine PState maintains an internal state and after an input event returns a singleton bag containing its new state. It is, essentially, a Moore machine.

A memory module will maintain an internal state (listing the nodes from which alive messages have been received); it outputs not its state but an out message—and not every change of state will cause an output. A simple way to achieve this is to define two classes: MemState, like PState, simply accumulates a state and makes it visible; Mem observes MemState and generates an output when appropriate.

The class (MemState round) accumulates and makes visible the internal state:

class MemState round = 
  let F _ (loc:Loc,r:Int) L = 
    if r = round & !(deq-member (op =) loc L) 
    then {loc.L} 
    else {L} 
  in F o (alive’base,Prior(self)?{\l.[]});;

An input event to this state machine is the arrival of an alive message. The state is a list of locations, initially empty; it contains the distinct locations from which alive messages have been received for round number round, and ignores all other messages. When a message arrives with body (loc,r) the new state is determined as follows: if the message’s round number is round, and loc is not yet on the list, prepend loc to the state; otherwise, no change. (Because round numbers are globally unique, this class can perform its function without knowing either the client who initiated the request or the request number assigned.)

Notation: Some of the formal arguments to the function F are labeled with types: (loc:Loc,r:Int), rather than (loc,r). It is always legal to label patterns or expressions with types; and, in some situations, the type inference algorithm needs the extra help. The use of labels can be eliminated by using variable declarations, which are introduced in section 5.

Notation: Recall that the first argument to deq-member must be an equality operation. In the term “deq-member (op =) loc L” the equality operation is denoted by “(op =).” In general, “(op g)” means “g used as a binary infix operator.”

When (Mem client req_num round) sees that the state of (MemState round) has grown to a list of length threshold it signals the client.

class Mem client req_num round = 
  let F _ L = if length L >= threshold 
              then {out’send client (L,req_num)} 
              else {} 
  in F o (MemState round);;

3.3 Leader election in a ring

Many distributed protocols require that a group of nodes choose one of them, on the fly, as a leader. Here is a simple strategy for doing that under the assumptions that:

  • the nodes are arranged in a ring (each node knowing its immediate successor)
  • each node has a unique integer id


specification leader_ring 
 
(* ------ Parameters ------ *) 
parameter nodes  : Loc Bag 
parameter client : Loc 
parameter uid    : Loc  Int 
 
(* ------ Imported Nuprl declarations ------ *) 
import imax 
 
(* ------ Type functions ------ *) 
type Epoch = Int 
 
(* ------ Interface ------ *) 
input    config  : Epoch * Loc (* To inform a node of its Epoch and neighbor *) 
output   leader  : Epoch * Loc (* Location of the leader    *) 
input    choose  : Epoch       (* Start the leader election *) 
internal propose : Epoch * Int (* Propose a node as the leader of the ring *) 
 
(* ------ Classes ------ *) 
let dumEpoch = 0 ;; 
 
class Nbr = 
  let F _ (epoch, succ) (epoch’, succ’) = 
    if epoch > epoch’ 
    then {(epoch, succ)} 
    else {(epoch’, succ’)} 
  in F o (config’base,Prior(self)?(\l.{(dumEpoch,l)})) ;; 
class PrNbr = Prior(Nbr)?(\l.{(dumEpoch,l)}) ;; 
 
class ProposeReply = 
  let F loc (epoch, succ) (epoch’, ldr) = 
    if epoch = epoch’ 
    then if ldr = uid loc 
         then {leader’send client (epoch, loc)} 
         else {propose’send succ (epoch, imax ldr (uid loc))} 
    else {} 
  in F o (PrNbr,propose’base) ;; 
 
class ChooseReply = 
  let F loc (epoch, succ) epoch’ = 
    if epoch = epoch’ 
    then {propose’send succ (epoch, uid loc)} 
    else {} 
  in F o (PrNbr,choose’base) ;; 
 
(* ------ Main class ------ *) 
main (ProposeReply || ChooseReply)  @ nodes

Figure 3: Leader election in a ring


Any node may start an election by sending its own id to its immediate successor (a proposal). With one exception, a node that receives a proposal will forward to its successor the greater of the following two values: {the proposal it received, its own id}. The exception occurs if (and only if) a node receives in a proposal its own id. In that case, the node stops forwarding messages and declares itself elected. If messages are delivered reliably and no nodes fail, this protocol will always succeed in electing the node with the greatest id.

Fig. 3 presents our specification of a slightly more sophisticated protocol. We add an interface that makes it possible for some external party to reconfigure the ring—e.g., if it believes that some nodes have failed. Informally, we call the intervals between reconfigurations epochs (setting aside the vagueness of “between” in a distributed setting). We number the epochs with positive integers—using 0 to mean “no epoch has started at this node.”

The inputs to the protocol are of two kinds:

  • a config message tells a node to begin a new epoch and stipulates which node is, in the new epoch, its immediate successor in the ring;
  • a choose message contains the number of an epoch, and asks for an election in that epoch.

The outputs of the protocol are leader messages sent to some designated client. The body of a leader message contains an epoch number and the id of the leader elected in that epoch.

Parameters to the protocol are

  • nodes : Loc Bag – the nodes from which a leader must be chosen
  • client : Loc – the node to be informed of the election results
  • uid : Loc Int – a function assigning a unique id to each member of nodes

Our slightly generalized protocol is still quite simple to describe. A node keeps track of the epoch in which it is currently participating and ignores all propose or choose messages labeled with other epochs. If it receives a config message for an epoch numbered higher than its current epoch, it switches to the new epoch, and otherwise ignores it. A node reacts to all non-ignored propose and choose messages as in the original protocol.

The delicate part lies in formulating the invariants preserved by the protocol and the conditions under which it succeeds. What if reconfiguration occurs while an election is going on? What if config messages arrive out of order—requesting epoch 4 and later requesting epoch 3? What if config messages partition the nodes into two disjoint rings? We ignore those questions.

Nbr, the state of a node

Informally, the state of any node is a pair epoch,succ : Int * Loc, where epoch is the number of its current epoch and succ is the location of its current successor. This state changes only in response to config messages. We capture that behavior in the class Nbr, which defines a state machine as follows:

  • At location l, its initial state is 0,l; essentially, these are both dummy values.
  • Input events are the arrivals of config messages, which are recognized by the base class config’base.
  • The state transition in response to the input epoch,succ′⟩ is: if epoch > epoch, then change to epoch,succ′⟩; otherwise, no change.

We use the state machine idiom described in section 3.2. In addition to Nbr, which observes the state after an input has been processed, we define PrNbr, which observes the state when an input arrives and before it has been processed. (In fact, Nbr is only an auxiliary for the sake of defining PrNbr.)

let dumEpoch = 0 ;; 
 
class Nbr = 
  let F _ (epoch, succ) (epoch’, succ’) = 
    if epoch > epoch’ 
    then {(epoch, succ)} 
    else {(epoch’, succ’)} in 
  F o (config’base,Prior(self)?(\l.{(dumEpoch,l)})) ;; 
class PrNbr = Prior(Nbr)?(\l.{(dumEpoch,l)}) ;;

Factoring the main program.

We factor the behavior of the protocol into two classes, one triggered by propose messages and one triggered by choose messages. We define

main (ProposeReply || ChooseReply)  @ nodes

and will define both ProposeReply and ChooseReply in terms of PrNbr.

ProposeReply.

The response to a proposal is as described informally: send a leader message if you receive your own id; otherwise, propose to your successor the max of the proposal received and your own id.

class ProposeReply = 
  let F loc (epoch, succ) (epoch’, ldr) = 
    if epoch = epoch’ 
    then if ldr = uid loc 
         then {leader’send client (epoch, loc)} 
         else {propose’send succ (epoch, imax ldr (uid loc))} 
    else {} 
  in F o (PrNbr,propose’base) ;;

Since Nbr changes only in response to config messages, the state of Nbr is the same both before and after a propose message arrives. So why couldn’t we simplify this definition by replacing the expression “F o (PrNbr,Propose)” with “F o (Nbr,Propose)”?

The reason is that Nbr can only observe config’base-events, whereas PrNbr can observe any event e. This use of (Prior (...))?(...)  is a basic idiom of EventML programming—although, as will be seen in section 4, it is often conveniently packaged within standard library combinators.

Note: If e is a propose’base-event at location loc, and no config’base-event has yet occurred at loc, then e is a PrNbr-event, and the only value PrNbr observes at e is the pair (dumEpoch,loc).

ChooseReply

When ChooseReply receives a choose instruction for the epoch on which it is currently working, it initiates an election by sending an appropriate propose message.

class ChooseReply = 
  let F loc (epoch, succ) epoch’ = 
    if epoch = epoch’ 
    then {propose’send succ (epoch, uid loc)} 
    else {} 
  in F o (PrNbr,choose’base) ;;

This uses PrNbr instead of Nbr for the same reason that ProposeReply does.