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

\movedUpBody{-0.75in}{Synchronization Fault Avoidance System}

\begin{center}
\vspace{1in}
	\begin{figure*}
	\centerline{\epsfbox{Figures/fig1-operation.eps}}
	\end{figure*}
\end{center}
%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{Avoiding Synchronization Faults}

\vspace{0.3in}
\begin{small}
\begin{center}
\Black{\begin{itemize}
	\item Data Race Avoidance:
	\Blue{\begin{itemize}
		\item  no two concurrent events access the same object, where
             one access is a write
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig18-race-avoidance.eps}}
		\end{figure*}
		\item  Off-line Mutual-exclusion with Read-Write Locks\\
				\PineGreen{[Tarafdar and Garg 98: in progress]}
	\end{itemize}}
\end{itemize}}
\end{center}
\end{small}

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

\movedUpBody{-0.75in}{Avoiding Synchronization Faults}

\vspace{0.3in}
\begin{small}
\begin{center}
\Black{\begin{itemize}
	\item Deadlock Avoidance: 
	\Blue{\begin{itemize}
		\item no set of concurrent events wait for one another (in a cycle) to give up a resource 
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig19-deadlock-avoidance.eps}}
		\end{figure*}
		\item Off-line Mutual-exclusion with Independent Locks\\
				\PineGreen{[Tarafdar and Garg 98: in progress]}
	\end{itemize}}
\end{itemize}}
\end{center}
\end{small}

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

\movedUpBody{-0.75in}{Avoiding Synchronization Faults}

\vspace{0.3in}
\begin{small}
\begin{center}
\Black{\begin{itemize}
	\item Server Unavailability Avoidance:
	\Blue{\begin{itemize}
		\item all servers are never unavailable concurrently
		\item \Tan{$(avail_1\ \vee\ avail_2\ \vee\ \cdots\ avail_n)$} \\
		where: \Tan{$avail_i$}: server $i$ is available for critical service
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig20-server-unavail-avoidance.eps}}
		\end{figure*}
		\item Off-line Disjunctive Predicate Control: \PineGreen{[Tarafdar and Garg 98: IPPS/SPDP]}
	\end{itemize}}
\end{itemize}}
\end{center}
\end{small}

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

\movedUpBody{-0.75in}{Off-line Predicate Control}

\vspace{0.3in}
\begin{center}
\Black{\begin{itemize}
	\item ``Given a concurrent computation and a predicate, add synchronizations
         to the computation to ensure that the predicate is always true, 
			if possible''
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig21-pred-control-defn.eps}}
		\end{figure*}
	\item Off-line Predicate Control is NP-Complete \\ 
				\PineGreen{[Tarafdar and Garg 98: IPPS/SPDP]}
\end{itemize}}
\end{center}

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

\movedUpBody{-0.75in}{Off-line Disjunctive Predicate Control}

\vspace{0.3in}
\begin{center}
\Black{\begin{itemize}
	\item ... is impossible iff there is an overlapping set of false intervals.\\
		\PineGreen{[Garg and Waldecker 96]}
		\vspace{0.5in}
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig22-overlap-intervals.eps}}
		\end{figure*}
\end{itemize}}
\end{center}

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

\movedUpBody{-0.75in}{Off-line Disjunctive Predicate Control}

\vspace{0.3in}
\begin{center}
\Black{\begin{itemize}
	\item Key Observation:
	\Blue{\begin{itemize}
		\item A chain of true intervals from the beginning to the end 
            ensures that every consistent global state satisfies the 
				predicate.
	\end{itemize}}
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig23-true-chain.eps}}
		\end{figure*}
	\item Algorithm: construct a chain while ensuring no cycles. \\
				\PineGreen{[Tarafdar and Garg 98: IPPS/SPDP]}
\end{itemize}}
\end{center}

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

\movedUpBody{-0.75in}{Off-line Mutex Predicate Control}

\vspace{0.3in}
\begin{center}
\Black{\begin{itemize}
	\item Define a relation \OrangeRed{precedes} on critical sections:
	\Blue{\begin{itemize}
		\item critical section $x$ precedes critical section $y$ iff: \\
				$x$ contains event $a$, and $y$ contains event $b$, and
				$a$ happened before $b$.
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig24-precedes-defn.eps}}
		\end{figure*}
	\end{itemize}}
	\item Note: there may be cycles
	\item Off-line Mutex Predicate Control is impossible iff there
         is a cycle in the critical sections. \PineGreen{[Tarafdar and Garg 98: in progress]}
\end{itemize}}
\end{center}

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

\movedUpBody{-0.75in}{Off-line Mutex Predicate Control}

\vspace{0.3in}
\begin{center}
\Black{\begin{itemize}
	\item Algorithm: 
	\Blue{\begin{itemize}
		\item Linearize the partial order of critical sections
		\item Add a synchronization from one critical section to the next.
	\end{itemize}}
		\vspace{0.5in}
		\begin{figure*}
		\centerline{\epsfbox{Figures/fig25-linearize.eps}}
		\end{figure*}
\end{itemize}}
\end{center}

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

\movedUpBody{-0.75in}{Extensions to Off-line Mutex Predicate Control}

\vspace{0.3in}
\begin{center}
\Black{\begin{itemize}
	\item Off-line Mutex Predicate Control with Read-Write Locks 
	\Blue{\begin{itemize}
		\item ... is impossible iff there is a cycle in the critical sections
            where at least one critical section is write-locked.
		\item Algorithm: 
		\Tan{\begin{itemize}
			\item Find strongly connected components (SCC's) of precedes graph.
			\item Linearize the partial order of SCC's.
			\item Add synchronizations from all members of one SCC to all members
					of next SCC.
		\end{itemize}}
	\end{itemize}}
	\item Off-line Mutex Predicate Control with Independent Locks:
	\Blue{\begin{itemize}
		\item ... along similar lines
	\end{itemize}}
\end{itemize}}
\end{center}

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