
\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}}
\newcommand{\AWAIT}[0]{\textbf{await}}

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

\title{Programaci\'on Concurrente \\
	Pr\'actico 3: Verificaci\'on (a posteriori) de Programas Concurrentes}
\author{J. Blanco, N. Wolovick}


\begin{document}
\maketitle

\begin{enumerate}

	
	\item{Demuestre que el siguiente multiprograma anotado es correcto.
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $x=0$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				$A:$ \= \{\=$ x=0 \vee x=2\}$ \\
					\> \>$a:=x$ \\
					\>$\{(a=0 \vee a=2) \wedge a\leq x\}$ \\
					\> \>$x:=a+1$ \\
					\>$\{x=1 \vee x=3\}$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				$B$: \= \{\=$ x=0 \vee x=1\}$ \\
					\> \> $x:=x+2$ \\
					\>$\{x=1 \vee x=2 \vee x=3\}$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $x=1 \vee x=3$} \\
			\hline
		\end{tabular}
		\end{center}
	}
	
	\item{Dado el siguiente multiprograma, muestre cuales son los posibles valores
		finales para $x$
		\[ \{u=0 \wedge v=1 \wedge w=2 \}
			\ x:=u+v+w \parallel u:=3 \parallel v:=4 \parallel w:=5\
			\{x\in S\}
		\]
	  \begin{enumerate}
	  	\item{si todas las asignaciones son at\'omicas,}
	  	\item{si no lo son y el \emph{rhs} se eval\'ua de izquierda a derecha.}
	  \end{enumerate}
	}

	\item{Elija las aserciones de forma tal que el multiprograma anotado resulte correcto
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $x=0$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: \= \{\=$ P_{0}\}$ \\
				\> \>$a:=x$ \\
				\>$\{P_{1}\}$ \\
				\> \>$x:=a+1$ \\
				\>$\{P_{2}\}$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \= \{\=$ Q_{0}\}$ \\
				\> \>$b:=x$ \\
				\>$\{Q_{1}\}$ \\
				\> \>$x:=b+2$ \\
				\>$\{Q_{2}\}$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $x=1 \vee x=2 \vee x=3$} \\
			\hline
		\end{tabular}
		\end{center}
	}

	\item{\label{xm1xm1}Demuestre el siguiente multiprograma\footnote{
		Notar como las variables auxiliares se utilizan para marcar el
		flujo de control del programa.}.
		\[
		\{x=0 \wedge \neg done\}\ x,done:=x+1,true \parallel x:=x+1\ \{x=2 \wedge done\}
		\]
	}

	
	\item{Los siguientes multiprogramas anotados son ejemplos que muestran la
		incompletitud del sistema de prueba de OG sin la Regla de las
		Variables Auxiliares.

		Demuestre, estos multiprogramas\footnote{Notar el primer ejemplo es un programas parelelo con variables disjuntas y sin sincronizaci\'on, luego la incompletitud se da con el operador $\parallel$.}
\footnote{El tercer multiprograma ya fue demostrado en el punto \ref{xm1xm1}, intente obtener una demostraci\'on alternativa, marcando completamente el flujo de programa.}.
		\[ \{x=y\}\ x:=x+1 \parallel y:=y+1\ \{x=y\} \]
		\[ \{true\}\ x:=x+2 \parallel x:=0\ \{x=0 \vee x=2\} \]
		\[ \{x=0\}\ x:=x+1 \parallel x:=x+1\ \{x=2\} \]	
	
	}

	
	\item{Demuestre la correcci\'on del siguiente multiprograma:
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $\neg x$} \\
			\hline
			A: $x:=true$ & B: $\IF\ x\rightarrow\ x:=false\ \FI$ \\
			\hline
			\multicolumn{2}{|l|}{Post: $\neg x$} \\
			\hline
		\end{tabular}
		\end{center}
	Tambi\'en verifique que si la componente $A$ la cambiamos por
	el par de instrucciones no-at\'omicas
	$A: x:=true; x:=true$
	la postcondici\'on $\neg x$ ya no se puede garantizar.
	}
	
	\item{Decore el siguiente multiprograma con aserciones local y globalmente correctas,
		de forma tal que verifiquen la pre/post.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $\neg b$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: \= \{\=$ P_{0}\}$ \\
				\> \>$\DO\ \neg b \rightarrow \SKIP\ \{P_{1}\}\ \OD$ \\
				\>$\{P_{2}\}$ \\
				\> \>$x:=y$ \\
				\>$\{P_{3}\}$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \= \{\=$ Q_{0}\}$ \\
				\> \>$y:=E$ \\
				\>$\{Q_{1}\}$ \\
				\> \>$b:=true$ \\
				\>$\{Q_{2}\}$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $x=y$} \\
			\hline
		\end{tabular}
		\end{center}
	}
	
	%AO91 pag.160
	\item{Demostrar el siguiente algoritmo paralelo \emph{coarse-grained} que
		encuentra un cero de la funci\'on $f:\mathcal{Z}\rightarrow\mathcal{N}$.
		\newline
		\begin{small}
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $\langle \exists u: u\in \mathcal{Z}: f.u=0\rangle \wedge \neg found \wedge x=0 \wedge y=1$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: \= $\{$ \= $Inv: p_0 \}$ \\
				\> \>$\DO$ \= $\neg found \rightarrow$ \\
				\> \>		\> $\{q_0\}$ \\
				\> \>		\> $\langle$ \= $x:=x+1;$ \\
				\> \>		\>	\> $\IF\ f.x=0 \rightarrow found:=true$ \\
				\> \>		\> 	\> $\Box f.x\neq 0\rightarrow \SKIP$ \\
				\> \>  		\>	\> $\FI$\\
				\> \>		\> $\rangle$ \\
				\> \>$\OD$ \\
				\>$\{p_0 \wedge found\}$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \= $\{$ \= $Inv: p_1 \}$ \\
				\> \>$\DO$ \= $\neg found \rightarrow$ \\
				\> \>		\> $\{q_1\}$ \\
				\> \>		\> $\langle$ \= $y:=y-1;$ \\
				\> \>		\>	\> $\IF\ f.y=0 \rightarrow found:=true$ \\
				\> \>		\> 	\> $\Box f.y\neq 0\rightarrow \SKIP$ \\
				\> \>  		\>	\> $\FI$\\
				\> \>		\> $\rangle$ \\
				\> \>$\OD$ \\
				\>$\{p_1 \wedge found\}$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $f.x=0 \vee f.y=0$} \\
			\hline
		\end{tabular}
		\end{center}
		\end{small}
		Donde
		\[ p_0\equiv 0\leq x \wedge (found \Rightarrow (0<x \wedge f.x=0)\vee(y\leq0 \wedge f.y=0)) \wedge (\neg found \wedge 0<x \Rightarrow f.x\neq 0) \]
		\[ p_1\equiv y\leq 1 \wedge (found \Rightarrow (0<x \wedge f.x=0)\vee(y\leq0 \wedge f.y=0)) \wedge (\neg found \wedge y\leq 0 \Rightarrow f.y\neq 0) \]
		Encontrar las aserciones $q_0$, $q_1$ y demostrar correcto el multiprograma. 
	}

	%Concurrent Vector Writing (chp10?) de WF99
	\item{Al siguiente algoritmo se lo conoce como \Idiom{Concurrent Vector Writing}. Demu\'estrelo utilizando la teor\'{\i}a\footnote{Es un ejercicio interesante comparar la verificacion \Idiom{a posteriori} que se realizar\'a, respecto a la construcci\'on del programa como se ver\'a en clase.}.
		\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$ \\
				\> \>		\> $\IF\ i<j \rightarrow \SKIP\ \FI;$ \\
				\> \>		\> $a.i:=0;$ \\
				\> \>		\> $i:=i+1$ \\
				\> \>$\OD$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: \= \=$\DO$ \= $j\neq N \rightarrow$ \\
				\> \>		\> $a.j:=1;$ \\
				\> \>		\> $j:=j+1$ \\
				\> \>$\OD$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{Post: $\langle \forall k: 0\leq k<N: a.k=0\rangle$} \\
			\hline
		\end{tabular}
		\end{center}
		\end{small}
	}

\end{enumerate}

\end{document}
