Proving the absence of refinement and valuables refinements

[Samyon Ristov]

Sometimes, finding a refinement isn't easy. It all started with me trying to create a detailed specification that implements (refines) an abstract specification. I had an abstract specification A, and an implementation specification, AImpls, for which I managed to find a refinement that shows (with the model checker) that AImpls => A. The variable substitution wasn't that simple, but it worked. The fact that the substitution wasn't simple made me suspicious, but more on that later.

Then, I wrote another specification, ADetailedImpls, that I wanted to refine the AImpls specification, so ADetailedImpls => AImpls => A. After some work, I understood that there's unlikely to be a refinement from ADetailedImpls to AImpls (or directly to A), because it allows some behaviors that are not in line with A. In fact, ADetailedImpls implements an abstract specification B. But "unlikely" is not enough. What I want is to prove, or show with TLC, that there can't be a refinement from A to B, or from B to A. Since refinements may not be trivial, I want to be certain that I'm not missing a possible refinement from B to A (or from A to B).

Q1: Is it possible to prove, or show with a model checker, that there can't be a refinement from specification A to specification B?

While trying to find a very simple example, I stumbled upon another problem: finding valuable refinements. I found that my concerns are partially addressed by Lamport's "Hiding, Refinement, and Auxiliary Variables" note (https://lamport.azurewebsites.net/tla/hiding-and-refinement.pdf), so I'll refer to this note a few times, but my concerns can be understood without it as well.

Here's a bit oversimplified example. It's a bit oversimplified because I don't have abstract vs. implementation specifications, but it'll serve my purpose. I have two specs, 2counter and 3counter:

