\documentclass[12pt]{amsart}
\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}
\usepackage{listings}
% uncomment next line to get pdf files with hyperlinks
%\usepackage[pdftex,bookmarks=true]{hyperref}
\input{defmath}
\def\cao{\c c\~ao}
\def\cc{\c c}
\def\coes{\c c\~oes}
\def\ii{\'{\i}}
\def\stdin{\emph{stdin}}
\def\stdout{\emph{stdout}}
\def\sqn{seqüência}
\def\ibf#1{\item\textbf{#1}}
\def\acl{\textbf{ACL2}}
\newtheorem{qst}{Questão}
\def\SC{\textbf{Senhor do Castelo}}
\title{Sistemas operacionais\\
Prova 0.1 \\ An Outcast of the Islands}

\author{Raul H.C. Lopes}
\date{13/03/2003}

\begin{document}

\maketitle
\section{Introdu\cao}
Esta parcial da prova $0$ avalia seu conhecimento de 
sincroniza\cao\ de processos.
A prova é individual. Você pode consultar as suas nostas de aula, seu
livro, outros professores, a mãe, o pai e o vizinho, mas não o namorado e
nem o \SC: a leitura e entendimento da prova faz parte do processo de
avalia\cao.

Todas as questões têm o mesmo peso.

\section{Notação}

Como convencionado em sala de aula, vale a seguinte nota\cao:
\begin{itemize}
\item Atribui\cao\ simultânea de $a$ para $x$ e $b$ para $y$.

\begin{lstlisting}{}
  x,y := a, b
\end{lstlisting}

\item Seqüência
\begin{lstlisting}{}
   P
 ; Q
\end{lstlisting}

\item Concorrente
\begin{lstlisting}[mathescape]{}
  P
 $\mid\mid$
  Q
\end{lstlisting}

\item atômico
\begin{lstlisting}{}
  $< P > $
\end{lstlisting}

\item atômico e bloqueante até que $B$ seja verdadeiro:
\begin{lstlisting}[mathescape]{}
  $< B \rightarrow S >$
\end{lstlisting}

\end{itemize}

\section{As questões}
Considere as defini\coes\ de L.Lamport para \emph{safety} e \emph{liveness}.

\begin{center}
  \textbf{Saftey}: bad things don't happen.

  \textbf{Liveness}: Good things do happen.

\end{center}

\begin{qst}
Identifique condi\coes\ de \emph{safety} e \emph{liveness} para o problema de
\emph{readers and writers}.  Você nao precisa prová-las, mas 
justifique-as informalmente.
\end{qst}

\begin{qst}
  Uma variante do seguinte algoritmo de exclusão mútua foi apresentada em
sala e identificada como incorreta. 
Identifique suas condiçoes de \emph{safety} e \emph{liveness} do algoritmo
a seguir,
estabelecendo:
\begin{itemize}
  \item Possíveis altera\coes\ que devam ser feitas para que essas condi\coes\
sejam satisfeitas.
 \item Condi\coes\ de corre\cao\ do algoritmo: invariantes, 
condi\coes\ de progresso, limites de variáveis, etc.
\end{itemize}

\vspace*{.3cm}
\lstset{indent=30pt}
\begin{lstlisting}[mathescape]{}
  $\mid\!\![\ \mid\mid i: i \in \{0,1\}:$
    y.i = true
  ; x.i,v := true,i
  ; $<$ not(y.i) $\vee$ v=$\,\bar{i}$ $\rightarrow$ skip $>$
  ; CS.i
  ; y.i,x.i := false, false  
  $]\!\!\mid$
\end{lstlisting}


\end{qst}


\begin{qst}
  Uma variante do seguinte algoritmo de exclusão mútua foi apresentada em
sala. 
Identifique as condiçoes de \emph{safety} e \emph{liveness} do algoritmo
a seguir,
estabelecendo:
\begin{itemize}
  \item Altera\coes\ mínimas que devam ser feitas para que essas condi\coes\
sejam satisfeitas.
 \item Condi\coes\ de corre\cao\ do algoritmo: invariantes, 
condi\coes\ de progresso, limites de variáveis, etc.
\end{itemize}

\vspace*{.3cm}
\lstset{indent=30pt}
\begin{lstlisting}[mathescape]{}
  $\mid\!\![\ \mid\mid i: i \in \{0,1\}:$
    n.i = 1
  ; n.i := n.$\bar{i}$ + 1
  ; while ($n.\bar{i} \neq 0 \wedge n.\bar{i} \leq n.i$)
  ; CS.i
  ; n.i := 0
  $]\!\!\mid$
\end{lstlisting}
\end{qst}
\bibliography{abbrev,analysis,formal,algorithms,program,string}

\bibliographystyle{amsplain}


\end{document}

