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.