0:07
Uh, in this lecture we'll see two very important properties
that are, uh, desired in distributed systems;
these properties are called safety and liveness,
and along the way we'll also discuss
the kinds of, um, properties
that, uh, the global snapshot algorithm can be used
to detect in a distributed system.
So correctness in distributed systems is, uh, highly desired,
and there are two properties that can be used to,
uh, specify correctness requirements.
These properties are known as liveness and safety.
Uh, the definitions are distinct,
uh, but they are often confused with each other,
so its' very important for us to be able to distinguish
one from the other.
0:42
Let's look at liveness first.
Uh, in a nutshell, liveness is a guarantee that something good
will happen eventually, okay?
Uh, eventually does not imply a time bound,
but if you let the-the system run long enough,
then it-it guarantees, uh, liveness.
Uh, so examples of this, uh, are, in the real world,
uh, the guarantee that in an Olympics 100 meter dash,
at least one of the athletes will win the gold medal.
This is a liveness guarantee, something good,
which is winning the medal, happens eventually.
Uh, a criminal will eventually be jailed
is a liveness guarantee
that legal systems in many countries, uh, try to guarantee.
It's hard to guarantee it, but it-it is a desired property.
In a distributed system, uh, the termination property
is a liveness property.
You want a distributed computation-computation
to terminate,
and, uh, this is the, uh, guarantee that something good,
which is termination, will happen eventually.
Completeness and failure detectors,
uh, is a liveness property.
This is a property that says that eventually,
every failure will be detected
by the other non-faulty processes in the system.
1:45
In consensus, uh, liveness says
that all processes eventually decide on a value.
Safety, on the other hand, is a guarantee that something bad
will never happen in the system, okay?
So notice that there we are using "bad" instead of "good"
earlier in the liveness,
and we are saying will never happen,
uh, because we desire that it never happens in the system.
Again, in the real world, a peace treaty between two nations
is an example of a safety property,
uh, which guarantees that war
will never happen between those two nations.
Again, this is a desired property;
this is not always what happens.
Uh, wars have happened in spite of treaties,
um, so treaties are clearly not safe all the time,
but it's an example of a desired safety property.
Uh, legal systems try to guarantee the safety property
that an innocent person will never be jailed;
that would be really bad.
In a distributed system,
uh, the fact that we do not want deadlocks
in a distributed transaction system
is an example of a safety property which we desire.
The fact that we do not want objects to be orphaned,
meaning they don't have any pointers pointing to them,
is an example of a safety property.
Accuracy and failure detectors is a safety property
because it says that we do not want any mistaken detections
of non-faulty processes being marked as failed.
And in consensus, we do not want two different processes
to decide on two different values,
uh, because that would be bad and that would be unsafe.
3:01
Uh, guaranteeing both liveness and safety is very hard.
In failure detectors guaranteeing,
um, uh, liveness and safety,
which is completeness and accuracy,
is, uh, impossible in an asynchronous distributed system,
especially if you want these to be time-bounded.
Uh, in c-in the consensus problem, uh, making decisions,
uh, within a time bound and, uh, correct decisions,
um, uh, making sure that
the correct decisions are correct
cannot both be guaranteed
in an asynchronous distributed system.
You can guarantee eventual liveness,
which is what algorithms like Paxos, uh, guarantee,
but time-bounded liveness cannot be guaranteed.
And of course, as many of us know,
it's very hard for legal systems to guarantee both,
uh, liveness and safety,
and in fact to guarantee either liveness or safety
is very hard.
Um, it's-it does happen
that some criminals never serve any jail time,
and it also does happen that innocents are jailed.
3:50
So in the language of global states;
remember that a distributed system moves
from one global state to another via causal steps,
um, which you saw in an earlier lecture
in the snapshot series,
uh, liveness with respect to a property Pr
in a given state S essentially means that,
uh, the state S satisfies Pr,
and if this is, uh, not true, then there is
some causal path that goes from the state S to another state S',
global state S', where S' would satisfy Pr.
Okay, so all you require here is that there is some way to get
from the current state to another state,
um, that, uh, satisfies liveness.
If this is true for every state that you are in,
that whate-whatever state you are in,
you can reach another state that
um, uh, that satisfies liveness
uh, the liveness property Pr,
then this system is said to be satisfying
the liveness property.
5:02
So how do we use a global snapshot algorithm
to detect global properties?
Well, the snapshot algorithm
can be used to detect global properties that are stable.
When I say stable, I mean properties that,
once they are true,
they st-they stay true forever afterwards.
Uh, these could be either stable liveness properties
or stable non-safety properties.
A stable liveness property might be of the kind
the computation has terminated.
Once a computation has terminated,
it stays terminated forever,
and this is obviously an example of a good property
that we want to be true,
so it's a liveness property that is stable,
and it can be u-and it can be detected
using the global snapshot algorithm.
Stable non-safety properties include, um, uh,
the fact that there is a deadlock.
Once a deadlock happens in the system,
it will stay forever until you do something about it.
Also, uh, once an object is orphaned, uh, that is,
it has no pointers pointing to it,
it will stay that way until you do something about it.
Both these are examples of non-safety properties
that are stable,
and so the global snapshot, uh, algorithm which we discussed,
the Chandy-Lamport algorithm,
can be used to detect, uh, these stable properties.
Uh, why can you use to dete-
these to detect the sto-stable properties?
Because Chandy-Lamport algorithm
is guaranteed to be causally correct.
Even though the Chandy-Lamport algorithm does not, uh,
guarantee that the snapshot calculated by it
holds at any physical point of time in the past,
it does guarantee causal correctness,
uh, which means that it does not violate
our, uh, human being's understanding of
what happens causally in the distributed system,
and so it can be used to detect, uh, stable properties.
Wrapping up our discussion of snapshots,
the ability to calculate a global snapshot
is really important in a distributed system,
uh, but you want to calculate the snapshot,
uh, concurrently and parallelly
while allowing the application to continue proceeding
and sending its application messages,
and the Chandy-Lamport algorithm allows us to do exactly that.
The output of a Chandy-Lamport algorithm is
a, uh, global snapshot that obeys causality.
In other words, it satisfies a consistent cut,
it's equivalent to a consistent cut,
and it can be used to detect stable global properties
which are either, uh, liveness properties
or non-safety properties.
We've also discussed two very important definitions,
liveness and safety,
which, um, are relevant of course
to the snapshot- snapshots discussion.
These are properties that appear, uh, elsewhere
and in other parts of this course,
uh, because these are very important,
uh, classes of properties
that we desire in distributed systems.
Indranil GuptaProfessor
