Ariadne's modeling language is quite simple. Communication patterns are described in terms of a three-level hierarchy of chains, p-chains, and pt-chains.
The three definitional levels appear to form a natural mechanism for describing parallel systems, as evidenced by their use in other contexts such as the XYZ levels of Phase Abstractions [42] and the LaRCS specification language [31]. The matching algorithm for our language is straightforward: a pt-chain is recognized by a finite state machine that invokes copies of other finite state machines to recognize chains on specific processes. This matching can be done efficiently - in most cases the matching can be done in linear time, although the verification of the logical time relationships between abstract events may take polynomial time - avoiding the costliness of pattern matching approaches [19][5] and the expensive implementations (number of states can potentially be exponential in the length of the parallel expression to be recognized) of previous languages [22]. At the same time, our matching algorithm can provide precise information on the reasons for a match failure.
Example: Binary Image Compression.
We illustrate the modeling language by using
it to model the behavior of a parallel version of
Binary Image Compression [39] on a 
processor
distributed memory computer. The algorithm compresses an image
in a tree representation by successfully combining identical subtrees
working up from the leaves.
We will use it throughout the paper.
Figure 2(a) and 2(b) show
a labeled 4 
4 pixel array, and a corresponding
image pixel array respectively. The
complete bintree representation is shown in
Figure 2(c); that image
is obtained by alternatively splitting the
image along 
and 
axes.
The compression algorithm performs a preorder traversal of the tree,
combining sibling leaf nodes with the same color by pruning them and
representing that color at their parent as shown in Figure 3.
The parallel version of the algorithm is very similar. The nodes of the representing tree are divided among the processors as shown in Figure 4. Each processor compresses its local subtree as before. Once the local compression is finished, processors enter a communication phase to determine whether the local compressed images can be merged together. At each step, the processor of a sibling pair with the higher identifier initiates a comparison for possible compression. To model this behavior in Ariadne, we used user defined message tags (indicated by underscores) to identify different functions of R and W operations. A trace file was then recorded with 6 message types: W_query, R_query, W_fail, R_fail, W_succ, and R_succ.
We modeled the two different outcomes of a sibling communication. The
case where the comparison failed and the nodes were not compressed was
modeled as:
ch compr_fail = W_query @ R_query
W_fail @ R_fail;
where ch is a keyword signalling a
chain definition. A single message
consists of a W connected by an edge (denoted by @) to the
receive of the same message (denoted by R).
A successful comparison was:
ch compr_succ = W_query @ R_query
W_succ @ R_succ;
From the perspective of an initiating processor,
the comparison behavior was represented as
ch compr = compr_fail or compare_succ
The concurrent execution of a comparison can be modeled as the
following p-chain behavior:
set procset = { 0..3 };
pch compr = compr_fail + compr_succ onsome
procset;
where set is a keyword signalling set declaration.
onsome signals that the pch need only to match on some
of the processes in the set procset.
Processors that initiate communication in a phase, does not take part
in subsequent iterations, and the number of processors are effectively
halved at each subsequent iteration. The pch definition tries
to model this at a very coarse level, by not specifying the cardinality
of the set of processes taking part in the match.
The whole behavior - a sequence
of iterations - can be modeled as
match compression = compr* ;
where match is a keyword, here
indicating some instances of the p-chain compr are to be matched
in the POEG and assigned to the variable compression
Figure 5 depicts how such a description might be matched with a POEG of the program.
As can be seen, Ariadne imposes a tree-hierarchy based on the user-defined model on the POEG of the program representing Lamport's happened before relationship. Each internal node of the tree represents a user-defined abstract event, and the leaves represent primitive events (that are vertices of the POEG). This tree is called the match tree, and should not be confused with the tree representation of the image that we discussed in the Binary Image Compression example. The levels of the match tree correspond to the hierarchical levels of the model definition and the root corresponds to the outermost level of pt-chains.
All nodes inherit the name provided by the user in the model definition, except those corresponding to the identifiers of processes where the chain description has been matched. By selecting any internal node of the match tree, the user can focus his/her attention to a portion of the execution history matched, and submit queries regarding the selected portion of the execution history. Selecting the root selects the whole matched behavior.
