\documentclass{seminar}

% To use the standard `color' package with Seminar

\usepackage{pstcol} 
\usepackage{semcolor}
\usepackage{graphicx}
\usepackage{fancybox}
\usepackage{fancyhdr}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{theorem}

\input{seminar.bug}

% \twoup

% Create the border 

\newcommand{\pstplframebox}[1]{\psframebox[linewidth=0.5pt,framesep=0.35mm,
					   cornersize=relative,framearc=0.2]
	                      {\psframebox[linewidth=1.0pt,framesep=0.35mm,
					   cornersize=relative,framearc=0.19]
                              {\psframebox[linewidth=0.5pt,cornersize=relative,
                                           framearc=0.18]{#1}}}} 

\newslideframe{sctriple}[\SemcolorFrameOps]{\pstplframebox{#1}}


% Adjust the margins etc.

\addtolength{\slidewidth}{0.825in}
\addtolength{\slideheight}{0.3in}
% \renewcommand{\slidetopmargin}{0.60in}
% \renewcommand{\slidebottommargin}{0.60in}
\renewcommand{\slideleftmargin}{0.25in}
\renewcommand{\sliderightmargin}{0.25in}
\renewcommand{\sliderightmargin}{0.25in}

% For font size etc.

% \slidesmag{4}
% \ptsize{10}


% Line spacing

\renewcommand{\slidestretch}{1.0}


% My colors 

\input{color}

% To customize the color settings in a slide

\newcommand{\SlideColours}[3][black]{
% #1 = frame line color (optional, default=black),
% #2 = foreground color, 
% #3 = background color
\slideframe[\psset{linecolor=#1,fillcolor=#3,fillstyle=solid}]{sctriple}
\color{#2}}



% Headers and footers personalization using the `fancyhdr' package

\fancyhf{} % Clear all fields


\renewcommand{\headrulewidth}{0.0mm} % disable headrule
\renewcommand{\footrulewidth}{0.0mm} % disable footrule



\fancyhead[C]{\sf\tiny Monitoring Multithreaded Distributed Computations}
\fancyfoot[L]{\sf\tiny January 3, 2005}
%\fancyfoot[C]{\sf\tiny Department of Computer Sciences, The University of Texas at Austin} 
\fancyfoot[C]{\sf\tiny ECE Dept., Univ. Texas at Austin} 
\fancyfoot[R]{\sf\tiny Page \theslide}


% To avoid that the headers be too close of the top of the page

\renewcommand{\slidetopmargin}{0.3in}

% To center horizontally the headers and footers (see seminar.bug)

\renewcommand{\headwidth}{\textwidth}

% To adjust the frame length to the header and footer ones

\autoslidemarginstrue


% Path for figures 

\graphicspath{{sliceFigures/}}

