PX - the Protocol eXplorer

Click here to download the source archive (including examples) suitable for compilation on Linux.

PX is the Protocol eXplorer, which is the best name I could come up with at the time for my protocol validator. WTF is a protocol validator, you ask? Well, first we have to define what we mean by protocol. For our purposes, a protocol is the set of rules and mechanisms by which a set of independent and entities ("nodes") communicate and cooperate to perform some task. The task could be anything, but usually it is a network-oriented task such as a distributed search or file transfer.

So that's what a protocol is; what's a validator? A validator is a program that proves a protocol does what it's supposed to do, by proving that every state reachable within the protocol is correct and eventually leads to a correct end state. The simplest way to do this is simply to generate every possible state, and then call various functions to determine whether the state is correct, whether it's an end state, etc. The sorts of protocol errors that can be detected by this approach include:

The PX approach to validation is based on Murphi, which is an excellent tool that anybody considering protocol-validation work should consider. PX has some slightly different goals than Murphi, though:

Structure and Variable Declarations

The most elemental entities in PX are nodes and messages. Nodes are the "places" or "actors" in a protocol, most often representing computers. Messages encapsulate the information exchanged between nodes, and are usually arranged into queues. Both are defined similarly in the PX mini-language:

message my_msg_type {
	type1 field1;
	type2 field2[length];
}
node my_node_type {
	type3 field3;
	my_msg_type my_queue[q_length];
}

Both of these get translated quite directly into C structures. In the example, the PX output will include declarations for "my_msg_type" and "my_node_type", also known as "struct _my_msg_type" and "struct _my_node_type" respectively. The fields within each of the C declarations will be almost identical to those in the PX declarations, with a few important caveats:

The PX specification file may also contain declarations for global node and message variables. These declarations are constrained in the same ways as fields within node/message declarations, and the values of all such variables at one point in time constitute a PX state that may be saved and restored. The "const" keyword cannot be applied to variables. If you want a constant value outside of a node or message structure, don't declare it in PX at all; just declare it somewhere else in C.

Message Queues

Message fields appearing within nodes and variables are automatically converted into message queues. For each message type xxx, the following types and functions are defined:

typedef struct _xxx { ... } xxx;
struct _xxx_queue { ... };
void xxxGet (struct _xxx_queue *, xxx *);
void xxxPut (struct _xxx_queue *, xxx *);
unsigned int xxxLen (struct _xxx_queue *);

The Get and Put functions are used to read and write messages on the queue, respectively; the Len function returns the number of messages currently in the queue. You don't need to know what's inside a queue structure, and shouldn't rely on it. Using message queues is actually easier than it looks, and can be best illustrated by an example. Consider the following PX declarations:

message mtype {
	int opcode;
}
mtype myqueue[8];

The common idioms for sending and receiving messages would then be as follows:

mtype mymsg;

// Sender.
mymsg.opcode = 7;
mtypePut(&myqueue,&mymsg);

// Receiver.
if (mtypeLen(&myqueue)) mtypeGet(&myqueue,&mymsg);

Note that the Get and Put functions will fail (abort) if the message queue is totally empty or totally full, respectively.

Transition Rules

So far we're able to define the data used by PX; now it's time to define the protocol itself. The "guts" of a protocol consists of the transitionrules - hereafter simply "rules" - that tell us about transitions from one state to another. In PX, rules are functions. When the PX engine is looking at a state, it simply calls these functions to generate new states. The PX declarations look like this:

rule SendRequest (5);
rule ReceiveRequest (1);

The corresponding C functions look like this:

int SendRequest (unsigned int nodeNum)
{
	if (!CheckPrecondition(nodeNum)) {
		return 0;
	}
	// Mess around, change state.
	return 1;
}

int ReceiveRequest (unsigned int notUsed) { ... }

