For expository reasons, we model only the part of the behavior
relevant to the error, that is, we model only point insertions. These
insertions begin with some number of attempts to lock relevant
triangles:
the initiating process sends a multicast requesting the
relevant locks on req, the recipients respond on either ok
or no, and the initiating process collects the responses. A simple
form of this pattern might be
M_req @ R (W_ok @ R + W_no @ R)
where the control of matching begins on the initiating
process with the multicast and splits at the first @ to proceed
independently on each of the receiving processes.
This simple expression, however, is not sufficient because we must
also model subsequent behavior on the initiating process. In the case
of an unsuccessful attempt, the initiating process subsequently sends
an ``abort'' message and then retries the lock attempt; in the case of
a successful attempt, it subsequently attempts to get all relevant
triangles to commit to the update. Thus, we must return the control
of matching to the initiating process. We indicate this by marking
the point of the split with the symbol <@ (replacing the
@) and the point of the return with the symbol @>.
Thus a lock attempt is defined as
LockAttempt = M_req <@ R (W_ok
@ R + W_no @ R) @>
Similarly, we define an abort, an unsuccessful attempt to commit, and a successful attempt to commit
Abort = M_abort <@ R @>
CommitNo = M_com <@ R W_committed
@ R @>
CommitYes = M_com <@ R start:W_committed
@ R @>
where the CommitYes includes a tag on events that essentially marks the beginning of the critical region for the insert. The initial, unsuccessful attempts are
matched by
Unsuccessful = ( (LockAttempt Abort) * LockAttempt CommitNo Abort) *
and the ultimately successful attempt by
Successful = (LockAttempt Abort) * LockAttempt CommitYes
Once the locking attempt succeeds, the initiating process performs the
actual insertion of its point by sending a
multicast on port add and waiting for acknowledgments
on port done. The pattern is
Addition = M_add <@ R end:W_done @ R @>
where the tag end is used to mark the end of the critical region for this insert. The entire
chain and the needed p-chains are as follows
? Insert = Unsuccessful Successful Addition
? for (i=0; i <= P-1; i++) do AddPoint[i] = Insert ONALL {i} od
We successfully matched the expected behavior with the command:
? Triangulation = match (AddPoint[]) *
This led us to conclude that all of the needed transactions had
occurred. We hypothesized that there must have been some interference
between insertions. To check this, we used the following query,
looking just at the ``successful" portion of the matched additions.
? e_non_overlaps(Triangulation WRT {start,end})
Assertion Failed.
AddPoint[17] overlaps AddPoint[13]
AddPoint[55] overlaps AddPoint[54]
AddPoint[100] overlaps AddPoint[98]
The feedback on the failure of this assertion led us to investigate
the pairs of points that had overlapping insertions. We discovered
that processes in each pair shared common triangle vertices. This
led us to an error in our locking mechanism: in effect, we
were locking the sides of the triangle but not their vertices.
Ariadne was designed as a testbed for investigating the utility and limitations of various types of match feedback. The above examples demonstrate successful uses of its current features. In the next section, we give an example of a program for which it was not successful.