5 ms·

> 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 ? Ref

by mrefj 10y ago

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

pron 10y ago
> (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.
- mrefj 10y ago
  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.
  - 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`)

by mrefj 10y ago

pron 10y ago

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

mrefj 10y ago
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.
- 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`)