% Figures related
\newcommand{\OneFigure}[2]{
\begin{figure}[h]
        \centerline{\includegraphics[#1]{#2}}
\end{figure}
}

\newcommand{\PutFigure}[2]{
% \begin{figure}[h]
\centerline{\includegraphics[#1]{#2}}
% \end{figure}
}

\newcommand{\PutFigureLatex}[2]{
% \begin{figure}[t]
\centerline{\resizebox{#1}{!}{\input{sliceFigures/#2}}}
% \end{figure} 
}

% Slide heading
% Possible choices: \fbox, \shadowbox, \doublebox, \ovalbox, \Ovalbox

\setlength{\fboxrule}{0.15mm}
\setlength{\fboxsep}{1.5mm}


\newcommand{\MyHeading}[2][2.0ex]{
\begin{center} 
	\textcolor{Brown}{\doublebox{\sf\large
	\textbf{\boldmath#2\unboldmath}}}  
\end{center}
\vspace{#1}
}

\newcommand{\MyTitle}[1]{{\color{Brown} \Large \textbf{#1}}}

% Citations

%\newcommand{\MyCite}[1]{\textcolor{NavyBlue}{[#1]}}
\newcommand{\myblue}[1]{\textcolor{NavyBlue}{#1}}
\newcommand{\MyCite}[1]{\textcolor{green}{[#1]}}
\newcommand{\mydesc}[1]{\textcolor{red}{#1}}


% Spacing at the beginning of a line

\newcommand{\MySpace}{\hspace*{0.0in}~~~~}

\newcommand{\nl}{\\ \hspace*{0.0in}}


% To comment a block of text

\newcommand{\punt}[1]{}
\newcommand{\remove}[1]{}


\input{macros}

\newcommand{\halflinespacing}{\vspace*{0.3em}}


\newcommand{\sbullet}{\triangleright}


% change label style for enumerate environment


\renewcommand{\labelenumi}{(\arabic{enumi})}


% \newenvironment{myenumerate}
% {\begin{enumerate}
% \setlength{\leftmargin}{5.0cm}}
% {\end{enumerate}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}



{\sf
\centerslidesfalse
\SlideColours[BurntOrange]{black}{white}
\pagestyle{fancy}
\renewcommand{\slidetopmargin}{0.50in}
\renewcommand{\slidebottommargin}{0.5in}

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

\begin{slide}
\centerslidestrue
\begin{center}
%\textcolor{black}{\small Dissertation Defense:}

~ \\

\MyTitle{Monitoring Multithreaded Distributed Computations}

~ \\ ~ \\ 


~ \\

\textcolor{blue}{Vijay K. Garg}
~ \\
{\color{black} \small
Department of Electrical and Computer Engineering\\
The University of Texas at Austin \\
Austin, TX 78712\\
email: garg@ece.utexas.edu\\
}





%~ \\
%
%\textcolor{black}{\small August 22, 2002}
\end{center}
\end{slide}

%-------------------------------------------------------------------------------
%\begin{slide}
%\MyHeading{Problem}
%
%\end{slide}
%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Motivation: Software Faults}

\begin{itemize}
\item Software faults are dominant reasons for system outages
\item Approx 2 to 3 bugs per 1000 lines of code! \MyCite{Gray and Reuter 93}
\end{itemize}

~ \\
\myblue{Testing and Debugging:}

\begin{itemize}

\item Distributed programs are prone to errors.

\item Traces need to be analyzed to locate bugs.

\end{itemize}

%only so many IIT K can produce
~ \\

\myblue{Software Fault-Tolerance:}
\begin{itemize}
\item Software fault detection
\item Rollback Recovery
\end{itemize}

\end{slide}
%-------------------------------------------------------------------------------

\begin{slide}
\MyHeading{Our Approach}

\begin{itemize}

%\item Develop techniques for locating global bugs.

%\begin{itemize}

%\item exponential number of global states in general

%\end{itemize}

\item Three abstractions defined: predicate detection, predicate
control and slicing.

\end{itemize}


\OneFigure{height=3.0cm}{testing}


\end{slide}
%-------------------------------------------------------------------------------

\begin{slide}
\MyHeading{Talk Outline}

~

\begin{itemize}
\item Motivation 
\item \mydesc{Predicate Detection} 
\item Computation Slicing
\item Predicate Control
\item Ongoing and Future Work
\end{itemize}
\end{slide}

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

\begin{slide}
\MyHeading{System Model}
\PutFigureLatex{2.0in}{model.pstex_t}

~

\textbf{computation:} a set of events ordered by ``happened before'' relation\\[0.5em]
\textbf{consistent cut:} subset of events that have been executed so
far \\[0.25em]
\begin{tabular}{@{\quad\quad}l}
e.g., $X$ is a consistent cut but $Y$ is not
\end{tabular}

%\vfill
%Assumptions: asynchronous communication
\end{slide}

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

\begin{slide}
\MyHeading{Predicate Detection Problem} 
\begin{itemize}
\item[] \mydesc{Predicate}: A global condition expressed using variables on processes\\[0.25em]
e.g., more than one process is in critical section,\\
there is no token in the system
\item[] \mydesc{Problem}: find a consistent cut that satisfies the given predicate \\[0.25em]
Exponential algorithm for general predicate \MyCite{Cooper and Marzullo 91}\\
Polynomial algorithm for conjunctive predicate \MyCite{Garg and Waldecker 91} 
\end{itemize} 
\vfill
\PutFigureLatex{2.75in}{detection.pstex_t}

%\textbf{The global predicate may express:}
%a software fault or a global breakpoint
\end{slide}

%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Motivation for Predicate Detection}
\mydesc{
{\em Dear Watson, you see but you do not observe...}\\
}


\begin{itemize}
\item Distributed Debugging, Testing
\begin{itemize}
\item stop when the predicate q is true\\
predicate q = (P1 is in critical section) and (P2 is in critical section).
\item Detect if the program violates any invariant
\end{itemize}
\item Fault-tolerance
\begin{itemize}
\item Monitoring while the program is operational
\end{itemize}
\item Distributed Active Rules
\begin{itemize}
\item On global condition $p$, trigger rule $a$
\end{itemize}
\item General paradigm for observing Distributed Algorithms
\begin{itemize}
\item Termination detection, deadlock detection, loss of token
\end{itemize}
\end{itemize}
\end{slide}

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

\begin{slide}
\MyHeading[0.5ex]{The Main Difficulty}
\PutFigureLatex{4.25in}{npcomplete.pstex_t}
% \begin{itemize}
% \item Exponential number of global states in general
%\item NP-complete for a conjunction of clauses such that each clause
% is a disjunction of at most two variables~~\MyCite{Mittal and Garg
% 01} \\[0.5em] e.g., $(x_1 \vee x_2) \wedge (x_3 \vee x_4) \wedge
% \cdots \wedge (x_{n-1} \vee x_n)$
%\end{itemize}
% \vspace*{1.0ex}
%\textbf{Problem:} Too many global states \\
Too many consistent cuts:
\begin{itemize}
\item[] A computation may contain as many as $O(k^n)$ consistent cuts \\[0.5em]
$k$: maximum number of events on a process \\
$n$: number of processes
\end{itemize}
\end{slide}
 
%-------------------------------------------------------------------------------


\begin{slide}
\MyHeading{Predicate Detection for Special Cases}
Exploit the structure of the predicate:
\begin{itemize}
\item \textbf{stable predicate:}~~\MyCite{Chandy and Lamport 85}
\\[0.25em] once the predicate becomes true, it stays true \\[0.25em]
e.g., deadlock
\item \textbf{unstable predicate:} 
\begin{itemize}
\item \textit{observer independent predicate}~~\MyCite
{Charron-Bost {\em et al\/} 95} \\[0.25em]
occurs in one interleaving $\implies$ occurs in all interleavings \\[0.25em]
e.g., any local predicate
\item \textit{relational predicate: $x_1 + x_2 + \cdots + x_n \geqslant
k$}~~\MyCite{Chase and Garg 95} \\[0.25em]
e.g., violation of mutual exclusion
\item \textit{linear predicate}~~\MyCite{Chase and Garg 95} \\[0.25em]
closed under intersection, e.g., conjunctive predicates such as
there is no leader in the system
\end{itemize}
\end{itemize}
\end{slide}

\begin{slide}
\MyHeading{Conjunctive Predicates}
A predicate that can be expressed as 
$l_1 \wedge l_2 \wedge \ldots \wedge l_n$, 
where $l_i$ is local to $P_i$.\\

Examples:
\begin{itemize}
\item \myblue{mutual exclusion problem}: (P1 in CS) and (P2 in CS)
\item \myblue{missing primary}: (P1 is secondary) and (P2 is secondary) and (P3 is secondary)
\end{itemize}
Detect errors that may be hidden in some run due to race conditions.
\end{slide}


\begin{slide}
\MyHeading{Importance of Conjunctive Predicates}

Sufficient for detection of any global 
\begin{itemize}
\item 
\myblue{boolean expression of local predicates}
which can be expressed as a disjunction of a small number of conjunctions.\\

{\em Example:}
$x,y$ and $z$ are in three different processes. Then,\\
$even(x) \wedge ((y<0) \vee (z > 6))$ \\
$\equiv$\\
$(even(x) \wedge (y<0))  \vee $
$(even(x) \wedge (z > 6))$ \\
\item
\myblue{predicate satisfied by only a small number of values}
{\em Example:} $x$ and $y$ are in different processes.\\
 $(x=y)$ is not a {\em local} predicate but $x$ and $y$ are binary.
\end{itemize}
\end{slide}

\begin{slide}
\MyHeading{Conditions for Conjunctive Predicates}
\begin{minipage}{4.0in}
\PutFigure{width=4.0in}{Predicate-Example}
\end{minipage}

Possibly $(l_1 \wedge l_2 \wedge \ldots  l_n)$ is true {\bf iff}
there exist $s_{i}$ in $P_i$ such that $l_i$ is true in state $s_{i}$, and
$s_{i}$ and $s_{j}$ are incomparable for distinct $i,j$. 
\end{slide}

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

\begin{slide}
\MyHeading{Tracking Causality: Clocks in a Distributed System}
\begin{minipage}{3.0in}
\PutFigure{width=3.0in}{VC1VectorAlgoFig}
%\centerline{\epsfbox{figs/VC1VectorAlgoFig.eps}}
%\epsffile{figs/run.p}
%\input{figs/VectorAlgoFig.latex}
%\vspace*{1.0in}
\end{minipage}

\myblue{Result}: $s$ happened before $t$ iff 
the vector at $s$ is less than the vector at $t$.
Vector Clocks \MyCite{Fidge 89, Mattern 89}


\end{slide}
%-------------------------------------------------------------------------------

\begin{slide}
\MyHeading{Dynamic Chain Clocks}
\myblue{Problem with vector clocks}: {scalability}\\
\\
\myblue{Idea}: {Computing the ``chains'' in an online fashion} \MyCite{Aggarwal and Garg 04}
\vfill

\begin{figure}[tp]
\begin{center}
  \includegraphics[width=3in,height=1in]{sliceFigures/relevant.eps}
\end{center}
\caption{(a) A computation with $4$ processes (b) The relevant subcomputation} 
\label{fig:relevant}
\end{figure}

\end{slide}
\begin{slide}
\MyHeading{Experimental Results}
 Simulation of a computation with 1\% relevant events\\
 Measured 
\begin{itemize}
\item number of components vs number of threads
\item total time overhead vs number of threads
\end{itemize}

\begin{figure*} 
  \begin{minipage}[t]{0.30\textwidth} 
  \includegraphics[width=2.5in,height=1.75in]{sliceFigures/threads-comp.eps}
  \setlength{\abovecaptionskip}{0pt}
  \label{fig:tc}
  \end{minipage}%
  \hspace{0.10\textwidth}
  \begin{minipage}[t]{0.30\textwidth} 
  \includegraphics[width=2.5in,height=1.75in]{sliceFigures/threads-time.eps}
  \label{fig:tt}
  \end{minipage}% 
\end{figure*}

\end{slide}


\begin{slide}
\MyHeading{Weak Conjunctive Predicates: Centralized Algorithm}
\begin{center}
\begin{minipage}{2.0in}
\PutFigure{width=2.0in}{checker}
\end{minipage}
\end{center}
%\begin{center}
%\setlength{\unitlength}{0.8pt}
%\begin{picture}(240,227)(0,0)
%\put(0,0){\special{psfile=checker.ps vscale=80 hscale=80}}
%\end{picture}
%\end{center}

\MyCite{Garg and Waldecker 92}
 Each non-checker process maintains its local $vector$ 
 and sends to the checker process the chain clock whenever
\begin{itemize}
\item local predicate is true
\item at most once in each message interval.
\end{itemize}
\end{slide}


\begin{slide}
\MyHeading{Overhead: Checker processes}
Space complexity:
$n$ queues, each containing at most $m$ vectors\\
\\
Time complexity:
\begin{itemize}
\item The algorithm for checker requires at most $O(n^2m)$
comparisons.
\item Any algorithm which determines whether
there exists a set of incomparable vectors of size $n$ in $n$ chains
of size at most $m$,
makes at least $mn(n-1)/2$ comparisons.
\MyCite{Garg and Waldecker 94}
\end{itemize}
\end{slide}



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

\begin{slide}
\MyHeading[0.5ex]{Predicate Detection in General}
\PutFigureLatex{2.00in}{full.pstex_t}
Construct the state-space (need to examine all consistent cuts)
\begin{itemize}
	\item \textit{breadth first manner}~~\MyCite{Cooper and
	Marzullo 91}  \\
	space-complexity: number of consistent cuts
	\item \textit{depth first manner}~~\MyCite{Alagar and
	Venkatesan 94}  \\
	space-complexity: number of events
	\item \textit{lexical order}~~\MyCite{Garg 03}  \\
	space-complexity: number of processes
\end{itemize}
\end{slide}

%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Talk Outline}

~

\begin{itemize}
\item Motivation 
\item Predicate Detection Problem
\item \mydesc{Computation Slicing}
%\begin{itemize}
%\item Main ideas and Definition
%\item Algorithm to compute slices
%\item Efficient Algorithm to compute slices
%\end{itemize}
\item Predicate Control
\item Ongoing and Future Work
\end{itemize}
\end{slide}

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

\begin{slide}
\MyHeading{The Main Idea of Computation Slicing}
\PutFigureLatex{4.25in}{idea1.pstex_t}
\end{slide}

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

\begin{slide}
\MyHeading{How does Computation Slicing Help?}
\PutFigureLatex{4.25in}{idea2.pstex_t}
\end{slide}

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

\begin{slide}
\MyHeading{Example}
Detect predicate $(x_1 * x_2 + x_3 < 5)$ $\wedge$ $(x_1 \geq 1)$ $\wedge$ $(x_3 \leq 3)$\\
\\
\\
\PutFigure{width=4.25in}{motivation1}
~\\
\\
Slice with respect to $(x_1 \geq 1) \wedge (x_3 \leq 3)$
\end{slide}

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

\begin{slide}
\MyHeading{Computation Slice} 
\textbf{computation slice:} a sub-computation such
that:~~\MyCite{Mittal and Garg 01}
\begin{enumerate}
\item it contains \textbf{all} consistent cuts of the computation
satisfying the given predicate, and
\item it contains the \textbf{least} number of consistent cuts \\
\end{enumerate}
\PutFigureLatex{3.5in}{slicing.pstex_t}
\end{slide}

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

 \begin{slide}
 \MyHeading{Example: Conjunctive Predicate}
 \vfill
 \PutFigureLatex{4.0in}{example1.pstex_t}

 ~  \\

 \vfill
 \end{slide}

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

\begin{slide}
\MyHeading{Example: Channel Predicate}
\vfill
\PutFigureLatex{4.0in}{example2.pstex_t}

~ \\

\vfill
\end{slide}

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

\remove{
 \begin{slide}
 \MyHeading{Third Example}
 \vfill
 \PutFigureLatex{3.25in}{example4.pstex_t}

 ~ \\

 \vfill
 \end{slide}

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

\begin{slide}
\MyHeading[1.5ex]{Slicing Example} 
\PutFigureLatex{4.4in}{example3.pstex_t}
\end{slide}

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

\begin{slide}
\MyHeading{Characterization of Consistent Cuts}
The set of consistent cuts of a computation forms a \textbf{distributive
lattice} % \\
% \MyCite{Garg and Mittal 01}
\begin{enumerate}
\item The set forms a \textbf{lattice} % \MyCite{Johnson and
				       % Zwaenepoel 88; Mattern 89} 
\begin{itemize}
\item if $X$ and $Y$ are consistent cuts then so are $X \cap Y$ and $X
\cup Y$ 
\item meet (infimum, greatest lower bound) ~$\rightarrow$~ intersection 
\item join (supremum, least upper bound) ~$\rightarrow$~ union 
\end{itemize}
\item The lattice is \textbf{distributive} 
\begin{itemize}
\item meet distributes over join \\[0.25em]
\end{itemize}
\end{enumerate}
\PutFigureLatex{3.75in}{lattice.pstex_t}
\end{slide}

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

\begin{slide}
\MyHeading{Join-irreducible Elements}
\centerline{A \textbf{join-irreducible element} has exactly one incoming
edge} % ~~\MyCite{Davey and Priestley 90}

~

\PutFigureLatex{2.65in}{join.pstex_t}
\end{slide}

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

\begin{slide}
\MyHeading[1.0ex]{Birkhoff's Representation Theorem}
\begin{center}
A distributive lattice can be \textbf{recovered exactly} from the set of its
join-irreducible elements
\end{center}
\vspace*{1.5ex}
\PutFigureLatex{4.2in}{birkhoff.pstex_t}
\end{slide}

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

\begin{slide}
\MyHeading[1.0ex]{What about a Subset of Consistent Cuts?}
\begin{minipage}{2.75in}
\PutFigureLatex{2.7in}{sublattice1.pstex_t}
\end{minipage}
\begin{minipage}{1.5in}
\begin{center}
$X$ in subset ~and~ \\[0.25em] $Y$ in subset \\[0.75em]
$\implies$ \\[0.75em]
$X \cap Y$ in subset ~and~ \\[0.25em]
$X \cup Y$ in  subset
\end{center}
\end{minipage}

~

\centerline{\textbf{sublattice:} subset of consistent cuts closed under
intersection and union}
\end{slide}

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

\begin{slide}
\MyHeading[1.0ex]{Representing a Sublattice}
\begin{center}
A sublattice of a distributive lattice is also a \textbf{distributive
lattice} \\
$\implies$ \\
A sublattice has a \textbf{succinct representation}
\end{center}
\vfill
\PutFigureLatex{4.25in}{sublattice2.pstex_t}
\vfill
\end{slide}

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

% \begin{slide}
% \MyHeading{Example Revisited}
% \vfill
% \PutFigureLatex{4.0in}{example2.pstex_t}

% ~ \\

% \vfill
% \end{slide}

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

\begin{slide}
\MyHeading{What if the Subset is not a Sublattice?}
\centerline{Add consistent cuts to complete the sublattice}
\vfill
\PutFigureLatex{3.75in}{sublattice3.pstex_t}
\vfill
\end{slide}

%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Computing the Slice}

~

\textbf{Algorithm:}
\begin{enumerate}
\item Find all consistent cuts that satisfy the predicate
\item Add consistent cuts to complete the sublattice
\item Find the basis elements of the sublattice
\end{enumerate}

~ \\ ~ \\

\centerline{\textit{Can we find the basis elements without
computing the sublattice?}} 
\end{slide}

%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Talk Outline}

~

\begin{itemize}
\item Motivation 
\item Predicate Detection Problem
\item Computation Slicing
\begin{itemize}
\item Main ideas and Definition
\item \mydesc{Efficient Algorithm to compute slices}
\end{itemize}
\item Predicate Control
\item Ongoing and Future Work
\end{itemize}
\end{slide}

%-------------------------------------------------------------------------------
}

\begin{slide}
\MyHeading{Regular Predicate} 
\textbf{regular predicate:} the set of consistent cuts satisfying the
predicate is closed under intersection and union~~\MyCite{Garg and
Mittal 01} 

~

Examples:
\begin{itemize}
\item conjunctive predicate---conjunction of local predicates
\item there are at most (or at least) $k$ messages in
transit from process $i$ to process $j$
\item every ``request'' message has been ``acknowledged''
in the system
\end{itemize}

~

The class of regular predicates is \textit{closed} under conjunction: \\[0.5em]
\centerline{If $b_1$ and $b_2$ are regular predicates then so is $b_1
\wedge b_2$}
\end{slide}

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

\begin{slide}
\MyHeading{Computing the Slice for Regular Predicate}
\PutFigureLatex{1.15in}{example5.pstex_t} 
\vspace*{0.75em}
\centerline{$b$ = ``no messages in transit''}

~

Algorithm: \\
\begin{tabular}{ll}
Step 1: & Compute the least consistent cut $L$ that satisfies $b$ \\
& $L = \{ \}$ \\
Step 2: & Compute the greatest consistent cut $G$ that satisfies $b$ \\
& $G = \{ u, v, w, x, y, z \}$
\end{tabular}
\end{slide}


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

\begin{slide}
\MyHeading{Computing the Slice for Regular Predicate}
Algorithm: \\
\begin{tabular}{ll}
Step 3: &  For every event $e \in G - L$, compute $L(e)$ defined as: \\
& (1) $L(e)$ contains $e$ \\
& (2) $L(e)$ satisfies $b$ \\
& (3) $L(e)$ is the least consistent cut satisfying (1) and (2)
\end{tabular}

~ \\

\begin{minipage}{2.0in}
\PutFigureLatex{1.15in}{example6.pstex_t} 
\end{minipage}
\begin{minipage}{2.25in}
$L(u) = \{ u, w \}$ \\
$L(v) = \{ u, v, w \}$ \\
$L(w) = \{ u, w \}$ (duplicate) \\
$L(x) = \{ u, w, x, y, z \}$ \\
$L(y) = \{ y \}$ \\
$L(z) = \{ u, w, x, y, z \}$ (duplicate)
\end{minipage}
\end{slide}

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

\begin{slide}
\MyHeading{Results}
Efficient polynomial-time algorithms for computing the slice for:
\begin{itemize}
\item \textbf{regular predicate:}~~\MyCite{Garg and
Mittal 01} 
\\[0.35em] \textit{time-complexity:}
\begin{itemize}
	\item general: $O(n^2m)$
	\item special cases (e.g., conjunctive predicate): $O(m)$
\end{itemize}
\item \textbf{general predicate:} \\
\textbf{Theorem:} Given a computation, if a predicate $b$ can be
detected efficiently then the slice for $b$ can also be
computed efficiently.
\MyCite{Mittal, Sen and Garg 02} 
\end{itemize}

~

$n$: number of processes \\
$m$: number of events
\end{slide}

\begin{slide}
\MyHeading{Experimental Evaluation: Dining Philosophers Verification}
\myblue{POTA}: Partial Order Trace Analyzer (based on slicing) \MyCite{Sen and Garg 03}\\
\myblue{SPIN}: A widely used model checking tool \MyCite{Holzmann 97}\\

\begin{figure}[htb] 
\centerline{
\includegraphics[width=1.8in]{sliceFigures/ddph.2.time.eps}
\includegraphics[width=1.8in]{sliceFigures/ddph.2.space.eps}
}
\end{figure}

SPIN: 250 seconds for n = 6, runs out of memory for $n > 6$.\\
POTA: can handle n= 200. Used 400 seconds.\\
\myblue{Predicate}: Two neighboring dining philosophers do not eat concurrently
\end{slide}

%\begin{slide}
%\MyHeading{Experimental Evaluation 2}
%\begin{figure}[htb] 
%\centerline{
%\includegraphics[width=2.0in]{sliceFigures/giop.4b.time.eps}
%\includegraphics[width=2.0in]{sliceFigures/giop.4b.space.eps}
%}
%\caption{GIOP verification results. SPIN runs out of memory for $n > 10$ 
%\protect\label{fig:giop.4b}} 
%\end{figure}
%\myblue{Predicate}: If the user received
%system exception then its request was processed at most once.

%\end{slide}
%-------------------------------------------------------------------------------

%\begin{slide}
%\MyHeading{Composing Two Slices}
%\vfill
%\PutFigureLatex{4.0in}{grafting1.pstex_t} 
%\vfill
%\end{slide}

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

%\begin{slide}
%\MyHeading{Composing Two Slices}
%\vfill
%\PutFigureLatex{4.0in}{grafting2.pstex_t} 
%\vfill
%\end{slide}

%-------------------------------------------------------------------------------
%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Talk Outline}

~

\begin{itemize}
\item Motivation 
\item Predicate Detection Problem
\item Computation Slicing
%\begin{itemize}
%\item Main ideas and Definition
%\item Algorithm to compute slices
%\item Efficient Algorithm to compute slices
%\end{itemize}
\item \mydesc{Predicate Control}
\item Ongoing and Future Work
\end{itemize}
\end{slide}
%-------------------------------------------------------------------------------

\begin{slide}
\MyHeading{Motivation for Control}

\mydesc{
{\em Who controls the past controls the future,
who controls the present controls the past...\\
\hspace*{3.5in} George Orwell, Nineteen Eighty-Four}.\\
}
\begin{itemize}
\item maintain global invariants or proper order of events\\
Examples: Distributed Debugging
\begin{itemize}
\item ensure that $busy_1 \vee busy_2$ is always true
\item ensure that $m_1$ is delivered before $m_2$
\end{itemize}
\item Resource Allocation
\begin{itemize}
\item maintain $\neg CS_1 \vee \neg CS_2$
\end{itemize}
\item Fault tolerance
\begin{itemize}
\item On fault, rollback and execute under control
\end{itemize}
\item Adaptive policies
\end{itemize}
\end{slide}



%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Rollback Recovery for Software Faults}
\PutFigureLatex{1.5in}{tolerance.pstex_t}

~

\textbf{Re-execution Problem:} 
\begin{itemize}
\item[] To re-execute in order to avoid a recurrence of a previously
detected failure 
	\begin{itemize}
	\item Progressive Retry~~\MyCite{Wang {\em et al\/} 97} 
	\item Controlled Re-execution~~\MyCite{Tarafdar and Garg 98}
	\end{itemize}
\end{itemize}
\end{slide}

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

\begin{slide}
\MyHeading{Controlled Re-execution}
\vfill
\PutFigureLatex{4.0in}{reexecution.pstex_t}

~

Add the synchronization necessary to maintain safety property
\begin{itemize}
\item[] e.g., mutual exclusion \\
\end{itemize}
\vfill
\end{slide}

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

\begin{slide}
\MyHeading{The Main Difficulty}
\vfill
\PutFigureLatex{4.0in}{reexecution1.pstex_t} 
\vfill
\end{slide}

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

\begin{slide}
\MyHeading{Results}
Efficient algorithms for computing the synchronization for: 
\begin{itemize}
\item \textbf{Locks}~~\MyCite{Tarafdar and Garg 98} \\
\begin{itemize}
\item \textit{time-complexity:} $O(nm)$ 
\end{itemize}
\item \textbf{disjunctive predicate}~~\MyCite{Mittal and Garg 00} \\[0.35em]
e.g., $(n-1)$-mutual exclusion 
\begin{itemize}
\item \textit{time-complexity:} $O(m^2)$ 
\item minimizes the number of synchronization arrows
\end{itemize}
\item \textbf{region predicate}~~\MyCite{Mittal and Garg 00} \\[0.35em]
e.g., virtual clocks of processes are ``approximately'' synchronized
\begin{itemize}
\item \textit{time-complexity:} $O(nm^2)$
\item maximizes the concurrency in the controlled computation
\end{itemize}
\end{itemize}

~\\
$n$: number of processes, $m$: number of events

\end{slide}

%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Ongoing and Future Work}
\begin{itemize}
\item \myblue{Predicate Detection}: Temporal logic predicates (\mydesc{Anurag Agarwal}), Online relational predicates (\mydesc{Selma Ikiz})
\item \myblue{Slicing}: Distributed and online algorithms (\mydesc{Vinit Ogale})
\item \myblue{Predicate Control}: Controlling message order (\mydesc{Arindam Chakraborty})
\item \myblue{Model Checking}: Based on predicate detection and slicing (\mydesc{Sujatha Kashyap})
\end{itemize}
\end{slide}
%-------------------------------------------------------------------------------
\begin{slide}
\MyHeading{Acknowledgments}
Collaborators on various ideas
\mydesc{Anurag Agarwal}
\myblue{
Craig M. Chase, Eddy Fromentin, 
Richard Kilgore,
}
\mydesc{
Ratnesh Kumar, James R. Mitchell, Neeraj Mittal, Venkat V. Murty,} 
\myblue{Michel Raynal,} 
\mydesc{Alper Sen, Chakarat Skawratonand, Ashis Tarafdar, Alex I. Tomlinson, and Brian Waldecker}
\end{slide}

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

\remove{
\begin{slide}
\MyHeading{Computing the Slice Using Composition}
\textbf{$\mathbf{k}$-local predicate for constant $\mathbf{k}$:}
depends on variables of at most $k$ processes
~~\MyCite{Mittal and Garg 02, TR-PDS-001}  
\\[0.35em] e.g.,
processes 1 and 2 do not agree on their votes 

~

\textbf{Theorem:} Given a computation, a $k$-local predicate can be
expressed as disjunction of at most $O(l^{k-1})$ conjunctive
predicates \\
\MyCite{Mittal and Garg 02, TR-PDS-001} 

~

\textit{time-complexity:} $O(n^2l^k)$


~

$n$: number of processes \\
$l$: maximum number of events on a process
\end{slide}

\begin{slide}

\MyHeading{Predicate Control: Problem Statement}


\textbf{Input:} A distributed computation $\comptn{E}{\precedes}$ and
a global predicate $B$.

\textbf{Output:} A distributed computation $\comptn{E}{\under}$,
if it exists, such
that:


\begin{itemize}

\item[\sf ~~~(1)] $\precedes \: \subseteq \: \under$, and 

\item[\sf ~~~(2)] every consistent cut of $\comptn{E}{\under}$ satisfies $B$.

\end{itemize}

~

Example: $B \equiv \neg critical_1 \vee \neg critical_2$

\vspace*{-3.0ex}

%\TwoFiguresV{height=2.25cm}{control}
%{\centerline{$\comptn{E}{\precedes}$}}
%{height=2.25cm}{controlled}
%{\centerline{$\comptn{E}{\under}$}}

\end{slide}

 \begin{slide}
 \MyHeading{Computing a Slice using Composition}
 For example: $(x_1 \vee x_2) \wedge (x_3 \vee x_4)$

 ~ 

 \PutFigureLatex{4.0in}{approximate.pstex_t}
 \end{slide}
}
%-------------------------------------------------------------------------------
\end{document}






} % \sf
