[tlaplus] Re: Safety Liveness Decomposition and Machine Closure

[Willy Schultz <will62794@xxxxxxxxx>]

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.

On Sunday, August 9, 2020 at 1:15:28 PM UTC-4 Leslie Lamport wrote:

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1e305cdb-795c-467f-bf8b-c5279b3b3018n%40googlegroups.com.