That is true. Scaling this to processor with caches and deep pipelines is completely non-trivial. There has been some attempt to scale to more "realistic" designs with compositional (stepwise) verification.
ACL2 is an alternative that strives to strike a balance between interaction and automation.
- It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, etc.
- Its authors received the ACM software system award in 2005.
-It is used in commercial products since several years in companies including AMD, Centaur , Rockwell Collins, etc. There is a not-so comprehensive but yet impressive list of applications here:
- Also, since the language is a subset of Common-lisp, any one who knows a bit of programming can very quickly start using ACL2. One does not need to learn type theory/logical formalism to start using it. It has an eclipse plugin that is used by first and second year undergraduate students (http://acl2s.ccs.neu.edu/acl2s/doc/).
> But reasoning with functions is a specific level of abstraction.
Excellent point. The level of abstraction is a fundamental concern, not just in modeling but also in reasoning about systems. And state machines (as used in TLA or otherwise) add temporal abstractions to the mix of abstraction mechanism. To add to its power, it does not lead to any loss of generality; since any program in a language with well-defined operational semantics can be modeled using state machine (transition systems with infinite state space to be little more precise).
> In TLA, bisimulation and trace equivalence are the same, and
simulation is just trace-inclusion.
There is a fundamental difference between (bi)simulation and trace inclusion(equivalence); the former is a branching time notion and the later is a linear time notion. In fact if one it is easy to show if A is a simulation of B then A is also a "trace inclusion" of B. And this difference has some practical ramifications as well.
The branching time notions of refinement also has (not so famous) the completeness result.
This has some practical ramification as well: the refinement map in Abadi/Lamport is a projection function, while in branching time it can be arbitrary function. The former is intuitively clear but often difficult in practice. The flexibility has been exploited to efficiently analyze correctness of several non-trivial systems like pipelined processors.
> So there is no such thing as two machines, one implementing the other, that cannot be expressed in this way.
To drive home the point what the completeness result means is
that one can always reason at the level of abstraction that was use to specify the system: state and their successors. This is what we are after in type-based reasoning: reasoning at the level of functional abstraction.
> the former is a branching time notion and the later is a linear time notion
I think it is more precise to say that you cannot formally encode the concept of (bi)sumlation in LTL while you can in CTL. The notion itself, however, is a general structural relation between state machines that is independent of the temporal logic you use to formalize properties of their behavior, if any. I.e. (bi)simulation would exist even if temporal logic didn't.
> the refinement map in Abadi/Lamport is a projection function
One of the few things I don't like in TLA+ is that you can create a "refinement" mapping which isn't sound (and therefore isn't a refinement). In particular, you can add auxiliary variables that interfere with the specification. I know Lamport is working on a paper where he gives syntactic rules that ensure that the mapping is sound.
> This is what we are after in type-based reasoning: reasoning at the level of functional abstraction.
The challenge is making that reasoning rich enough (to reason about a wide class of programs), scalable enough, and at the same time affordable and simple for engineers. This goal is far from realized (and currently falls short, at least in the last two requirements).
P.S
I also think that TLA allows reasoning about structural properties of the state machine without any use of temporal logic at all. If A and B are action formulas and S is a state-predicate, then `S ∧ A` denotes the set of transitions from the set of states denoted by S (conversely `S' ∧ A` is the set of transitions into S). And so `S ∧ A ⇒ S ∧ B` means "for every transition A leaving S, there is a transition B leaving S". I think that you can therefore show (bi)simulation directly, structurally, rather than behaviorally; there is no use of behaviors (traces) or computation trees here at all (you may want to show that all the states S are reachable from the initial states).
[1]: Unless behaviors are sequences of states, in which case the relationship coincides with the trace-equivalence relationship. There may be subtle technical differences (that I don't quite understand) even then, but they don't matter.
> create a "refinement" mapping which isn't sound (and therefore isn't a refinement).
Could you please illustrate what do you mean by unsound refinement ? Refinement mapping along with the notion of correctness forms the part of "trust computing base". More precisely, the statement "A implements B under a refinement map r" assumes two things (1) what it means to implements; is it trace inclusion or simulation or stuttering simulation .... (2) what is the refinement map r. What am i missing here ?.
Also can you please illustrate (with an example possibly) on the syntactic rules that Lamport is working on ?
Addition of auxiliary variables to the specification introduces an extra proof obligation, namely, that it does not change its observable behavior. Often this is not very difficult as one can syntactically differentiate between auxiliary variables and the state variables.
>I also think that TLA allows reasoning about structural properties of the state machine without any use of temporal logic at all.
Definitely. Like you mention the refinement based on (bi)simulation or trace inclusion is different from the use of temporal logic to formalize properties of systems. Though two are related in the sense of adequacy of temporal logic: simulation preserves ACTL* properties while trace inclusion preserves LTL properties.
> I think that you can therefore show (bi)simulation directly, structurally, rather than behaviorally; there is no use of behaviors (traces) or computation trees here at all.
I do not quite understand what you mean here. Behaviors are succinctly represented using state machines -- set of states and there successors-- and then we look at a state machine as a generator of (possibly infinite) behaviors -- either as traces or computation trees.
The scenarios where trace inclusion requires addition of prophecy and history variables to recover local reasoning (in other words structural reasoning using state and its successors) is more related to the completeness argument you mentioned earlier.
> (1) what it means to implements; is it trace inclusion or simulation or stuttering simulation .... (2) what is the refinement map
Well, in TLA there's only one kind of implementation relation, as the three relations you mention coincide since a trace is a sequence of states, under a stuttering equivalence. All other implementation relations (like event-trace-inclusion) are the same relation on a reduced (abstracted) machine, with some of the state erased, or a refined machine with an added time variable. So the map (which we take to include auxiliary variables) fully describes the "kind" of implementation.
> Could you please illustrate what do you mean by unsound refinement?
The TLA+ features are, of course, completely sound, but you may not be mapping what you intended to map. The trickiest problem has to do with prophecy variables. You need to ensure that they don't restrict the behavior of the spec, and it's not always obvious.
> Also can you please illustrate (with an example possibly) on the syntactic rules that Lamport is working on ?
The simplest rule is that if the spec is
Init ∧ ◻[Next]_x
and, under an invariant:
Inv ∧ Inv' ⇒ (Next ≣ ∃i∈Π : N(i))
Then the spec remains equivalent when introducing the prophecy variable p like so:
∃∃p : (Init ∧ p ∈ Π) ∧ ◻[N(p) ∧ p' ∈ Π]_<x, p>
This basically means that the prophecy must cover the entire parameter space of N, and that once used, a prophecy must be "forgotten". The problem is parameterizing N. So the rules treat various forms of Next (disjunction, quantification etc.).
But if Next is parameterized well so that its behavior isn't restricted by p, then obtaining a useful value from p for the mapping can be tricky: so you know what value will be picked by an existential quantifier, and you know what disjunct will be chosen etc., but you still need an interpreter for those choices to obtain the result of the machine's action. You could write the spec itself in a clever parameterized way so that it would be its own prophecy interpreter, but then you'd make it completely unreadable.
In short, the problem is that you need to make sure that your prophecy variables are sound, but you still want to keep the spec at that refinement level readable and not sacrifice it for the sake of refinement to some other level, and the two requirements pull in opposite directions.
What you could do (and that's what I did in a complex spec), is to use a prophecy variable that interacts well with the spec (i.e., doesn't make it unreadable) but doesn't conform with Lamport and Merz's rules, and then prove that it is sound. Unfortunately, that property alone can be 95% of what you intend the refinement to show in the first place, and here the model checker can't help you at all.
We really need a model checker that can handle temporal quantification.
> I do not quite understand what you mean here.
Oh, it was just to emphasize the point that simulation is a structural property, unrelated to temporal logic or any notion of time or behavior.
Thanks for the explanation especially with the example.
I now understand what you meant by "unsound refinement" and the desire to keep the spec readable.
> and that's what I did in a complex spec
Do you believe that your hands were tied because the mapping can only be a projection of state?
Is this spec and the corresponding implementation that you are working on in public domain ?
> We really need a model checker that can handle temporal quantification.
Do you intend to restrict the quantification only over time variable only ? Why do I ask this? This is because even in presence of finite stuttering, one only needs to analyze about state and the successors ?
If you intend to quantify over state variables (including the prophecy/history variable, for instance in the example you mentioned) -- that is a more general problem of dealing with quantifiers and there is still long way to automate that aspect.
> Is this spec and the corresponding implementation that you are working on in public domain ?
Not currently. Maybe in the future.
> Do you believe that your hands were tied because the mapping can only be a projection of state?
Rather than? I'm not sure I understand the question, so maybe. My problem is that some reductions require moving certain transitions backwards or forwards in time. In theory, the idea is described well in section 3 of this paper https://research.microsoft.com/en-us/um/people/lamport/pubs/... (this is pretty much exactly my problem: I wanted to see if a distributed transaction is a refinement of an atomic transaction). In practice, using prophecy variables isn't easy.
> Do you intend to restrict the quantification only over time variable only?
Oh, no, in TLA "temporal quantification" means hidden state, or quantifiers over state variables. Having the model checker handle that would make auxiliary variables unnecessary in cases where the more abstract specification has hidden internal state (unless you want a deductive proof). It will save us the hardest work, and ensure that the implementation relation is sound (no auxiliary variables necessary).
It would have solved my problem, too. Even though auxiliary variables would still be necessary, the model-checker could check that they're sound by checking:
S ⇒ (∃∃ aux : S_with_aux)
to see that adding the auxiliary variables doesn't restrict the spec (and then I could check, as I do today, that `S_with_aux ⇒ Abstract_S`)
> My problem is that some reductions require moving certain transitions backwards or forwards in time.
This is definitely a more involved problem. A cleaner solution, I believe, requires a new notion of correctness than trace containment/simulation up to stuttering. This is because neither of these notions allow one to move forward or backward observable transitions. The key here is to differentiate between non-observable and observable non-determinism. While the former can be accounted by using prophecy variable in linear time framework or directly in the branching time framework. I will recommend reading the comparison of the two approaches in [1]. However, the later is not what can be accounted by adding auxiliary variables. It is done currently by complicating a simple sequential specification -- create a new specification that includes all possible interleaving of transitions implicitly or explicitly. I will be curious to hear your insights on this while using TLA+ in particular and Lamport's theory of refinement in general.
I must say that the above must be at best considered speculative from a practical methodology point of view. I do suggest a concrete alternative nor do I have extensive experience in validating actual distributed systems.
> Rather than? I'm not sure I understand the question, so maybe
This is the easier part and a less speculative comment :).
In the theory of refinement in branching-time framework developed in [1,2] the refinement can be any computable function rather than just a projection of states space. This often is very helpful. For example a refinement map for a pipelined processor is defined by invalidating all partially executed instructions and setting the program counter to the oldest instruction in flight. This is relatively more involved than just a projection map that "hides" the internal states. Notice that, as we have already mentioned earlier, branching time refinement implies trace containment, a linear-time notion. So there is nothing lost. There are follow up papers with case studies illustrating the use of this flexibility to define refinement map that makes automated reasoning more amenable.
Thanks for clarifying the temporal quantification.
I read the paper in the first link, and I may read it again, but I have a few remarks:
1. Refinement mappings in TLA also allow arbitrary state functions.
2. There are very good reasons to want machine closure, and one of the things mentioned at the end of that paper as an advantage (that there is no necessity in a separate liveness property), is actually a serious disadvantage.
Let me give you an example, using what Lamport calls "raw" TLA, which is TLA which is not stuttering invariant:
Spec1 ≜ t = 1 ∧ x = 1 ∧ ◻(t' = t + 1 ∧ x' = x + 10)
Spec2 ≜ t = 1 ∧ x ∈ Nat ∧ ◻(t' = t + 1 ∧ x' = x + 10 ∧ t = 10 ⇒ x = 100)
The two specifications specify the same behavior. But, in this world, a safety property can imply a liveness property, e.g. x ∈ Nat ∧ ◻(x' = x + 10) ⇒ ◇(x ≥ 100)
Now, this is bad because the second specification is actually not implementable in a computer with complexity similar to that of the behavior as it relies on "angelic" nondeterminism. It is possible to use angelic nondeterminism in TLA (it's important for high-level specs) like so:
Spec3 ≜ t = 1 ∧ x ∈ Nat ∧ ◻[t' = t + 1 ∧ x' = x + 10 ∧ t = 10 ⇒ x = 100]_<t, x> ∧ ◇(t ≥ 10)
(the square brackets mean that either the action is true, or <t, x> are unchanged) But now, the liveness property is not implied by the safety property, and it requires an explicit statement in the formula. That last formula, Spec3, is not machine-closed, and this makes it easier to see that the algorithm implied is unrealizable as written.
> 1. Refinement mappings in TLA also allow arbitrary state functions.
Could you please point me to a reference for this. The completeness result from "The existence of refinement mapping" only includes projection. I know that TLA does allow existential quantification over internal variables (corresponds to hiding) and one can eliminate the quantifier by defining a function. But notice that is just the logical way of specifying "hiding" and is different from having arbitrary refinement mapping.
>2. There are very good reasons to want machine closure ...
Definitely. However, these are the concerns when we are specifying a system -- is the specification correctly models the system that I have in mind. While the comments in the paper -- no necessity to separately analyze liveness -- refers to the easy while proving that a concrete specification "implements" an abstract specification. And this is what your example specifications illustrates (thanks for specific examples, it helped me to understand the point you are making).
> I know that TLA does allow existential quantification over internal variables (corresponds to hiding) and one can eliminate the quantifier by defining a function.
That's what I meant. The functions do not necessarily apply to hidden variables only, but to any variable. E.g., in TLA+, if Spec1 has variable x and Spec2 has variables q and t, you could write:
Spec2 ⇒ INSTANCE Spec1 WITH x ← q + t
Which implements Spec to by mapping (q + t) to x.
> But notice that ... is different from having arbitrary refinement mapping.
Can you explain what you mean?
> However, these are the concerns when we are specifying a system -- is the specification correctly models the system that I have in mind.
Right, but you want an easy way to determine if a specification is machine-closed or not. TLA provides a sufficient syntactic condition. A specification is guaranteed to be machine closed if it can be written as
Init ∧ ◻[M]_vars ∧ Fairness
Where M is an action and `Fairness` is a conjunction of ⬦ clauses containing WF/SF (weak/strong fairness) conditions only. In fact, when testing safety properties alone (which is normally the case), a specification is usually just
Init ∧ ◻[M]_vars
Which TLA guarantees is machine-closed. Otherwise, a ◻ formula alone may not be machine-closed (and may imply a liveness property, like in my example above), and proving whether it is or it isn't may be non-trivial.
http://www.ccs.neu.edu/home/pete/research/ieee-vlsi-composit...
http://www.ccs.neu.edu/home/pete/research/todaes-safety-live...