4 ms·

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. > an

• pron 10y ago
  > 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/cohen-tlareduction.pdf 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`)
  • mrefj 10y ago
    > 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. [1] http://www.ccs.neu.edu/home/pete/pub/charme-refinement-branching-time.pdf http://www.ccs.neu.edu/home/pete/pub/charme-refinement-branc... [2] https://arxiv.org/pdf/1502.02942v1.pdf https://arxiv.org/pdf/1502.02942v1.pdf
    • pron 10y ago
      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.