\documentclass[11pt,a4paper]{article}
\usepackage[english]{babel}
\usepackage{mathpazo}
\linespread{1.05}
\usepackage{alltt}
\usepackage{fullpage}
\usepackage{algorithm2e}
\usepackage{amssymb}
\SetKwFor{Operation}{operation}{}{end}
\SetKwFor{Function}{function}{}{end}
\SetKwComment{Comment}{// }{}
\SetKwInput{Uses}{uses}
\SetKwInput{Initially}{initially}
\SetKw{KwNot}{not}
\SetKw{KwAnd}{and}
\SetKw{KwOr}{or}
\SetKw{KwDownto}{downto}
\newcommand{\putval}{\gets}
\newcommand{\true}{\textit{true}}
\newcommand{\false}{\textit{false}}
\newcommand{\ok}{\textit{ok}}
\newtheorem{theorem}{Theorem}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{fakelemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}{Proposition}
\newcommand{\toto}{xxx}
\newcommand{\idlow}[1]{\mathord{\mathcode`\-="702D\it #1\mathcode`\-="2200}}
\newcommand{\id}[1]{\ensuremath{\idlow{#1}}}
\newcommand{\litlow}[1]{\mathord{\mathcode`\-="702D\sf #1\mathcode`\-="2200}}
\newcommand{\lit}[1]{\ensuremath{\litlow{#1}}}
\newcommand{\andSo}{\ensuremath{\Rightarrow}}
\begin{document}
\title{Concurrent Algorithms: Exercise Set~3, Problems 2-3}
\maketitle
\sloppypar
\section*{Problem 2}
Consider the \emph{binary consensus} problem. Recall that this abstraction
satisfies
the following properties:
\begin{description}
\item[Agreement] No two processes decide different values.
\item[Validity] The value decided is one of the values proposed.
\end{description}
Let's assume that processes might in fact \emph{crash}, i.e. stop taking steps, at any point during the execution of
an algorithm. We add an extra condition on progress:
\paragraph{Termination} Every process that does not crash will eventually decide.
Assume the following theorem is true:
\begin{theorem}[FLP]
Binary consensus is impossible among $N$ processes, if one of them might fail by crashing, in an asynchronous system
that disposes of binary SRSW safe registers\footnote{In fact, this is one of the major results in distributed computing,
first stated by
Fisher, Lynch and Patterson, in their paper ``Impossibility of Distributed Consensus with One Faulty Process'' in
1985. For details, see the presentation in the Encyclopedia of Algorithms (available on Google Books), or the original
paper, which is quite readable.}.
\end{theorem}
Using what you know about registers, prove the following result:
\begin{theorem}[Students' FLP]
Binary consensus is impossible among $N$ processes, if one of them might fail by crashing, in an asynchronous system
that disposes of MRMW atomic registers.
\end{theorem}
\section*{Solution for Problem 2}
Assume for the sake of contradiction that there exists an algorithm $\mathcal{A}$ that solves consensus in an
asynchronous system using MRMW atomic registers. We prove that in this case there exists an algorithm $\mathcal{A}'$
that solves consensus in an asyncronous system using SRSW safe registers, which contradicts the \lit{FLP} theorem.
Let us write down the code of algorithm $\mathcal{A}$. The algorithm makes use of a (possibly infinite) number of MRMW
atomic registers $R_1, R_2, \ldots$. We know from the course that there exists an implementation of MRMW atomic
registers using (an infinite number of) SRSW safe registers. Therefore, for each call of $R_i.\lit{read}$ or
$R_i.\lit{write}$ that the algorithm $\mathcal{A}$ makes, we replace the call with the implementation of $R_i$ using
only SRSW safe registers. We call the resulting algorithm code $\mathcal{A}'$.
To conclude the proof, we notice that algorithm $\mathcal{A}'$ implements consensus using only SRSW registers. The
correctness of $\mathcal{A}'$ follows from the (assumed) correctness of $\mathcal{A}$ and the correctness of the
register implementation, which has been shown in class.
\section*{Solution for Problem 3}
Follows from $1$ and $2$.
\end{document}