Re: [tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)

Stephan,

Thank you for your thoughts on this.

I've updated my repo and the spec as you suggested. Spec copied below.

Limiting the state space and removing actions definitely reduced the number of states in the model, but I still wonder if I'm missing something. I suspect there must be a way to break a spec like this into two parts, one is the spec for the algorithm, and the other is a scaffolding spec to contain all the auxiliary stuff needed to fully test the algorithm, much like the tests and test harness for production software.

Here's the problem:

/\ clock = (p1 :> 0)
/\ clock_h = (p1 :> <<>>)
/\ sent = (p1 :> <<>>)
/\ read = (p1 :> <<>>)
/\ inbox = (p1 :> <<>>)

The sent, read, and clock_h variables explode the state space. I'm using them to reason about the clock. I suppose I should delete these extra variables and be more clever about how I reason about the algorithm...and in fact that's my next step. However, my general question is: Is there an idiomatic way to separate the stuff we use to verify that an algorithm works the way we want from the core of the algorithm itself? In this fantasy, I'm imagining that I put clock and inbox in SpecA, and put the auxiliary stuff into SpecB and then have a 3rd SpecC that combines the two as a unit or integration test?. Or perhaps I'm just thinking like a developer and thinking that application code and test code should be separate...

Thanks again,

-Todd

------------------------------ MODULE logical_clock ------------------------------
EXTENDS TLC
PT == INSTANCE PT
LOCAL INSTANCE FiniteSets
LOCAL INSTANCE Integers
LOCAL INSTANCE Sequences
LOCAL INSTANCE Naturals

\* ---------------------------------------------------------------------------
\* Constants
\* ---------------------------------------------------------------------------
CONSTANT Proc \* processors
CONSTANT MaxValue \* max value for any clock
\* (limit state space)
CONSTANT MaxSent \* max number of sent items per process
\* (limit state space)
CONSTANT Solution \* which solution to try (see readme.md)

ASSUME Solution \in { 1 , 2, 3 }
ASSUME Cardinality(Proc) > 0 \* we need at least one proc

\* ---------------------------------------------------------------------------
\* Variables
\* ---------------------------------------------------------------------------
VARIABLES
\* Variables intrinsic to the clock
clock, \* each clock has it's current value
inbox, \* each clock process has a msg inbox (queue)

\* Auxilary variables for use in reasoning about the clock
read, \* messages that the process has read from inbox
sent, \* each clock process has a history of sent changes
clock_h \* each clock has a history of value changes

vars == << inbox, read, sent, clock, clock_h >>

\* ---------------------------------------------------------------------------
\* Helpers
\* ---------------------------------------------------------------------------
MyReduceSeq(op(_,_), set, acc) ==
IF set = <<>>
THEN acc
ELSE PT!ReduceSeq(op, set, acc)

\* ---------------------------------------------------------------------------
\* Constraints
\*
\* These are artificial constraints to limit the state space of the specs.
\* This decreases the runtime of the spec, but may limit the modeler such
\* that it misses interesting paths.
\* ---------------------------------------------------------------------------

ClockConstraint ==
\A p \in Proc : clock[p] <= MaxValue

MaxSentConstraint ==
\A p \in Proc : Len(sent[p]) <= MaxSent

\* ---------------------------------------------------------------------------
\* Behaviours
\* ---------------------------------------------------------------------------

Init ==
/\ inbox = [p \in Proc |-> <<>>]
/\ sent = [p \in Proc |-> <<>>]
/\ read = [p \in Proc |-> <<>>]
/\ clock = [p \in Proc |-> 0]
/\ clock_h = [p \in Proc |-> <<>>]

EmptyOrNaturalSeq(s) ==
Len(SelectSeq(s, LAMBDA x: ~(x \in Nat))) = 0

TypeInvariant ==
/\ \A p \in Proc :
/\ clock[p] \in Nat
/\ EmptyOrNaturalSeq(inbox[p])
/\ EmptyOrNaturalSeq(sent[p])
/\ EmptyOrNaturalSeq(read[p])
/\ EmptyOrNaturalSeq(clock_h[p])

MaxInClockHist(p) == MyReduceSeq(PT!Max, clock_h[p], 0)
MaxInSent(p) == MyReduceSeq(PT!Max, sent[p], 0)
MaxInRead(p) == MyReduceSeq(PT!Max, read[p], 0)
MaxInInbox(p) == MyReduceSeq(PT!Max, inbox[p], 0)

Coherence ==
/\ \A p \in Proc :
\* A clock is always current
/\ clock[p] = MaxInClockHist(p)
\* A clock is never behind what it sent
/\ clock[p] >= MaxInSent(p)
\* A clock always increases in value
/\ IF clock_h[p] = <<>>
THEN
TRUE
ELSE
IF Len(clock_h[p]) = 1
THEN
TRUE
ELSE
\A i \in 1..(Len(clock_h[p])-1): clock_h[p][i] < clock_h[p][i + 1]

(*
Solution 1

This is the incorrect interpretation of the algorithm:

* increment the `s` process's clock
* send the incremented `s` clock to the target process's inbox

Later, the target process will read it's inbox and set it's clock to the
max of the inbox values and it's current value, and then add 1.
*)

