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

[tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store



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 the boundary between allowing TLA+ to explore reachable states, and me telling it what 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).

Goal
:
Have 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 subsets
    with v \in HashKey, v \in HashValue, op \in ClientOps  
    do
       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 told to 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 stack
    variables rpcs=Permutations(SUBSET(HashKey, v \in HashValue, op \in ClientOps))
    with i \in rpcs
    do
       // 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 that on 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e3a99dad-9df9-48a9-b0ad-c9ba95a25d7dn%40googlegroups.com.