\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\'{a}ctico 4: Manejando la Complejidad}
\author{J. Blanco, N. Wolovick}


\begin{document}
\maketitle

\begin{enumerate}

	%WF99-1
	\item{Demuestre la correcci\'on de la postcondicion en el siguiente
		multiprograma\footnote{Utilize que $x.(-1)\leq 0$.}.
		\newline
		\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 47 \rightarrow$  \\
				\> \> $i:=i+1$ \\
				\>$\OD$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \= $\DO$ \= $j\neq 47 \rightarrow$  \\
				\> \> $x.j:=i;$ \\
				\> \> $j:=j+1$ \\
				\>$\OD$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $\langle\forall k : 1\leq k<47 : x.(k-1)\leq x.k\rangle$} \\
			\hline
		\end{tabular}
		\end{center}
	}

		
	%WF99-0
	\item{Encuentre enteros $C$ y $D$ para que en el siguiente multiprograma
		el predicado $x\leq y+C \wedge y\leq x+D$ resulte invariante.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $x=0 \wedge y=0$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: $*$\=$[$\=$x:=y;$ \\
				\> \> $x:=x+1$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: $*$\=$[$\=$y:=x;$ \\
				\> \> $y:=y+1$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
	}


	%WF99-11
	\item{Muestre la invariancia de $x+y\leq z$ en el siguiente multiprograma\footnote{Hint:
		se puede ver como el 1er lema de topolog\'{\i}a}. ?`Qu\'e pasa si el multiprograma contiene varias
		instancias de $A$ y $B$?
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $x=0 \wedge y=0 \wedge z=0$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: $*$\=$[$\=$y:=y-1;$ \\
				\> \> $x:=x+1$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: $*$\=$[$\=$z:=z+1;$ \\
				\> \> $y:=y+1$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
	}


	%????De donde salio?
	\item{Demuestre la siguiente versi\'on del teorema ``general'' de topolog\'{\i}a\footnote{Hint: se puede demostrar utilizando 3 veces el 1er lema de topolog\'{\i}a.}.
		\newline
		\begin{center}
		\begin{tabular}{|l|}
			\hline
			Pre: $x=0 \wedge y=0$ \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				Comp.i: $*$\=$[$\=$\{$ \=$y:=y+1$ \kill
				Comp.i: $*$\>\>$[$\> $y:=y+1;$ \\
				\> \> $\{x<y\}$ \\
				\> \> \> $x:=x+1$ \\
				\> \> \> $x:=x-1$ \\
				\> \> $\{x<y\}$ \\
				\> \> \> $y:=y-1$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			Inv: $0\leq x \wedge x\leq y$ \\
			\hline
		\end{tabular}
		\end{center}
	}


	%WF99-3	
	\item{Demuestre el siguiente multiprograma donde los \'angulos $\langle\ \rangle$ representan
		la atomicidad y $\downarrow$ es el operador binario de m\'{\i}nimo.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $true$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: \=$\IF$ \=$\langle x\leq y\rangle \rightarrow \langle m:=x\rangle $ \\
				   \>$\Box$\>$\langle y\leq x\rangle \rightarrow \langle m:=y\rangle $ \\
				   \>$\FI$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \=$\langle m:=x\rangle$ \\
				   \>$\IF$ \=$\langle m\leq y\rangle \rightarrow \SKIP $ \\
				   \>$\Box$\>$\langle y\leq m\rangle \rightarrow \langle m:=y\rangle $ \\
				   \>$\FI$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $m=x\downarrow y$} \\
			\hline
		\end{tabular}
		\end{center}
	}


	%WF99-10	
	\item{Muestre la exclusi\'on mutua entre $cs.A$ y $cs.B$ en el siguiente multiprograma\footnote{Deber\'a pensar en como expresar la noci\'on de exclusi\'on mutua.},
	donde s\'olo suponemos \'atomica la evaluaci\'on de las guardas y las asignaciones\footnote{Es decir que el $\DO\ldots \OD$ puede ser interrumpido luego de haber evaluado la guarda.}.

	Piense si adem\'as de cumplir con la propiedad de seguridad, tambi\'en tiene buenas propiedades de progreso como las indicadas en cualquier libro de texto de Sistemas Operativos.

	Investigue si es posible utilizar este algoritmo tipo \Idiom{spin-lock} en arquitecturas x86.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $\neg x \wedge \neg y$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: $*$ \= $[\ $\=$\DO\ \neg x \rightarrow x:=\neg y\ \OD$ \\
				\> $;$ \> $\ cs.A$ \\
				\> $;$ \> $x:=false$ \\
				\> $]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: $*$ \= $[\ $\=$\DO\ \neg y \rightarrow y:=\neg x\ \OD$ \\
				\> $;$ \> $\ cs.B$ \\
				\> $;$ \> $y:=false$ \\
				\> $]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
	}
	
\end{enumerate}

\end{document}
