Discussion for: Bowen Alpern and Fred B. Schneider, "Defining Liveness" (Information Processing Letters, 1985)

Paper overview

The paper remarks the formal definition of properties as classes of executions. Then, it provides a definition for safety properties, with examples like mutual exclusion, deadlock detection, first-come-first-serve, and partial correctness to support the idea. Later, it gives a formal definition for liveness properties and provides related examples, such as starvation freedom, termination, and guaranteed service. In addition, the reading also differentiates between liveness, uniform liveness, and absolute liveness. The class of absolute liveness properties is a subset of the class of uniform liveness properties, which in turn is a subset of the class of (all) liveness properties. Finally, the reading demonstrates how “every property P is the intersection of a safety property and a liveness property.”

Discussion questions

Q0 (warm-up question)

Rewrite the abstract of the paper to get rid of the passive voice! :)

Discussion summary for Q0

We propose a formal definition for liveness properties. We argue that this definition captures the intuition that liveness properties stipulate that “something good” eventually happens during execution. We provide a topological characterization of safety and liveness. We show that every property is the intersection of a safety property and a liveness property.

Q1

(Contributed by @nliittsc)

The definitions of safety and liveness properties in section 2 are given in first-order logic. Can you translate the logical statements into their English equivalents? For example, the definition of safety might begin:

"P is a safety property if and only if, for all infinite executions sigma, sigma not satisfying P implies that..."

What is the benefit of writing down these properties in pure first-order logic, rather than as a definition stated in English (like you would find in a math textbook)?

Discussion summary for Q1

Safety: An infinite execution does not follow safety if there exists an unsafe finite prefix of it that cannot be made safe by any infinite continuation.

The version collaboratively created in class: P is a safety property, if and only if, given some execution \sigma, if \sigma does not exhibit a property P, then there exists some state \sigma_{i} such that no matter which sequence of infinite states \beta is following \sigma_{i}, \sigma_{i}\beta does not exhibit P.

Liveness: For all finite partial executions, there is an infinite continuation of the execution that when appended, satisfies the Liveness property.

The version collaboratively created in class: P is a liveness property, if and only if, for all partial executions \alpha, there exists an execution \beta where \alpha\beta satisfies P.

Benefits of using first-order logic:

• Easier to follow and prove what is being stated.
• No information is lost and there is less scope for ambiguity; everything is more concrete. On the other hand, in English, you get interpretations, which can include morals, etc.; like the words “good” and “bad” that we use when defining liveness and safety.
• Can be encoded and used as input to software, e.g., SMT solvers that can check the correctness of both logic and syntax.

Q2

Let F be the set of executions that observe FIFO delivery. F is a safety property, as we've discussed before in class. Theorem 1 says that every property is also the intersection of a safety property and a liveness property. What safety and liveness properties is F the intersection of?

Hint 1: If you're stuck, look at the first part of the proof of theorem 1 (the part before "It remains to show that L is dense" -- you don't need to know any topology to answer this!). What is L? Remember that in set theory, negation is complement.

Hint 2: Keep in mind the last sentence of section 4.

Discussion summary for Q2

Liveness: The execution will continue, or in other words, any execution in S^{\omega} Safety: FIFO itself: messages are to be delivered in the order they are sent.

A note from class: properties are sets themselves; they aren’t in the intersection, they are the intersection.

Q3

A couple of weeks ago, we read Lamport's "Time, Clocks, and the Ordering of Events in a Distributed System", which specifies the following three properties that should hold for a program that solves the distributed mutual exclusion problem:

(I) A process which has been granted the resource must release it before it can be granted to another process. (II) Different requests for the resource must be granted in the order in which they are made. (III) If every process which is granted the resource eventually releases it, then every request is eventually granted.

For each of these properties, is it a safety property, a liveness property, or a combination of the two? Explain your group's reasoning.

Discussion summary for Q3

• Property I: Safety; There is an identifiable point where a violation could happen. Once it’s violated, it cannot be unviolated. It’s stopping a bad thing, i.e., something being allocated to two or more processes at once.
• Property II: Safety; It doesn’t say that they should be granted; it’s basically FIFO.
• Property III: Liveness; It says “eventually”!

Errata

Running list of typos / issues found in the paper:

N/A

Other

Any interesting points or questions from the group discussion that didn't fit above:

N/A