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

*From*: recepient recepient <netsmaza@xxxxxxxxx>*Date*: Mon, 23 Nov 2020 09:31:49 -0800 (PST)

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

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****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]);

-- 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)

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

do

call PerformOp(k,v.op);

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!

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))

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?**

At this point TLA+ can't read our minds:

with i \in rpcs

do

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

call PerformOp(....);

// 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

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.

**Follow-Ups**:

- Prev by Date:
**[tlaplus] Specification as part of an agile software delivery process** - Next by Date:
**[tlaplus] Re: Specification as part of an agile software delivery process** - Previous by thread:
**[tlaplus] Re: Specification as part of an agile software delivery process** - Next by thread:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Index(es):