Unlike many other protocol validators, including Murphi, PX invokes all rules for all states. Rules are therefore responsible both for checking their own applicability and for generating new states. If the rule is not currently applicable (i.e. its preconditions are not met), the function should return zero and PX will consider that rule "skipped" this time around. If the rule is applicable and its application results in a new state, the function should return non-zero and PX will add the new state to its tables for later evaluation.

Rule declarations in PX always have an associated "repeat count" (5 for SendRequest in the above example) which would most often be an index into an array declared within PX but could be anything. When applying a rule with repeat count N to a state, PX will call the associated function N times with arguments from 0 to N-1. This provides a convenient though limited way to apply a rule to each node within a system without having to provide separate functions (for a more powerful mechanism, see Murphi's rulesets).

Invariants and Goals

Once the data structures, variables, and transition rules are defined, we have a protocol. To verify the correctness of that protocol, PX needs only two additional pieces of information, both similar to the rules described above:

Invariant and goal declarations look just like rule declarations in PX, except for different keywords:

invariant OnlyOneCritical (1);
goal MessageReceived;

Invariants may be specified without a repeat count, in which case the associated function is called once per state. Goals never have repeat counts. In both cases, the C function takes the same argument as if a repeat count had been specified, even though the argument value is always zero.

For an invariant, the function should return non-zero to indicate that the invariant is satisfied, i.e. that the state is valid and PX should continue; a zero return would mean that the state is invalid and PX should report an error. For a goal, the function should return non-zero to indicate that the state meets the requirements for a goal state. PX will flag this state as a goal state internally; when all states have been generated and have passed all invariant tests, this flag will be used to determine that all states lead to goal states.

Input File

The PX input file consists of three parts, separated by "%%" on a line by itself as in YACC. For example:

#include <stdio.h>
#include "px_defs.h"
typedef char[8] data_t;
%%
message msg_t {
	char opcode;
}
node node_t {
	msg_t queue[3];
	data_t data;
}
# Hi!  This is a comment.
node_t my_nodes[4];
rule KickNode(4);
invariant NotScrewedUp(1);
goal Finished(1);
%%
int KickNode (unsigned int n) { ... }
int NotScrewedUp (unsigned int n) { ... }
int Finished (unsigned int n) { ... }

The following notes also refer to the example:

To process the PX input, simply "px < input_file.p > output_file.c". You must then compile the output and link it with px_main.o (plus any other object files you want) to create a protocol validator.

Other Functions

There are several functions either provided or required by PX. The naming convention used in PX is as follows:

You don't need to know about most of these symbols unless you're hacking the PX code itself. Those you do need to know are:

void XuInitialize (void)
You must provide this function. It is called once, when validation starts, for you to set up any constant values and "plumbing" (e.g. pointers within a node to other node's message queues) that you want.
void XuPrint (char *)
You must provide this function, used to print out all information about the state currently contained in global variables. The argument is a textual description of the rule that fired to get to the current state. For the sake of clarity, the current state should be printed out indented one level, followed by the rule information.
void XeError (char *)
PX provides this function, which you may call to report an error and terminate the program.

Puzzle Solving

Because PX contains a lot of infrastructure for generating and checking states, it can be used not only for validation but also to solve certain puzzles that can be expressed as protocols. For example, the classic "frustrated farmer" puzzle (described in the "fox" example) is amenable to this approach. The state transitions are river crossings, the invariants are the inverse of states in which something gets eaten, and the goal state is the one in which everything is across the river. To facilitate these uses, the PX engine supports some additional command-line options in the final program:

With only a little bit of further work, PX could probably be used to play some sorts of games - specifically fully deterministic zero-sum games with perfect information. This would require only a trivial enhancement of goal functions into evaluation functions and some fairly minor changes to the pruning code. However, other engines already exist for that particular purpose and do a much better job of it, so it's unlikely that PX will ever actually evolve in that direction.

Examples

Two examples are provided in the source archive, to show possible uses of PX:

Future Work

This is mostly just a to-do list for myself. Of course, if someone else felt like donating patches I'd be delighted.