You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
\textit{Something good happens eventually} (Cannot be violated by finite computation)
61
+
\end{definitionbox}
62
+
\begin{definitionbox}{Safety Properties}
63
+
\textit{Nothing bad happens} (Only violated by finite computations)
64
+
\end{definitionbox}
65
+
\end{tcbraster}
66
+
67
+
As liveness properties depend on computation, they can be constrained by a \textit{fairness property}.
68
+
\\\begin{tabular}{l p{.8\textwidth}}
69
+
\textbf{unconditional fairness} & Every process gets its turn infinitely often. \\
70
+
\textbf{strong fairness} & Every process gets its turn infinitely often if it is enabled infinitely often. \\
71
+
\textbf{weak fairness} & Every process gets its turn infinitely often if it is continuously enabled from a particular point in the execution. \\
72
+
\end{tabular}
73
+
74
+
\subsection{Key Aspects}
75
+
\begin{enumerate}
76
+
\item {\textbf{The problem}
77
+
Specified in terms of the \textit{safety} and \textit{liveness} properties of the algorithm.
78
+
}
79
+
\item {\textbf{Assumptions made}
80
+
\\\begin{tabular}{l l}
81
+
Bounds on process delays & (timing assumption) \\
82
+
Types of process failures tolerated & (failure assumption) \\
83
+
Use of reliable message passing & (communication assumption) \\
84
+
\end{tabular}
85
+
}
86
+
\item {\textbf{The algorithm}
87
+
Expresses the solution to \textit{the problem}, given \textit{the assumptions}.
88
+
\begin{itemize}
89
+
\item Must prove the algorithm is correct (satisfies all \textit{safety} and \textit{liveness} properties)
90
+
\item Time and space complexity of the algorithm
91
+
\end{itemize}
92
+
}
93
+
\end{enumerate}
94
+
95
+
\begin{examplebox}{Mutual Exclusion Properties}
96
+
What are the safety, liveness and fairness properties required for mutual exclusion of processes over some critical section?
97
+
\tcblower
98
+
\begin{center}
99
+
\begin{tabular}{l p{.5\textwidth} l}
100
+
\textbf{Safety} & At most one process accesses the critical section. & $(s \| t) \land (s \neq t) \Rightarrow\neg (cs(s) \land cs(t))$ \\
101
+
\textbf{Liveness} & Every request for the critical section is eventually granted. & $req(s) \Rightarrow (\exists t : s \preccurlyeq t \land cs(t))$ \\
102
+
\textbf{Fairness} & Requests are granted in the order. & $\begin{matrix*}[l]
103
+
req\_start(s) \land req\_start(t) \land (s \to t) \\
104
+
\Rightarrow (next\_cs(s) \to next\_cs(t)) \\
105
+
\end{matrix*}$ \\
106
+
\end{tabular}
107
+
\end{center}
108
+
Note that $\preccurlyeq$ is the \textit{happens-before} relation.
109
+
\end{examplebox}
110
+
111
+
\begin{definitionbox}{Concensus}
112
+
\[\text{Processes Propose Values} \to\text{Processes decide on value} \to\text{Agreement Reached}\]
113
+
\begin{center}
114
+
\begin{tabular}{l p{.7\textwidth}}
115
+
\textbf{Agreement Property} & Two correct processes cannot decide on different values. \\
116
+
\textbf{Validity Property} & If all processes propose the same value, then the decided value is the proposed value. \\
117
+
\textbf{Termination Property} & System reaches agreement in finite time. \\
118
+
\end{tabular}
119
+
\end{center}
120
+
Consensus is impossible to solve for a fully asynchronous system, some timing assumptions are required.
121
+
\end{definitionbox}
122
+
123
+
It is difficult to prove the correctness of even simple distributed systems formally. By specifying an abstract model of an algorithm automatic model checkers can be used to verify properties.
124
+
125
+
\subsection{Timing Assumptions}
126
+
\begin{definitionbox}{Asynchronous Systems}
127
+
A system where process execution steps and inter-process communication take arbitrary time.
128
+
\begin{itemize}
129
+
\item No assumptions that processes have physical clocks.
130
+
\item Sometimes useful to use \textit{logical clocks} (used to capture a consistent ordering of events on a virtual timespan)
131
+
\end{itemize}
132
+
\end{definitionbox}
133
+
134
+
\begin{definitionbox}{Synchronous Systems}
135
+
A system containing assumptions on the upper bound timings for executing steps in a process.
136
+
\begin{itemize}
137
+
\item This means there are upper bounds for steps such as receiving messages, sending messages, arithmetic, etc.
138
+
\item Easier to reason about.
139
+
\item Implementation must ensure bounds are always met, this can potentially require very high bounds (so guarantee holds) which reduce performance. \textit{Eventually synchronous models} were created to overcome this.
A link allowing for processes to communicate is disconnected and remains disconnected.
169
+
\\
170
+
\\ A network connecting machines hosting processes may become partitioned due to a \textit{link failure}
171
+
\end{definitionbox}
172
+
\begin{definitionbox}{Byzantine Failure}
173
+
Also called \textbf{Fail-Arbitrary}, a process exhibits some arbitrary behaviour (can be malicious).
174
+
\end{definitionbox}
175
+
\end{tcbraster}
176
+
\begin{definitionbox}{Omission Failure}
177
+
\begin{center}
178
+
\begin{tabular}{l l}
179
+
\textbf{Send Omission} & Fails to send all messages required by the algorithm. \\
180
+
\textbf{Send Omission} & Fails to properly receive all messages required. \\
181
+
\end{tabular}
182
+
\end{center}
183
+
\end{definitionbox}
184
+
185
+
\subsection{Communication Assumptions}
186
+
\subsubsection{Asynchronous Message Passing}
187
+
Processes continue after sending messages, they do not wait for a message to be delivered. It is possible to build a synchronous message passing abstraction from asynchronous message passing.
188
+
189
+
\subsubsection{Reliable Message Communication}
190
+
Messages are assumed to be conveyed using a reliable medium.
191
+
\begin{itemize}
192
+
\item All sent messages are delivered.
193
+
\item No duplicate messages are created.
194
+
\item All delivered messages were sent.
195
+
\end{itemize}
196
+
\noindent
197
+
Network failure is still a concern (breaks assumption), so TCP is used for messages, and more reliable message passing abstractions built on top.
198
+
\\
199
+
\\ Message delays are bounded, as a timeout is used.
200
+
201
+
\subsection{Complexity}
202
+
Complexity can be characterised using:
203
+
\begin{itemize}
204
+
\item Number of messages exchanged.
205
+
\item Size of messages exchanged.
206
+
\item Time taken from the perspective of an external observer, or some clock on a synchronous system.
207
+
\item Memory, CPU time or energy used by processes.
0 commit comments