
\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 6: Derivaci\'on y Transformaci\'on}
\author{J. Blanco, N. Wolovick}


\begin{document}
\maketitle

\begin{enumerate}

	\item{Esta es la versi\'on 3 de la derivaci\'on del algoritmo
		\Idiom{Concurrent Vector Writing}.
		\newline
		\begin{small}
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $i=0 \wedge j=0$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: \= $\DO\ $\=$i\neq N \rightarrow $ \\
				   \>	 \>$x.i:=0;$ \\
				   \>	 \>$\{x.i=0?\}$ \\
				   \>	 \>$i:=i+1$ \\
				   \>$\OD$ \\
				   \>$\{i=N\}$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \= $\DO\ $\=$j\neq N \rightarrow $ \\
				   \>	 \>$\{i\leq j?N_0\}$ \\
				   \>	 \>$x.j:=1;$ \\
				   \>	 \>$j:=j+1$ \\
				   \>$\OD$ \\
				   \>$\{j=N\}$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Inv: $\langle \forall k : 0\leq k<i : x.k=0\rangle$} \\
			\hline
			\multicolumn{2}{|l|}{Post: $\langle \forall k : 0\leq k<N : x.k=0\rangle$} \\
			\hline
		\end{tabular}
		\end{center}
		\end{small}
		\begin{enumerate}
			\item{Muestre que si continuamos la derivaci\'on fortaleciendo ligeramente la aserci\'on
			de la Nota 0 a $\{i<j\}$, el multiprograma resultante tiene riesgo de deadlock
			}
			\item{Realice una derivaci\'on alternativa, asegurando la Nota 0 con un skip
			      guardado en $B$. Demuestre que el resultado obtenido no sufre de deadlock.
			}
		\end{enumerate}
	}

	%WF99-21
	\item{Considere un multiprograma con 23 componentes de tipo $A$ y 47
		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: $*[s:=s-1]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		Sincronice las componentes usando s\'olo skips guardados para que $0\leq s\leq 100$
		sea un invariante del sistema\footnote{Hint: vea el ejercicio 4 del pr\'actico 5.}.
	}


	%WF99-37,38
	\item{Sincronice las 2 componentes del siguiente multiprograma de manera tal
		que la postcondici\'on implique $x=0 \wedge y=1$.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A:\ \= \ \= $x:=0$ \\
				  \> $;$ \> $y:=0$ 
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B:\ \= \ \= $x:=1$ \\
				  \> $;$ \> $y:=1$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}

		Ahora ataque el problema para $N=3$, es decir, agregue sincronizaci\'on
		al multiprograma de manera tal que la postcondici\'on implique 
		$x=0 \wedge y=1 \wedge z=2$.
		\newline
		\begin{small}
		\begin{center}
		\begin{tabular}{|l|l|l|}
			\hline
			\multicolumn{3}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A:\ \= \ \= $x:=0$ \\
				  \> $;$ \> $y:=0$ \\
				  \> $;$ \> $z:=0$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B:\ \= \ \= $x:=1$ \\
				  \> $;$ \> $y:=1$ \\
				  \> $;$ \> $z:=1$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				C:\ \= \ \= $x:=2$ \\
				  \> $;$ \> $y:=2$ \\
				  \> $;$ \> $z:=2$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		\end{small}
	}


	%WF99-19 -- JAVIER --



	%WF99-20



	%WF99-pag117
	\item{Reducir el grado de atomicidad para el siguiente multiprograma
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $x \wedge y$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: $*$ \= $[$ \= $\IF\ x \rightarrow\SKIP\ \FI$ \\
					\> $;$\> $x,y:=\neg y,true$ \\
					\> $]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: $*$ \= $[$ \= $\IF\ y \rightarrow\SKIP\ \FI$ \\
					\> $;$\> $y,x:=\neg x,true$ \\
					\> $]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		\begin{enumerate}
			\item{Demostrar que la soluci\'on no sufre de riesgo de deadlock total.
			}
			\item{?`Podemos asegurar progreso individual\footnote{Hint: pensar en las anotaciones --ocultas-- del multiprograma.}?
			}
		\end{enumerate}
	}


	%Inventado
	\item{La siguiente es la \Idiom{computation proper} de una barrera de $N$ procesos, donde $e.i$ y $x.i$ son variables auxiliares que marcan respectivamente la entrada y salida de la barrera.
		\newline
		\begin{center}
		\begin{tabular}{|l|}
			\hline
			Pre: $\langle\forall i:0\leq i<N:\neg e.i \wedge \neg x.i \rangle$ \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				Comp.k: \= \\
					\> \= $\vdots$ \\
					\> $e.k:=true;$ \\
					\> $barrera.k$ \\
					\> $x.k:=true;$ \\
					\> \> $\vdots$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			Inv: $\langle\forall i: 0\leq i<N: x.i \Rightarrow
					\langle \forall j: 0\leq j<N: e.i\rangle \rangle$ \\
			\hline
		\end{tabular}
		\end{center}
		\begin{enumerate}
			\item{Derive la barrera del contador.
			}
			\item{Derive la barrera del contador implementada con $N$ bits. Genere primero una versi\'on \Idiom{coarse grained}, para luego aplicar lemas de reducci\'on del grado de atomicidad y obtener una versi\'on \Idiom{one-point}.
			}
			\item{Compare en t\'erminos pr\'acticos las dos implementaciones.
			}
		\end{enumerate}
	}


	\item{A partir de la siguiente \Idiom{computation proper}, crear sentencias que establezcan la Post.
		El resultado deber\'a ser sim\'etrico y \Idiom{one-point}.
		Notar que esta es la especificaci\'on de un problema de \textbf{elecci\'on de l\'{\i}der}.
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				$C.i$: \= $y.i:=B.i$ 
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				$C.j$: \= $y.j:=B.j$ 
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $N.y.i + N.y.j = 1$? } \\
			\hline
		\end{tabular}
		\end{center}
	}
\end{enumerate}

\end{document}
