\section{Predicate Control}

We introduced the predicate control problem in \cite{tg98-spdp} with an
emphasis on its application to distributed debugging. Predicate control
involves adding causal dependencies (synchronizations) to a concurrent
computation in order to ensure that a global condition (predicate) is
always satisfied.  Depending on whether the computation is known {\em a
priori\/} or provided on-line, we may distinguish between off-line
predicate control and on-line predicate control. On-line predicate
control encompasses most known synchronization techniques. For example,
typical mutual exclusion algorithms work on-line and are special cases
of on-line predicate control. As we will see, off-line predicate
control is easier to solve than on-line predicate control. This key
observation is strong motivation for our rollback and replay approach
to avoiding synchronization faults.

\subsection{Past Work}

In a previous work \cite{tg98-spdp}, we investigated the predicate
control problem in full generality and demonstrated that it is
NP-hard.  Our next step was to attempt to solve predicate control for a
simple but useful class of predicates -- {\em disjunctive
predicates\/}.  A disjunctive predicate specifies that at least one of
a set of local conditions must be true at all times. In other words, a
combination of bad conditions must never arise. We designed an
efficient algorithm for solving off-line disjunctive predicate
control. We further showed that on-line disjunctive predicate
control is impossible to solve in general. This is an example of
our observation that solving predicate control off-line is easier
than solving it on-line. We did, however, place a reasonable
restriction on the computation, and we provided an efficient algorithm
for on-line disjunctive predicate control.

A general boolean predicate can be converted into a conjunction of
disjunctive predicates. Although, we know from our results in
\cite{tg98-spdp} that such predicate control is NP-hard, we have solved
the problem efficiently under restrictions on the computation itself.
The types of computations allowed are those for which the regions where
the local conditions are false are mutually separated from each other.
We call predicates of this kind {\em locally independent predicates\/}.
By placing a restriction similar to the one for on-line disjunctive predicate
control, we can solve the on-line case as well.

Recently, we have made more progress towards extending the scope
of predicate control. A useful type of predicate that falls in
neither of these categories is {\em general mutual exclusion\/}.  We
have designed algorithms that not only solve off-line predicate control
for mutual exclusion, but also for useful variants such as mutual
exclusion with independent locks and mutual exclusion with read-write
locks. We are currently working on the proofs of these algorithms but
there is strong indication that they work! Again, these algorithms
are remarkable because mutual exclusion is impossible to solve on-line.
Although many algorithms have been published for on-line mutual exclusion,
each of them makes some simplifying assumption, such as non-blocking
critical sections.

While on-line predicate control has been exploited in various
specialized forms to control on-line synchronization (such as standard
mutual exclusion algorithms), off-line predicate control is relatively
a recent discovery. We now demonstrate its use in two application
domains: distributed debugging and our fault avoidance system.

\subsubsection*{Application 1: Distributed Debugging}

\begin{figure}
\centerline{\epsfbox{Figures/active-debugging.eps}}
\caption{Distributed Debugging \label{fig:example}}
\end{figure}

Consider a replicated server system with three server processes $P_1$,
$P_2$ and $P_3$.  During debugging, a trace of the distributed
computation was taken as shown in Figure~\ref{fig:example}(a).  The
thicker intervals in the process executions indicate intervals when the
servers weren't available for service.

The system should have been designed to ensure that one server was
available at all times. So we run a predicate detection algorithm on
the computation (as discussed in the previous section) to detect the
bug:
$$ P_1\ is\ unavailable\ \wedge\ P_2\ is\ unavailable\ \wedge\ P_3\ is\ unavailable$$ 
Note that this happens to be a conjunctive predicate. We detect two
consistent global states $G$ and $H$, as shown in the diagram, where
this is possible.

Our next step is to control the computation with the predicate:
$$ P_1\ is\ available\ \vee\ P_2\ is\ available\ \vee\ P_3\ is\ available$$
Note how this disjunctive predicate is the negation of the conjunctive
predicate that represents the bug. It is noteworthy that our efficient
solution for conjunctive predicate detection works so well with our
efficient solution for disjunctive predicate control.  We use our
off-line predicate control algorithm, and the resulting computation is
shown in Figure~\ref{fig:example}(b).  Note how the synchronizations
from $a$ to $b$ and from $c$ to $d$ ensure that global states $G$ and
$H$ are no longer consistent and the bug doesn't occur. Having gotten
rid of the bug in this computation, we can now replay it for further
observation. This process of observation followed by control helps
us localize the source of the bug (refer to \cite{tg98-spdp} for further
details).

\subsubsection*{Application 2: Fault Avoidance}

We have noted that the negation of a conjunctive predicate is a
disjunctive predicate. In section~3, we presented an example of a
race condition expressed as a conjunctive predicate. The negation
of this predicate is the following disjunctive predicate:
$$ P_1\ is\ not\ writing\ object\ x\ \vee\ P_2\ is\ not\ reading\ object\ x $$
Avoiding this race can, therefore, be achieved efficiently
using our predicate control algorithm. However, it must be
noted that this would work only for a two process race.

However, since we are likely to solve general off-line mutual exclusion
in the near future, we would be able to avoid a general race condition
by controlling the general mutual exclusion predicate:
$$no\ two\ processes\ access\ object\ x\ together$$
Since we should be able to solve mutual exclusion with
independent locks and read-write locks, we have the corresponding
ability to avoid independent races (on different objects, for example)
and read-write races:
$$no\ two\ processes\ access\ object\ x\ together\ \wedge\ 
no\ two\ processes\ access\ object\ y\ together$$
$$no\ two\ processes\ access\ object\ x\ together,\ where\ one\ access\ is\ a\ 
write$$

For an explicit example of how a race would be avoided in the fault
avoidance system, refer to the example in section~2.


\subsection{Proposed Work}

We propose to complete our ongoing work towards solving off-line
mutual exclusion. As we have noted above, this type of predicate
control has important implications for race avoidance.

Our studies in predicate control have so far been limited to the
happened before model. However, as we have noted, potential causality
is the better model for the fault avoidance system. Therefore, we now
propose to extend our study of predicate control to the potential
causality model.

Ease of implementation has been an issue in predicate control that
has not been studied so far. The natural requirement to implement
predicate control as part of the fault avoidance system is a convenient
way to test the ease of implementation of predicate control in general.