(all TLA+ files are available here: https://gist.github.com/samyonr/f3aa6f3c874dd09d65bf85ff218da285)

------------------------------ MODULE 2counter ------------------------------

EXTENDS Naturals

VARIABLES x

Init == x = 0

Next == x' = (x + 1) % 2

Spec == Init /\ [][Next]_x

XIs2CounterAction == x' # x => \/ x = 0 /\ x' = 1
                                                        \/ x = 1 /\ x' = 0

XIs2Counter == [][XIs2CounterAction]_x

THEOREM Spec => XIs2Counter

=============================================================================

------------------------------ MODULE 3counter ------------------------------

EXTENDS Naturals

VARIABLES x

Init == x = 0

Next == x' = (x + 1) % 3

Spec == Init /\ [][Next]_x

XIs3CounterAction == x' # x => \/ x = 0 /\ x' = 1
                                                        \/ x = 1 /\ x' = 2
                                                        \/ x = 2 /\ x' = 0

XIs3Counter == [][XIs3CounterAction]_x

THEOREM Spec => XIs3Counter

=============================================================================

I can show that 3counter implements 2counter:
(*
\* Option 1: 3counter -> 2counter

2C == INSTANCE 2counter WITH x <- IF x = 2 THEN 1 ELSE x

THEOREM Spec => 2C!Spec
*)

(As a side note, all my "INSTANCE" statements are commented out, because eventually, I get an error similar to this one:

Unknown location
Circular dependency among .tla files; dependency cycle is:
2counter.tla --> 2and3counter.tla --> 2counter.tla

In the Toolbox, it's even more problematic because after seeing this error, commenting out the circular dependency isn't enough. I had to delete the dependent specification and re-include it to make it work. If needed, I can provide more details, but I guess that normally people don't get the above error.)

I'm not sure how valuable this refinement is. It doesn't tell me much, and the substitution takes me away from my original spec. If I don't get a solid insight from a refinement, that makes it questionable. Of course, the example is oversimplified, but still.

I can, also, show a refinement from 2counter to 3counter. For that, I'll use an auxiliary variable which is a stuttering variable mentioned in Lamport's note:

----------------------------- MODULE 2counter_s -----------------------------

EXTENDS 2counter

VARIABLES s

InitS == Init /\ s = 0

NextS0 == /\ s = 0
                   /\ Next
                   /\ s' = 1

Stutter == /\ s = 1
                   /\ s' = 0
                   /\ UNCHANGED x

NextS == NextS0 \/ Stutter    

SpecS == InitS /\ [][NextS]_<<x, s>>

-----------------------------------------------------------------------------

THEOREM Spec => SpecS

3C == INSTANCE 3counter WITH x <- IF x = 1 /\ s = 0 THEN 2 ELSE x

THEOREM SpecS => 3C!Spec

=============================================================================

OK, so I found a refinement from 2counter to 3counter and from 3counter to 2counter. But there's another way to do that, even simpler:

---------------------------- MODULE 2and3counter ----------------------------

EXTENDS Naturals

VARIABLES x, y

Init == /\ x = 0
            /\ y = 0

TwoCounterStep == /\ x' = (x + 1) % 2
                                    /\ UNCHANGED y

ThreeCounterStep == /\ y' = (y + 1) % 3
                                       /\ UNCHANGED x

Next == \/ TwoCounterStep
               \/ ThreeCounterStep

Spec == Init /\ [][Next]_<<x,y>>

XIs2CounterAction == x' # x => \/ x = 0 /\ x' = 1
                                                        \/ x = 1 /\ x' = 0

XIs2Counter == [][XIs2CounterAction]_x

THEOREM Spec => XIs2Counter

YIs3CounterAction == y' # y => \/ y = 0 /\ y' = 1
                                                       \/ y = 1 /\ y' = 2
                                                       \/ y = 2 /\ y' = 0

YIs3Counter == [][YIs3CounterAction]_y

THEOREM Spec => YIs3Counter

-----------------------------------------------------------------------------

(*
2C == INSTANCE 2counter WITH x <- x

THEOREM Spec => 2C!Spec

3C == INSTANCE 3counter WITH x <- y

THEOREM Spec => 3C!Spec
*)

=============================================================================

I can add this to 2counter:
(*
\* Option 2 (See option 1 in 2counter_s):
2And3C == INSTANCE 2and3counter WITH x <- x, y <- 0

THEOREM Spec => 2And3C!Spec
*)

and this to 3counter:
(*
\* Option 2: 3counter -> 2and3counter -> 2counter

2And3C == INSTANCE 2and3counter WITH y <- x, x <- 0

THEOREM Spec => 2And3C!Spec
*)

It means that for every couple of specifications, A and B, I can create specification AB which has all variables of specification A and specification B, by modifying their names so they'll be disjoint, and showing that SpecA => SpecAB => SpecB => SpecAB => SpecA.

I think that something similar is discussed in the "Completeness" section in Lamport's note, but here it's a practical way to show that there is a refinement from every specification to any other specification. However, it doesn't mean anything at all.

Saying for 2counter that there's some other variable y for which 3counter's invariants are true, doesn't say a thing. 2counter has an endless amount of other variables that hold for various invariants, but it doesn't teach me anything about the 2counter specification.

Therefore, here's another question:

Q2: How to know that a refinement is valuable?
and:
Q1a: Is it possible to prove, or show with a model checker, that there can't be a refinement from specification A to specification B that is valuable?

Writing an abstract specification helps thinking about the problem. Creating a detailed implementation is valuable as well. But doing a refinement can be tricky: it'll show that the invariants of the abstract refinement are true, but if I'm substituting the implementation variables to get the abstract variables, then I'm not sure whether I get any new information.

I think it's discussed in Lamport's note in section 5 "Refinement in General", where observable variables and internal variables are discussed. But honestly, I'm not sure what an observable variable is, same for internal. For example in the FIFO specification discussed in the note, the queue is considered to be internal, but, is it? Queues are part of my system, whether it's in the OS, network card, brokers, and more. Many of them are directly visible, and others directly affect my coding, even if they are hidden under heavy abstraction. So I'm not sure whether I can call the queue to be internal or not.

Refinements are discussed in many tutorials, but not enough is written about when they are valuable and when they are not. So, how to make sure that a refinement is valuable?


Thanks in advance,
Samyon.

[Abhishek Singh]

Hi Samyon,

You have not specified any fairness constraints. If two specs A (abstract) and C (concrete) have no fairness constraints, you can show that C "implements" A by using a trivial refinement mapping that maps all states of C to an initial state of A. This is not useful because we want A to make some progress. If you had composed 2And3counter fairly, then you would have found it harder (impossible?) to show that 2counter implements 2and3counter.

I think that your counter modules are not interacting with an "environment" at the moment. If you can think of some context/environment for them, then "implements" will make more sense: if C implements A then it can act as a substitute for A in the environment.

If you view the FIFO queue in the note abstractly, only in terms of its operations, then the variable op should be external, and the variable queue should be internal. Chapter 5 in Specifying Systems contains a good example demonstrating the concepts of internal/external and implements/refines.

Regards,

Abhishek.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7d072f74-ef96-4265-835c-86603656c867n%40googlegroups.com.

[Samyon Ristov]

Good point!

In my real spec, I had a version of A with fairness conditions, but avoided using it, focusing on safety and leaving the liveness for a later stage.

Indeed adding fairness should make the refinement more valuable. 

I'll also check Chapter 5 in Specifying Systems. Thanks.

In that case, back to Q1: can I show that there can't be a refinement from (some) spec A to spec B?

Regards,

Samyon.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/ZwI6E-F_vbg/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFrvoiOHikJWh2vfZdtgUsU_tZaxaZA2FLjSwoJfnmJ0AwBx%3DQ%40mail.gmail.com.

[Abhishek Singh]

Consider a spec Nothing that has one state. It does not refine 2counter (with fairness). Proof: Suppose, for the sake of contradiction, that a refinement map f exists. f must map the single state of Nothing to one state of 2counter. Thus, any behavior of Nothing is mapped to a behavior of 2counter where it remains in one state, which is not a valid behavior due to fairness constraints. We have a contradiction.

The strategy in the above proof may be generalized to show the nonexistence of refinement maps in some cases, I think.

-Abhishek

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAAgQ8-tAbmyR9DmaK8ttSwz3zDbjnfrv59gXGkQcjPA_RWz5VA%40mail.gmail.com.

[Samyon Ristov]

Thanks, I had similar ideas (but without liveness, which caused problems), but hoped there was a more general case or approach. It would've been great if it was possible to show that two specs are inherently different.