Safety Liveness Decomposition and Machine Closure

[Willy Schultz]

In Alpern and Schneider's paper Defining Liveness they show that any system property P can be expressed as the conjunction of a safety and liveness property. I am wondering whether this decomposition always produces a safety property S and liveness property L such that (S, L) is machine closed. In a later Schneider paper, Decomposing Properties into Safety and Liveness using Predicate Logic, they explicitly define the safety property for the safety-liveness decomposition as S = (P ∪ Mp), where Mp is defined as the set of all behaviors B such that for every behavior b ∈ B, all prefixes of b have an extension that satisfies P.

It would seem that, by construction, the safety property of this decomposition is machine closed with respect to L, since any prefix in the safety property has an extension that satisfies P = S ∧ L, according to the definition of machine closure from Chapter 8 of Specifying Systems. 

If this is the case, does it also mean that we can use this decomposition to transform a non machine closed spec into a machine closed one? For example, if we originally express our system as a conjunction S' ∧ L' such that (S', L') is not machine closed, can we then decompose the property S' ∧ L'  into an alternate safety property S and liveness property L according to Schneider's technique to get a machine closed spec (S, L). 

I believe this may be touched upon already in the related paper Safety and liveness from a methodological point of view [1] but it wasn't entirely clear to me.

[1] https://dl.acm.org/doi/10.1016/0020-0190%2890%2990181-V

[Leslie Lamport]

For safety and liveness properties S and L, machine closure means that any prefix of a behavior satisfying S can be extended to a behavior satisfying S /\ L.  There is no reason that should be true for arbitrary S and L.  For example take

   S == (x \in {1, 2}) /\ [][x' = x + x]_x

   L == <>(x = 17)

Any property can be written as S /\ L where (S, L) is machine closed.

One of the virtues of TLA is that there's a simple, practical way to write only machine-closed specs.  If you write

    S == Init /\ [][Next]_v

Then S, L is machine closed if L is the conjunction of at most countably many formulas of the form WF_v(A) or SF_v(A),  where A => Next is true for all reachable states of S.

As for the paper "Safety and liveness from a methodological point of view", I suggest you read this response to it:

   Preserving Liveness: Comments on "Safety and Liveness from a Methodological Point of View"

   http://lamport.azurewebsites.net/pubs/abadi-preserving.pdf

As explained in Section 4.3 of

   Prophecy Made Simple

   http://lamport.azurewebsites.net/pubs/simple.pdf

adding prophecy variables can and often does produce a spec that is not machine closed.  This is the case for the prophecy variables in the examples in Section 5.

Leslie

[Willy Schultz]

Ok, thank you. It's now clearer to me that machine closure is a characteristic of how we express a particular temporal property as the conjunction of a safety and liveness property, which means that some safety-liveness decompositions for a given property P may be machine closed and others may not be, even though they both permit the same set of behaviors.

I have read the "Preserving Liveness" paper you referenced and my takeaway is that it is sometimes desirable to write non machine closed specification if it makes the specification simpler. Therefore, we should not try to unconditionally avoid non machine closed specifications since they can sometimes be useful.

Having said this, I am still trying to understand the motivating cases where one might want to write a specification that is not machine closed. I understand the formal definition and its correspondence to the notion of fairness. I am also aware that machine closure has some significance in the context of refinement mappings, but I'm trying to look at motivating examples without considering the refinement issue for now. I have come up with one example that is relatively concrete to me and I believe illustrates the concept of machine closure, even if it's somewhat of a toy example.

Imagine we have a rectangular grid system, and an agent that starts at the bottom left of this rectangle (i.e. at point (0,0)). Let's say that the top right corner of the rectangle is the "goal" node. We can imagine the grid as being discrete, though I think it works just as well to imagine it as a continuous two dimensional space.

We impose an initial condition on the agent i.e. x=0, y=0, and we can impose a liveness constraint that says "eventually the agent reaches the goal". Any path through our grid system that leads from the start point to the goal point satisfies our specification. We can think of a path in this example as a "behavior" in TLA+ terminology. We can then add a modification to our system so that there is a region near the top of the grid that the agent is not allowed to enter. With our specified liveness property, the agent should still be able to take routes that avoid or go around the obstacle. But, if we impose an additional safety property that the agent "can only move up or to the right", then it's possible for the agent to get "stuck" in a corner, without the ability to get out and ever reach the goal (i.e. to satisfy liveness). This seems like a valid example of a machine closure violation, and I believe that it illustrates one intuitive aspect of them, which is that satisfaction of both the safety and liveness property in cases like this might require "foresight" (Stephan Merz previously referred to this as "prescience") on the part of the agent. That is, without knowledge of the entire layout upfront, by only making local moves the agent has no way of knowing that it may be traveling into a "dead end" region, that will prevent it from ever reaching its goal.

My goal is to understand more real world examples of non machine closed specs. I have seen references to the "Lazy Caching in TLA" paper which gives a non machine closed spec for sequential consistency. I may need to study it in more depth, since that seems to be one of the main examples I've seen referenced. It appears that the memory spec in Chapter 11.2 of Specifying Systems is also similar to that one. One "weird" aspect of sequential consistency (and other, similar specifications like transaction serializability), is that they may permit behaviors that can "predict the future" i.e. a read can potentially return the result of a write that has not yet occurred yet. My understanding of these specifications is not thorough enough, however, to understand whether or not this "predict the future" aspect is the precise reason why such a specification would be non machine closed.

Note that Ron's blog post section on machine closure was helpful for me in understanding the concept more thoroughly.

[Leslie Lamport]

There are two kinds of specifications: ones that specify what a system does and those that specify how it does it.  Ideally one writes both and verifies that the how spec implements the what spec.  But currently, I believe that most industrial specs are how specs, and users verify that they satisfy invariants and simple liveness properties.

How specs should be machine closed; if they're not, then they don't really specify how.  In principle, it doesn't matter whether what specs are machine closed.  You should write the spec in a way that makes it easiest to understand.  In practice, machine closed specs are usually easier to understand.  But there are exceptions.  I don't think there's any way to characterize those exceptions.  This is not something to worry about.  You should just make sure that you don't write a non-machine closed spec without realizing that's what you're doing; if you do, then your spec is probably wrong.

Leslie

[Willy Schultz]

When writing real world industrial specs I have indeed never had to worry about the concept of machine closure explicitly. My questions stemmed from a theoretical interest, not a practical one. I was simply curious to know if there were particular, nontrivial examples of non machine closed specifications that were well motivated. Perhaps the "Lazy Caching" spec is the best one to study in this category.