[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Proving the absence of refinement and valuables refinements
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.
--
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/7d072f74-ef96-4265-835c-86603656c867n%40googlegroups.com.