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

*From*: Todd Greenwood-Geer <t.greenwoodgeer@xxxxxxxxx>*Date*: Wed, 22 Apr 2020 10:33:33 -0700*References*: <d54894f6-7282-4c29-be50-8cf19439953d@googlegroups.com> <CBC7C298-D53A-46EB-AD60-5B779E27387E@gmail.com>

Stephan,

Thank you for your thoughts on this.

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

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

`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

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] <= MaxClockas 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]) <= MaxChannelOf 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 theclocks 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 changesRunning this model with 1 process is straight forward (3 states):CONSTANT Proc = { p1 }CONSTANT MaxValue = 2But 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 = 2I'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 specremains small enough to be useful/tractable etc.? Am I miss-using auxillary/ghost variables? Should theybe put in a separate spec? Or am I misunderstanding something more fundamental ?-Toddp.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.

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/CAP0yLOu%2Bh2sq9Tdudfq2_FydfbVrEnDimYG173rqWa20MmEVNg%40mail.gmail.com.

**References**:**[tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)***From:*Todd Greenwood-Geer

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

- Prev by Date:
**Re: [tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)** - Next by Date:
**[tlaplus] Re: (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)** - Previous by thread:
**Re: [tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)** - Next by thread:
**[tlaplus] Re: (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)** - Index(es):