WorkerIncrementSAndThenSendToT(self) ==
/\ Cardinality(Proc) > 1
/\ LET
other_clocks == {x \in Proc : x # self}
next_clock == clock[self] + 1
IN
/\ clock' = [clock EXCEPT ![self] = next_clock]
/\ clock_h'= [clock_h EXCEPT ![self] = Append(@, next_clock)]
/\ \E target \in other_clocks :
/\ inbox' = [inbox EXCEPT ![target] = Append(@, next_clock)]
/\ sent' = [sent EXCEPT ![self] = Append(@, next_clock)]
/\ UNCHANGED <<read>>

(*
Solution 2

IMO this is the correct interpretation of the algorithm:

* send `s` process's clock to target process
* `s` does not increment it's own clock as part of the send action

Later, the target process will read it's inbox the same as above.
*)
WorkerSendSToTAndThenIncrement(self) ==
/\ Cardinality(Proc) > 1
/\ LET
other_clocks == {x \in Proc : x # self}
IN
/\ \E target \in other_clocks :
/\ inbox' = [inbox EXCEPT ![target] = Append(@, clock[self])]
/\ sent' = [sent EXCEPT ![self] = Append(@, clock[self])]
/\ UNCHANGED <<read, clock, clock_h>>

WorkerReadInbox(self) ==
/\ inbox[self] # <<>>
/\ LET
inbox_max == PT!ReduceSeq(PT!Max, inbox[self], 0)
IN
/\ IF inbox_max > clock[self]
THEN
/\ clock' = [clock EXCEPT ![self] = inbox_max + 1]
/\ clock_h' = [clock_h EXCEPT ![self] = Append(@, inbox_max + 1)]
/\ UNCHANGED << sent>>
ELSE
/\ UNCHANGED << sent, clock, clock_h>>
/\ read' = [read EXCEPT ![self] = @ \o inbox[self]]
/\ inbox' = [inbox EXCEPT ![self] = <<>>]

\* Internal increment steps are required if number of processors
\* is 1, otherwise the spec deadlocks.
WorkerInternal(self) ==
LET
next_clock == clock[self] + 1
IN
/\ clock' = [clock EXCEPT ![self] = next_clock]
/\ clock_h' = [clock_h EXCEPT ![self] = Append(@, next_clock)]
/\ UNCHANGED <<inbox, read, sent>>

Worker(self) ==
CASE Solution = 1 ->
\/ WorkerIncrementSAndThenSendToT(self)
\/ WorkerReadInbox(self)
\/ WorkerInternal(self)
[] Solution = 2 ->
\/ WorkerSendSToTAndThenIncrement(self)
\/ WorkerReadInbox(self)
\/ WorkerInternal(self)
[] Solution = 3 ->
\/ WorkerSendSToTAndThenIncrement(self)
\/ WorkerReadInbox(self)

Next == \E self \in Proc: Worker(self)

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

=============================================================================
\* Modification History
\* Created by Todd D. Greenwood-Geer

On Tue, 21 Apr 2020 at 23:49, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

Hello,

I didn't find your TLA spec in your GitHub repository, but since it includes logical clocks that get incremented repeatedly, I am assuming that you use a state constraint for bounding the clock values? (You mention MaxValue but do not indicate how it is used.) For example, you could add

\A p \in Proc : clock[p] <= MaxClock

as a state constraint for a suitable value of MaxClock (Additional spec options -> State Constraint in the TLC Toolbox pane). Similarly, you are appending clock values to sequences (inbox and sent) [1] and you will probably have to bound the length of these sequences using constraints such as

\A p \in Proc : Len(inbox[p]) <= MaxChannel /\ Len(sent[p]) <= MaxChannel

Of course, with these constraints TLC will not explore the full (infinite) state space of the model but you gain confidence because the set of states that can be reached while respecting these constraints is explored exhaustively. Use engineering judgment for choosing the bounding constants, looking for a compromise between what TLC can handle and what part of the state space you believe should be explored in order gain confidence.

Stephan

[1] By the way, the text is ambiguous about whether you mean to append clock[self] or clock[self]+1.
On 22 Apr 2020, at 02:53, Todd Greenwood-Geer <t.greenwoodgeer@xxxxxxxxx> wrote:
How do I limit the state space of the model checker?

I am implementing a logical clock and attempting to verify that the clock operates as expected... that the
clocks always increment, and that this property holds:

\A s,t \in S : s->t => clock[s] < clock[t]

The logical clock is described by:
clock, \* each clock has it's current value
inbox, \* each clock process has a msg inbox (queue)
And reasoning about the clock is aided by these auxillary/ghost variables:
    read,                       \* messages that the process has read from inbox
    sent,                       \* each clock process has a history of sent changes
    clock_h                   \* each clock has a history of value changes

Running this model with 1 process is straight forward (3 states):

CONSTANT Proc = { p1 }
CONSTANT MaxValue = 2
But when I increase the number of processes to 2, the state space explodes (I stopped after
1,349,853 states):
CONSTANT Proc = { p1, p2 }
CONSTANT MaxValue = 2
I've written this up in much more detail here (see solution 2).

My implementation doesn't seem that different from the LamportMutex example here.

So my question is, what's the idiomatic way to write a spec such that the state space of the actual spec
remains small enough to be useful/tractable etc.? Am I miss-using auxillary/ghost variables? Should they
be put in a separate spec? Or am I misunderstanding something more fundamental ?

-Todd
p.s. Markus K. thank you for the pointer about not using Print|PrintT in my last email.
--
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/d54894f6-7282-4c29-be50-8cf19439953d%40googlegroups.com.
--
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/CBC7C298-D53A-46EB-AD60-5B779E27387E%40gmail.com.