Parameters to our specifications are of two kinds. Some are “abstract”—e.g., the integer parameters threshold (see section 3.2) and flrs (see section 5). We can instantiate these by providing a Nuprl term of type integer. Others are “real world”—e.g., the parameter client of type location. Their meanings are specific to a particular installation of EventML: the messaging system determines what must be supplied to instantiate a location parameter. Our prototype assumes that messaging is by TCP/IP, and a location is a pair consisting of an IP address and a port.17Note that TCP/IP provides stronger guarantees—namely, FIFO delivery—than our examples have assumed.
The parameter declarations
illustrate the open-ended nature of real world parameters.
Suppose that we supply an (IP address, port) pair for client and a list of such pairs for nodes.18Computationally, a bag is just a list in which we ignore the order. How do we instantiate uid? Knowing the locations, we could simply define a function that assigns integers to them. If we wanted a more flexible implementation, we might want to base uid on the MAC address of a node’s network card; in that case the configuration file would provide some reference to a piece of code that does the computation. For now, the only primitive real-world type that we allow is Loc. All other parameter types must be intepretable from Loc and abstract types.
Here is what a configuration file looks like:
This is an example of a configuration file for the leader election in a ring protocol presented in section 3.3. A configuration file is divided into three parts: the locations part declares the machines on which one wishes to install the specified protocol (n1 is a location name which is specified by the IP address 192.168.0.12 and the port number 1977); the parameters part instantiates the parameters declared in the given specification (the leader election in a ring specification presented in section 3.3 declares three parameters: nodes, client, and uid); the messages part declares a bag of messages initially in transit. One has to declare at least one message in transit because EventML allows on to define reactive agents that can only react on receipt of messages. Therefore nothing happens as long as no message is received.
