
\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}
\usepackage{fancyvrb}
\usepackage{color}

\title{Programaci\'on Concurrente \\ Examen para la casa}
\author{J. Blanco, N. Wolovick}


\begin{document}
\maketitle

\begin{enumerate}

	\item{\cite[ej.24]{wf:method}
	  \begin{enumerate}
	  	\item{Para el siguiente multiprograma de $N$ componentes,
		  con $2\!\leq\!N$, demuestre que el n\'umero de componentes ejecutando los
		  fragmentos $S$ es a lo m\'as $N\!-\!1$.
		  \newline
		  \begin{center}
		  \begin{tabular}{|l|}
			\hline
			Pre: $true$ \\
			\hline
			\begin{minipage}[t]{3in}
			\begin{tabbing}
				Comp.p: $*$ \= $[$ \= $v:=p$ \\
					\>$;$	\> $\IF\ v\neq p \rightarrow \SKIP\ \FI$ \\
					\>$;$	\> $S.p$ \\
					\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		  \end{tabular}
		  \end{center}
		}
		
		\item{Demuestre que la misma propiedad vale en el siguiente multiprograma:
		  \newline
		  \begin{center}
		  \begin{tabular}{|l|}
			\hline
			Pre: $\langle \forall q :: \neg x.q\rangle$ \\
			\hline
			\begin{minipage}[t]{3in}
			\begin{tabbing}
				Comp.p: $*$ \= $[$ \= $x.p:=true$ \\
					\>$;$	\> $\IF\ \langle \exists q : q\neq p: \neg x.q\rangle
							\rightarrow \SKIP\ \FI$ \\
					\>$;$	\> $S.p$ \\
					\>$;$	\> $x.p:=false$ \\
					\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		  \end{tabular}
		  \end{center}
		}
		
		\item{Explique si la situaci\'on se modifica cuando cambiamos las componentes
			a\footnote{la atomicidad es l\'{\i}nea a l\'{\i}nea.}:\\
		  \newline
		  \begin{center}
		  \begin{tabular}{|l|}
			\hline
			Pre: $\langle \forall q :: \neg x.q\rangle$ \\
			\hline
			\begin{minipage}[t]{3in}
			\begin{tabbing}
				Comp.p: $*$ \= $[$ \= $x.p:=true$ \\
					\>$;$	\> $v:=p$ \\
					\>$;$	\> $\IF\ v\neq p \vee \langle \exists q : q\neq p: \neg x.q\rangle
							\rightarrow \SKIP\ \FI$ \\
					\>$;$	\> $S.p$ \\
					\>$;$	\> $x.p:=false$ \\
					\>$]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		  \end{tabular}
		  \end{center}
		}
	  \end{enumerate}
	}


	\item{\cite[ej.32]{wf:method} Elimine las multiasignaciones utilizando Fortalecimiento de Guarda.
		\newline
		\begin{center}
		\begin{tabular}{|l|l|l|}
			\hline
			\multicolumn{3}{|l|}{Pre: $x \wedge \neg y \wedge \neg z$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A: $*$\=$[$\=$\IF\ x \rightarrow \SKIP\ \FI;$ \\
				\> \> $x,y:=false, true$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B: $*$\=$[$\=$\IF\ y \rightarrow \SKIP\ \FI;$ \\
				\> \> $y,z:=false, true$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				C: $*$\=$[$\=$\IF\ z \rightarrow \SKIP\ \FI;$ \\
				\> \> $z,x:=false, true$ \\
				\>$]$
			\end{tabbing}
			\end{minipage}			
			\\
			\hline
		\end{tabular}
		\end{center}
	}
	
	
	\item{\cite[ej.4.32]{and:2000}\cite{ewd:703} Tres tipos de procesos comparten el acceso a una lista ligada: los que buscan (\Idiom{searchers}), los que insertan (\Idiom{inserters}) y los que borran (\Idiom{deleters}).
		Los searchers s\'olo examinan la lista, por lo tanto pueden ejecutarse concurrentemente con sus pares.
		Los inserters agregan nuevos elementos al final de la lista, luego deben estar en exlusi\'on mutua para prevenir que dos de ellos inserten nuevos datos al mismo tiempo. Sin embargo, un inserter puede	proceder de forma paralela con cualquier cantidad de searchers.
		Finalmente, los deleters quitan datos de cualquier lugar de la lista, por lo tanto s\'olo puede haber un deleter a la vez el cual debe ser mutuamente exclusivo	con searchers e inserters.

		\begin{enumerate}
			\item{Obtenga una especificaci\'on formal de este requerimiento
			}
			\item{Obtenga programas que satisfagan el punto anterior
				utilizando la t\'ecnica del sem\'aforo binario dividido ($\SIG{SBS}$).
			}
			\item{Simplifique lo m\'as posible los multiprogramas resultantes.
			}
			\item{Analice la posibilidad de otorgar	prioridad a alguno de los tipos de procesos reduciendo el no-determinismo de las guardas de salida.}
			\item{Resolver este problema usando alguna clase de \textbf{monitores}.}  
		\end{enumerate}
	}
	
	
	\item{Durante la materia vimos que incorporar algunas instrucciones de granularidad ligeramente mayor a \Idiom{1-point}, simplificaba enormemente ciertos algoritmos de sincronizaci\'on, como por ejemplo los de inclusi\'on y exclusi\'on mutua.

		Sin embargo, estas instrucciones \Idiom{$\mbox{fetch-and-}\Phi$} agregan complejidad al pipeline del microprocesador por el ciclo \Idiom{read-modify-write}, y latencia a los protocolos de consistencia de cache y de interconexi\'on del microprocesador\cite[p.695]{caaqa}.

		En \cite{jen:87} se presenta una nueva t\'ecnica actualmente utilizada en microprocesadores $\SIG{RISC}$, denominada \textbf{sincronizaci\'on optimista}, completamente an\'aloga al control de concurrencia optimista en el \'area de transacciones en bases de datos \cite{ber:87}.
		Esta t\'ecnica consiste en tener el par de instrucciones \Idiom{load-linked}, \Idiom{store-conditional}, de las cuales podemos observar si fueron ejecutadas de manera at\'omica\cite{caaqa,jen:87}.

		A partir de este par de instrucciones podemos construir sentencias de mayor granularidad que \Idiom{1-point}, como por ejemplo el incremento at\'omico y el \Idiom{test-and-set}.
		\begin{center}
		\begin{small}
		\begin{tabular}{cc}
		\begin{minipage}{3in}
		\begin{Verbatim}[label=atomic\_inc,formatcom=\color{blue},frame=lines,rulecolor=\color{blue},xleftmargin=0.5in,xrightmargin=0.5in]
try:   LL(R0,n)
       INC(R0)
       SC(n,RO)
       BZ try
		\end{Verbatim}
		\end{minipage}
		&
		\begin{minipage}{3in}
		\begin{Verbatim}[label=test\_and\_set,formatcom=\color{blue},frame=lines,rulecolor=\color{blue},xleftmargin=0.5in,xrightmargin=0.5in]
try:   LL(R0,lock)
       OR(R1,R0,1)
       SC(lock,R1)
       BZ try
		\end{Verbatim}
		\end{minipage}
		\end{tabular}
		\end{small}
		\end{center}

		Para representar estas instrucciones en nuestro formalismo podemos realizar algunas simplificaciones a fin de no inundar con detalles irrelevantes.
		Por ejemplo en el siguiente multiprograma que \textbf{\emph{deber\'an demostrar correcto}}, al tener s\'olo una variable compartida, invalidamos el \Idiom{link register} s\'olo por cambios de contexto, y no por usar diferentes direcciones de memoria para el $\SIG{SC}$.
		  \newline
		  \begin{center}
		  \begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{$Pre: n=0 \wedge p_0\neq p_1$} \\
			\hline
			\begin{minipage}[t]{3in}
			\begin{tabbing}
				$P_0$: \= $s_0:=false;$ \\
					\>$\DO\ \neg$ \= $s_0 \rightarrow$ \\
					\> \> $\langle a_0:=n; lr:=p_0\rangle;$ \\
					\> \> $a_0:=a_0+1;$ \\
					\> \> $\langle$ \= $\IF\ lr=p_0\rightarrow s_0,n:=true,a_0$ \\
					\> \>		\> $\Box\ lr\neq p_0 \rightarrow s_0:=false$\\
					\> \> 		\> $\FI\rangle$ \\
					\>$\OD$ 
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{3in}
			\begin{tabbing}
				$P_1$: \= $s_1:=false;$ \\
					\>$\DO\ \neg$ \= $s_1 \rightarrow$ \\
					\> \> $\langle a_1:=n; lr:=p_1\rangle;$ \\
					\> \> $a_1:=a_1+1;$ \\
					\> \> $\langle$ \= $\IF\ lr=p_1\rightarrow s_1,n:=true,a_1$ \\
					\> \>		\> $\Box\ lr\neq p_1 \rightarrow s_1:=false$\\
					\> \> 		\> $\FI\rangle$ \\
					\>$\OD$ 
			\end{tabbing}
			\end{minipage}
			\\
			\hline
			\multicolumn{2}{|l|}{$Post: n=2$} \\
			\hline
		  \end{tabular}
		  \end{center}
		Notar que si demostramos este programa estamos estableciendo condiciones necesarias para la equivalencia entre los $P_i$ y $\langle n:=n+1\rangle$

		Como ejercicio complementario escriba \Idiom{test-and-set} en nuestro formalismo y realice alguna demostraci\'on que muestre que son intercambiables en el contexto de un multiprograma, como por ejemplo el problema de la secci\'on cr\'itica.
	}

\end{enumerate}


%------------------------------------------------------------------------
\begin{thebibliography}{99}

	\bibitem{and:concprog} Gregory R. Andrews,
	\emph{Concurrent Programming: principles and practice},
	Benjamin Cummings,
	1991
	
        \bibitem{and:2000} Gregory Andrews,
        \emph{Foundations of Multithreaded, Parallel, and Distributed Programming},
        Addison Wesley,
        2000

	\bibitem{ber:87} P. A. Bernstein and V. Hadzilacos and N. Goodman,
	\emph{Concurrency Control and Recovery in Database Systems},
	Addison-Wesley, Reading, Massachussetts,
	1987.

	\bibitem{ewd:703} Edsger W. Dijkstra,
	\emph{A Tutorial on the Split Binary Semaphore},
	EWD703,
	1979

	\bibitem{wf:method} W.H.J. Feijen and A.J.M. van Gasteren,
	\emph{On a Method of MultiProgramming},
	Monographs in Computer Science,
	Springer,
	1999

	\bibitem{jen:87} Jensen E. and Hagensen G. and Broughton J.
	\emph{A new approach to exclusive data access in shared memory multiprocessors},
	Technical Report UCRL-97663, Lawrence Livermore National Laboratory,
	Nov 1987.

	\bibitem{caaqa} John L. Hennessy and David Goldberg and David A. Patterson,
	\emph{Computer Architecture: A Quantitative Approach},
	Morgan Kaufmann, 2nd Edition,
	1996

	\bibitem{rh:86} Rob Hoogerwoord,
	\emph{Semaphores},
	RH86
	
	\bibitem{rh:221} Rob Hoogerwoord,
	\emph{Two Applications of the Split Binary Semaphore},
	RH221
	
        \bibitem{sch:onconc} F. Schneider,
        \emph{On Concurrent Programming},
        Graduate Texts in Computer Science,
        Springer,
        1997

\end{thebibliography}


\end{document}
