[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: TLA+-style Refinement vs. Backward and Forward Simulation

In the compiler paper the authors assume that Impl is "deterministic, that is, ... it admits only one observable behavior... This is the case if the target language ... has no internal non-determinism (programs change their behaviors only in response to different inputs but not because of internal choices) and the execution environment is deterministic (inputs given to programs are uniquely determined by their previous outputs)".

In this special case, Impl has only one observable behavior; then if Spec => Impl and Spec has at least one observable behavior then we must also have Impl => Spec.

They are interested in showing Impl => Spec but they go the other way because it works in this special case and because Spec => Impl is easier to prove than Impl => Spec. They are interested in this special case because their target language is a single-threaded assembly language that is shown to have no internal non-determinism; however, I do not know if the determinism of the environment is a reasonable assumption. I have only skimmed the paper.


On Saturday, March 5, 2022 at 4:57:04 PM UTC-6 Leslie Lamport wrote:
Spec describes those behaviors that are considered correct.  Impl describes those behaviors that the system can produce.  The engineers I talk to want to know that every behavior the system can produce is correct, for which they have to check if Impl => Spec is true.  I presume that for compiler verification, Spec describes the code written in the compiler's input language and Impl describes the compiled code.  I have no idea why they want to verify Spec => Impl.  Can you explain why they want to do that?


On Friday, March 4, 2022 at 8:08:43 PM UTC-8 alex.m.w...@xxxxxxxxx wrote:
Hi everyone. Refinement is a big part of TLA+. Pretty much all examples that I've seen of TLA+ refinement are of the following form:

Impl => Spec

where Impl is the specification of an implementation, and Spec is a higher-level specification. The intuition of this is that Impl must have a subset of Spec's behaviors in order to be true, i.e. Spec can "do more" and Impl can "do less."

My first question is, why don't I see the opposite statement being checked? That is:

Spec => Impl

Is this not also an acceptable correctness statement, even though it has different properties?

That's where my question about the relation to simulation comes in. Is it accurate to say that the first refinement shown here is equivalent to a backward simulation and the second is a forward simulation? If not, what are the differences?

For background, the reason I've become curious to understand this better is that I've been reading and re-reading A formally verified compiler back-end, the paper about proving compiler correctness in CompCert. While the verification of CompCert doesn't use TLA+, and that might lead to a difference in terminology, in the paper they equate backward simulation to refinement. To verify the compiler, however, they chose to prove forward simulation, which has me wondering why we don't prove more TLA+ specifications via Spec => Impl.

Most of all I'm just looking for a clarification of terminology and some deeper intuition about refinement and simulation. Thanks for any responses.

- Alex Weisberger

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/46ade60f-33ac-4341-b519-29cd3bf5dffen%40googlegroups.com.