%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{The Predicate Control Problem}}

\vspace{1in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>{\bf Problem Statement:}\\ 
\>\>Given a computation $\langle E, \ra \rangle $ and a global predicate $B$, \\
\>\>find a controlling computation of $B$ in $\langle E, \ra \rangle$.\\ \ \\ \ \\[0.4in]
\>Applications:\\[0.2in]
\>\>$\bullet$ Software fault tolerance\\[0.1in]
\>\>$\bullet$ Distributed debugging\\[0.1in]
\>\>$\bullet$ Off-line scheduling
\end{tabbing}

%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Why is it difficult?}}

\vspace{0.7in}
\begin{center}
	\begin{figure*}
	\centerline{\epsfbox{Figures/fig4-difficult.eps}}
	\end{figure*}

\vspace{0.6in}

\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\> $\bullet$ Cycles must be avoided. (e.g. $a - b - e - f$)\\ \ \\
\> $\bullet$ General Predicates: NP-Complete \MidnightBlue{[Tarafdar and Garg 98]}
\end{tabbing}
\end{center}
%INC: Maybe some more complicated examples to show how difficult it can be
%INC: involving computation -> contr. comp. figures
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Disjunctive Predicates}}
\vspace{0.3in}
\begin{center}
$B\ =\ \l_1\ \vee\ \l_2\ \vee\ \cdots\ \vee\ \l_n$\\[9pt]
$\mbox{\hspace{5in}}$ {\small ($\l_i$: {\em local predicate} of process $P_i$)}
\vspace{0.2in}
	\begin{figure*}
	\epsfxsize=3.5in
	\centerline{\epsfbox{Figures/fig5-disj-preds.eps}}
	\end{figure*}
\vspace{-0.1in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ Examples:\\
\>\>$-$ At least one server is available: \\
\>\>\>$avail_1\ \vee\ avail_2\ \vee\ \cdots\ \vee\ avail_n$\\
\>\>$-$ At least one philosopher has no fork: \\
\>\>\>$\neg fork_1\ \vee\ \neg fork_2\ \vee\ \cdots\ \vee\ \neg fork_n$
\end{tabbing}
\end{center}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Interval Graphs}}
\vspace{0.5in}
	\begin{figure*}
	\epsfxsize=5.5in
	\centerline{\epsfbox{Figures/105.eps}}
	\end{figure*}
\vspace{0.4in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ $i1 \ord i2$ denotes ``$i1$ starts before $i2$ finishes''\\ \ \\
\>$\bullet$ $\langle {\cal I}, \ord \rangle$ is an {\em interval graph\/} \\ \ \\
\>$\bullet$ Interval graphs may contain cycles
\end{tabbing}

%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Solving for Disjunctive Predicates}}
\vspace{0.6in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>{\bf Theorem:} \ \ \MidnightBlue{[Tarafdar \& Garg 98]}\\
\> A controlling computation of a computation $C$ exists {\bf iff}\\
\> the interval graph for $C$ contains no cliques of $n$ false intervals.
\end{tabbing}
\vspace{0.5in}
	\begin{figure*}
	\epsfxsize=6.0in
	\centerline{\epsfbox{Figures/106.eps}}
	\end{figure*}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Solving for Disjunctive Predicates}}
\vspace{0.7in}
	\begin{figure*}
	\epsfxsize=7.5in
	\centerline{\epsfbox{Figures/107.eps}}
	\end{figure*}
\vspace{0.5in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\> complexity:  $O(np)$\\
\> \> $n$ is the number of processes\\
\> \> $p$ is the number of false intervals in the computation
\end{tabbing}
%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{\Brown{Mutual Exclusion Predicates}}
\vspace{0.6in}
\begin{center}
$B\ =\ \forall \ \mbox{distinct} \ i, j: \ \neg (critical_i \  \wedge \  critical_j)$\\[15pt]
$\mbox{\hspace{4in}}$ {\small ($critical_i$: local predicate of process $P_i$)}
\vspace{0.5in}
	\begin{figure*}
	\epsfxsize=4.5in
	\centerline{\epsfbox{Figures/109.eps}}
	\end{figure*}
\end{center}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Variants of Mutual Exclusion Predicates}}
\vspace{1.0in}
\begin{center}
	\begin{figure*}
	\epsfxsize=9.0in
	\centerline{\epsfbox{Figures/108.eps}}
	\end{figure*}
\end{center}
%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{\Brown{Solving for Mutual Exclusion}}
\vspace{0.3in}
\begin{tabbing}
xxxxxx\= xxxxx\=\kill
\>{\bf Theorem:\/} \ \ \ \MidnightBlue{[Tarafdar \& Garg 99]}\\
\>A controlling computation of a computation $C$ exists {\bf iff} \\
\>the interval graph for $C$ contains no cycles of critical sections.\\ [0.3in]
\>{\bf Direct Algorithm:\/}\\
\>\>$\bullet$ topologically sort precedence graph of critical sections\\
\>\>$\bullet$ add control synchronizations in sorted order\\
\>\>$\bullet$ $O(p^2)$ \ \ ($p$: number of critical sections in computation)
\end{tabbing}
	\begin{figure*}
	\epsfxsize=3.7in
	\centerline{\epsfbox{Figures/218.eps}}
	\end{figure*}
%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{\Brown{Solving for Mutual Exclusion}}
\vspace{0.2in}
\begin{center}
	\begin{figure*}
	\epsfxsize=3.7in
	\centerline{\epsfbox{Figures/219.eps}}
	\end{figure*}
\begin{tabbing}
xxxxxx\= xxxxx\=\kill
\>{\bf Improved Algorithm:\/}\\
\>\>$\bullet$ Key idea: use process ordering of critical sections\\
\>\>$\bullet$ $O(p^2) \  \rightarrow \  O(n^2p)$ \ \ (further reducible to $O(np)$) \\ [0.2in]
\>$n$: number of processes\\
\>$p$: number of critical section in computation
\end{tabbing}
\end{center}
%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{\Brown{Extending to Mutual Exclusion Variants}}
\vspace{0.2in}
\begin{center}
	\begin{figure*}
	\epsfxsize=3.7in
	\centerline{\epsfbox{Figures/220.eps}}
	\end{figure*}
\begin{tabbing}
xxxxxx\= xxxxx\=\kill
\>To allow {\bf independent} and {\bf read/write} critical sections.\\[0.1in]
\>{\bf Extended Algorithm:\/}\\
\>\>$\bullet$ Key idea: critical sections in the same SCC are {\em safe\/}.\\
\>\>$\bullet$ Similar optimization leads to $O(np)$ algorithm.\\[0.2in]
\>Readers Writers : solves, if possible.\\
\>Independent Mutex: solves, under constraints (NP-Complete).
\end{tabbing}
\end{center}

%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{\Brown{Talk Outline}}
\vspace{1.0in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ Model\\ \ \\
\>$\bullet$ Predicate Control Problem\\ \ \\
\>$\bullet$ \Red{Predicate Detection Problem}\\ \ \\
\>$\bullet$ Controlled Re-execution: An Experimental Study \\ \ \\
\>$\bullet$ Conclusions
\end{tabbing}
%-------------------------------------------------------------------------------
