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

\vspace{1in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>{\bf Problem Statement:}\\[5pt]
\>\>Given a computation $\langle E, \ra \rangle $ and a global predicate $B$, \\
\>\>find a consistent cut in $\langle E, \ra \rangle$ that satisfies $B$.\\ \ \\ \ \\ [0.6in]
\>Applications:\\[0.2in]
\>\>$\bullet$ Distributed monitoring\\[0.1in]
\>\>$\bullet$ Distributed debugging
\end{tabbing}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{General Computations}}
\vspace{0.3in}
\begin{center}
	\begin{figure*}
	\epsfxsize=6.0in
	\centerline{\epsfbox{Figures/110.eps}}
	\end{figure*}
\vspace{0.2in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ General computations: \ \ \MidnightBlue{[Ahuja et al 93]}\\[3pt]
\>\>$-$ Events in a process may be partially ordered.\\
\>\>$-$ Allows improved detection of predicates (faulty conditions).\\[9pt]
\>$\bullet$ Examples of {\em independent events\/}:\\[3pt]
\>\>$-$ Multithreading\\
\>\>$-$ Nonblocking communication
\end{tabbing}
\end{center}
%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{\Brown{Predicate Detection in Locally Ordered Computations}}
\vspace{0.3in}
\begin{center}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ ... is difficult (NP-Complete) \MidnightBlue{[Chase \& Garg 95]}\\[5pt]
\>$\bullet$ Intuition: too many cuts!
\end{tabbing}
	\begin{figure*}
	\epsfxsize=5.0in
	\centerline{\epsfbox{Figures/many-states.eps}}
	\end{figure*}
\vspace{0.2in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ In general, $O(m^n)$ cuts, where:\\
\>\>$m$ is the number of events in a process, and\\
\>\>$n$ is the number of processes
\end{tabbing}
\end{center}

%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Conjunctive Predicates in Locally Ordered Computations}}
\vspace{0.2in}
\begin{center}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ {\bf Conjunctive Predicate}: \\[5pt]
\>\>\>$B\ =\ \l_1\ \wedge \ \l_2\ \wedge \ \cdots\ \wedge \ \l_n$\\ [3pt]
\>\>\>\>{\small ($\l_i$: {\em local predicate} of process $P_i$)}\\[0.1in]
\>$\bullet$ Example: all servers are unavailable: \\
\>\>$unavail_1\ \wedge\ unavail_2\ \wedge\ \cdots\ \wedge\ unavail_n$\\[0.5in]
\>$\bullet$ Algorithm: \ \ \MidnightBlue{[Garg \& Waldecker 94]}
\end{tabbing}
	\begin{figure*}
	\epsfxsize=5.0in
	\centerline{\epsfbox{Figures/pred-detect-1.eps}}
	\end{figure*}
\end{center}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Predicate Detection in General Computations}}
\vspace{0.3in}
\begin{center}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ ... is difficult even for Conjunctive Predicates! (NP-Complete) \\
\>\>\>\> \MidnightBlue{[Tarafdar \& Garg 98]}
\end{tabbing}
\vspace{0.2in}
	\begin{figure*}
	\epsfxsize=6.0in
	\centerline{\epsfbox{Figures/pred-detect-2.eps}}
	\end{figure*}
\end{center}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Receive-ordered Computations}}
\vspace{0.2in}
\begin{center}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ totally ordered receive events:
\end{tabbing}
	\begin{figure*}
	\epsfxsize=4.0in
	\centerline{\epsfbox{Figures/recv-order.eps}}
	\end{figure*}
\end{center}
\vspace{0.1in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>$\bullet$ Example: Multi-threaded Server
\end{tabbing}
\begin{tt}
\hspace{1in}repeat\\
\hspace{1in}\hspace{0.5in} receive a request;\\
\hspace{1in}\hspace{0.5in} create a thread to process the request\\
\hspace{1in}until done
\end{tt}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Conjunctive Predicates in Receive-ordered Computations}}
\vspace{0.4in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>Key observation:\\
\>\>$-$ linearize each process's computation ensuring that\\
\>\>$\mbox{\hspace{12pt}}$ receive events are ordered after all concurrent events
\end{tabbing}
\vspace{0.2in}
\begin{center}
\begin{figure*}
	\epsfxsize=6.0in
	\centerline{\epsfbox{Figures/pred-detect-3.eps}}
\end{figure*}
\vspace{0.2in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>we can now apply predicate detection as before!
\end{tabbing}
\end{center}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Conjunctive Predicates in General Computations}}
\vspace{0.3in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>Another look at general (not receive-ordered) computations:
\end{tabbing}
\vspace{0.2in}
\begin{center}
\begin{figure*}
	\epsfxsize=4.5in
	\centerline{\epsfbox{Figures/pred-detect-4.eps}}
\end{figure*}
\vspace{0.2in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxx\=xxxxxxxxxxxxxxxxxx\= \kill
\>There are an exponential number of receive-ordered computations.\\
\>But the alternative -- interleaved computations -- is exponentially worse.
\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$ Predicate Detection Problem\\ \ \\
\>$\bullet$ \Red{Controlled Re-execution: An Experimental Study} \\ \ \\
\>$\bullet$ Conclusions
\end{tabbing}
%-------------------------------------------------------------------------------
