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

*From*: recepient recepient <netsmaza@xxxxxxxxx>*Date*: Tue, 24 Nov 2020 15:54:58 -0800 (PST)*References*: <e3a99dad-9df9-48a9-b0ad-c9ba95a25d7dn@googlegroups.com> <E8F7421E-B99E-430C-A393-120CB3F018B8@gmail.com>

Stephan, Thank you - know how on display.

How does TLA ever escape from 'while (TRUE)'? It does in fact. But any reasonable interpretation would argue TRUE is a constant true condition.

Second, you write: "

The cartesian product k \in HashKey, v \in HashValue, op \in ClientOps is 12 elements big so 2^12 elements in its power set. And for each element in the power set it would have to try all permutations contributing n! calls per each. Altogether that's over 1 billion calls into PerformOp. On the other hand TLA reports:

>278 states generated, 178 distinct states found, 0 states left on queue.

Adding a print in PerformOp (I know, I know!) only shows ~100 calls. I'm only seeing <200 nodes and <300 edges in the .dot graph albeit there are cycles all over the place. Even then I can only find ~100 unique paths from the initial node to final node without revisiting nodes.

But there's even more. If this is to be

Example, suppose we only cared about exploring all possible sequences of operation calls on just two tuples. I'd expect TLA to do the following.

Case 1:

altHash = [ altHashKey \in HashKey |-> Nil ],

call PerformOP( tuple1 );

call PerformOP( tuple1 );

Case 2:

altHash = [ altHashKey \in HashKey |-> Nil ],

call PerformOP( tuple2 );

call PerformOP( tuple2 );

Case 3:

altHash = [ altHashKey \in HashKey |-> Nil ],

call PerformOP( tuple1 );

call PerformOP( tuple2 );call PerformOP( tuple1 );

Case 4:

altHash = [ altHashKey \in HashKey |-> Nil ],

call PerformOP( tuple2 );

call PerformOP( tuple1 );call PerformOP( tuple2 );

Again, if this fragment:

is really running this kind of state exploration ...** mark me down as extremely impressed**

while (TRUE) {

with k \in HashKey, v \in HashValue, op \in ClientOps {

call PerformOp(k,v,op)

}

}

is really running this kind of state exploration ...

On Tuesday, November 24, 2020 at 2:43:10 AM UTC-5 Stephan Merz wrote:

Why don't you just write a loop of the formwhile (TRUE) {with k \in HashKey, v \in HashValue, op \in ClientOps {call PerformOp(k,v,op)}}TLC will explore all possible sequences of operation calls, for all possible combinations of arguments. Whenever it runs into a state that it has seen before (because the store has the same value for every key), it will stop exploring that branch. The power of model checking is that it lets you explore even infinite executions over finite state spaces. There's no need to materialize the search that TLC will perform in the data structures of your specification.Regards,StephanOn 23 Nov 2020, at 18:31, recepient recepient <nets...@xxxxxxxxx> wrote:Hi -

I'm working on a distributed KV store in Pluscal. Using TLA+ our desire is to ``SQLtise" our Pluscal code everywhere possible: describe what is to be done & checked without proscribing the steps ala imperative code to TLA+. Granted, we can fly closer to that mentality by avoiding Pluscal altogether ... but that's out of scope for the moment.

I am stuck on one basic aspect of this work which seems to exist right at theboundary between allowing TLA+ to explore reachable states, and me telling itwhat I think reachable states are...Assume:key \in {0,1}, value \in {100,101}, {OP_GET, OP_PUT, OP_DELETE} for {0,1} \X {100,101} \X {OP_GET_PUT,OP_DELETE} or 12 unique possible client requests. (Note: get/delete operations never use the value part).:

GoalHave TLA+ check correctness properties (not shown) by exploring all possible ways a client can send KV requests. Imperatively all possible ways are given by:

For each subset s in {0,1} \X {100,101} \X {OP_GET_PUT,OP_DELETE}:

For each permutation p in s:

(re)initialize model

model check operations in p by running p[i] where i \in 1..Len(p)Candidate Process 1 (elided): BAD: Doesn't do all permutations or subsetswith v \in HashKey, v \in HashValue, op \in ClientOpsdo

call PerformOp(k,v.op);end with;Enabling DOT visualization & writing some python to print all paths from initial to final states using the DOT data, we can show that TLA+ tries the first rpc tuple, then tries rpc tuples 1 and 2, then 1 and 2 and 3 ... and on up to 1..12. But that's it!Candidate Process 2 (elided): BAD: Doesn't do permutations or subsets:\* Alternative formulation of process 1. Choose approach much the same ...

with i \in HashKey \X HashValue \X ClientOps

do

call PerformOp(i[1],i[2],i[3]);end with;

At this point TLA+ can't read our minds:it needs to be toldto try all permutations of all subsets. But if one writes writes something like the following, JAVA runs out of stack:Candidate Process 3 (elided): BAD: Won't work; runs out of stackvariables rpcs=Permutations(SUBSET(HashKey, v \in HashValue, op \in ClientOps))with i \in rpcsdo

// now try to dig out individual RPCs and run them...

call PerformOp(....);end with;

Moreover, even if this compiled and ran it's not clear if this achieves the goal. Did it check all permutations on subsets of size 5 starting from the initial state or did it run thaton top of permutations on subsets size 4?What does one do here?--

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...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e3a99dad-9df9-48a9-b0ad-c9ba95a25d7dn%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/ce825f7b-4614-4031-8395-91765f479fe9n%40googlegroups.com.

**Follow-Ups**:

**References**:**[tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store***From:*recepient recepient

**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLC error when choosing an arbitrary value** - Next by Date:
**[tlaplus] Including TLA+ in a Pandoc paper.** - Previous by thread:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Next by thread:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Index(es):