
\documentclass[a4paper]{article}

\setlength\textwidth{6.5in}
\setlength\oddsidemargin{0in}
\setlength\evensidemargin{0in}

%\setlength\headheight{0in}
%\setlength\headsep{0in}

%\setlength\topmargin{-0.5in}
%\addtolength{\textheight}{0.5in}


\newcommand{\SIG}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\Idiom}[1]{\textsl{#1}}
\newcommand{\IF}[0]{\textbf{if}}
\newcommand{\FI}[0]{\textbf{fi}}
\newcommand{\SKIP}[0]{\textbf{skip}}
\newcommand{\DO}[0]{\textbf{do}}
\newcommand{\OD}[0]{\textbf{od}}

\usepackage{latexsym}
\usepackage[spanish]{babel}

\title{Programaci\'on Concurrente \\ Pr\'actico 5: Sincronizaci\'on y Progreso}
\author{J. Blanco, N. Wolovick}


\begin{document}

\maketitle

\begin{enumerate}

	\item{Para cada uno de los siguientes programas, \textbf{analice} sus propiedades de progreso\footnote{Suponga atomicidad en todas las asignaciones y sentencias guardadas. La composici\'on paralela tiene menor precedencia que la secuencial. La notaci\'on $[b]$ es el skip guardado $\IF\ b\rightarrow\SKIP\ \FI$.}.
		\begin{enumerate}
			\item{$\{\neg b\}\ b:=true \parallel [b];b:=false\ \{\neg b\}$
			}
			\item{$\{\neg b\}\ b:=true \parallel b:=false;[b]\{b\}$
			}
			\item{$\{\neg b\}\ b:=true;b:=false \parallel[b]\{?\}$
			}
			\item{$\{\neg b \wedge \neg c\}\ b:=true;[c]\parallel\ c:=true;[b]\{b\wedge c\}$
			}
			\item{$\{\neg b\}\ *[b:=true; b:=false] \parallel [b]$
			}
		\end{enumerate}
	}
	
	\item{Demuestre progreso en los siguientes multiprogramas
	  \begin{enumerate}
	    \item{\label{ej:vigualq}
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: \= \ \  \= $v:=q$ \\
				   \> $;$ \> $\IF\ v=p \rightarrow\ \SKIP\ \FI$ \\
				   \> $;$ \> $v:=q$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \= \ \ \= $v:=p$ \\
				   \> $;$ \> $\IF\ v=q \rightarrow\ \SKIP\ \FI$ \\
				   \> $;$ \> $v:=p$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $?$} \\
			\hline
		\end{tabular}
		\end{center}
	    }
	    \item{
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $x=y$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: $*$\=$[$\ \= $\IF\ x\neq y \rightarrow\ \SKIP\ \FI$ \\
				      \> $;$  \> $x:=x+1$ \\
				      \> $]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: $*$\=$[$\ \= $\IF\ x=y \rightarrow\ \SKIP\ \FI$ \\
				      \> $;$  \> $y:=y+1$ \\
				      \> $]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Inv: $?$} \\
			\hline
		\end{tabular}
		\end{center}
	    }
	  \end{enumerate}
	}
	
	%inventado
	\item{En [AO91] plantea la siguiente regla para demostrar \Idiom{deadlock freedom}
		(individual y total) para programas paralelos con variables compartidas y
		sincronizaci\'on.
		\begin{quotation}
			Considere un programa paralelo
			$S \equiv [S_{1}\parallel \ldots \parallel S_{n}]$.
			
			\begin{enumerate}
			  \item{Una tupla $(R_{1},\ldots, R_{n})$ de sentecias se denomina
				\emph{deadlock potencial de $S$} si se dan las siguientes
				condiciones
			 	\begin{itemize}
			 	  \item{Para todo $i\in \{1,\ldots,n\}$, $R_{i}$ es una sentencia guardada
			 	  en la componente $S_{i}$ o el s\'{\i}mbolo $E$ que denota la sentencia
			 	  vac\'{\i}a y representa la terminaci\'{o}n de $S_{i}$,
			 	  }
			 	  \item{para alg\'un $i\in\{1,\ldots,n\}$, $R_{i}$ es una sentencia guardada.
			 	  }
			 	\end{itemize}
			  }
			  \item{Dada un esquema de prueba estandard de correcci\'on parcial para no interferencia
			  $\{p_i\}S_{i}^{*}\{q_i\}$, $i\in\{1,\ldots,n\}$,
			  con cada deadlock potencial de $S$ asociamos una tupla
			  $(r_{1},\ldots,r_{n})$ de aserciones, poniendo para $i\in\{1,\ldots,n\}$:
			  \begin{itemize}
 			    \item{$r_{i}\equiv pre(R_{i}) \wedge \neg B$ si $R_{i}\equiv \IF\ B\rightarrow S\ \FI$
			    }
			    \item{$r_{i}\equiv q_{i}$ si $R_{i}\equiv E$.
			    }
			  \end{itemize}
			  }
			\end{enumerate}
			
			Si podemos demostrar $\neg \bigwedge_{i=1}^{n}r_{i}$ para \underline{todas} las tuplas de aserciones
			$(r_{1},\ldots,r_{n})$, ninguno de los deadlocks potenciales pueden ocurrir, estableciendo
			\Idiom{deadlock freedom}.
		\end{quotation}
		Utilizando esta regla demuestre ausencia de deadlock para
		\begin{enumerate}
			\item{el ejercicio (\ref{ej:vigualq}) de este pr\'actico,}
			\item{el algoritmo de \Idiom{Concurrent Vector Writing} derivado en clase,}
			\item{la resoluci\'on del ejercicio 1 del primer pr\'actico.
				\newline
				\begin{scriptsize}
				\begin{center}
				\begin{tabular}{l|l}
				        \begin{minipage}[t]{1in}
				        \begin{tabbing}
				                $A:$ \= \ \ \= $y:=false$ \\
						\> $;$ \> $x:=true$ \\
				                \> $;$ \> $\IF\ y \rightarrow \SKIP\ \FI$ \\
						\> $;$ \> $x:=true$
				        \end{tabbing}
				        \end{minipage}
				        &
				        \begin{minipage}[t]{1in}
				        \begin{tabbing}
				                $B:$ \= \ \ \= $x:=false$ \\
						\> $;$ \> $y:=true$ \\
				                \> $;$ \> $\IF\ x \rightarrow \SKIP\ \FI$ \\
						\> $;$ \> $y:=true$
				        \end{tabbing}
				        \end{minipage}
				\end{tabular}
				\end{center}
				\end{scriptsize}
			}
		\end{enumerate}
	}

	%WF99-14
	\item{Considere un multiprograma con 1 componente de tipo $A$ y 47 componentes de tipo $B$.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $s=0$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: $*[s:=s+1]$ \\
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: $*$\=$[\ $\=$\IF\ K\leq s \rightarrow \SKIP\ \FI$ \\
				\> $;$ \> $s:=s-1$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		Derive para que valores de $K$ se cumple el invariante del sistema $0\leq s$.
	}

	%Inventado?	
	\item{Demuestre el progreso de las $N$ componentes del multiprograma	
		\newline
		\begin{center}
		\begin{tabular}{|l|}
			\hline
			Pre: $\langle\forall q :: x.q=0\rangle$ \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				Comp.p: $*$\=$[\ $\=$\IF\ \langle\forall q :: x.p\leq x.q\rangle \rightarrow \SKIP\ \FI$ \\
				\> $;$ \> $x.p:=x.p+1$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
	}
	

	%WF99-9	
	\item{\emph{``No siempre debilitar las guardas de un $\IF$ o fortalecer
		las de un $\DO$ ayuda al progreso''}.
		\begin{enumerate}
		\item{
		Muestre la terminaci\'on del siguiente programa:
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A:$\ \DO\ x\vee y \rightarrow x:=false\ \OD$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B:$\ \DO\ x\vee y \rightarrow y:=false\ \OD$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		}
		\item{
		Pero la terminaci\'on no se garantiza si cambiamos a \ldots
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A:$\ \DO\ y \rightarrow x:=false\ \OD$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B:$\ \DO\ x \rightarrow y:=false\ \OD$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		}
		\item{
		Analice la situaci\'on para esta \'ultima modificaci\'on.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A:$\ $\=$\DO\ y \rightarrow x:=false\ \OD;$ \\
				      \>$x:=false$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B:$\ $\=$\DO\ x \rightarrow y:=false\ \OD;$ \\
				      \>$y:=false$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		}
		\end{enumerate}
	}

\end{enumerate}

\end{document}
