How do we use the transaction api in spec？

[保建国]

Such as we write an distributed app spec which need access db.

For multiply keys  transaction access, we just wrapped  it's ops as an action or  put in a label if using pluscal. Is is enough ?  In my humble knowledge, this way just enable single key linearizablity and transaction atomic.  but no transaction isolation, am i right?

Always we may need external consistency or strict Serializable , or serializable , even snapshot isolation level.

So how do we use this api in an spec?

I see too many spec impl transaction to verfiy the consistency  or the atomic. But What is the transaction api it expose? such as beginop,  keyops, commit/abort?

 

[Andrew Helwer]

If you want functionality like snapshot isolation for each transaction you'll need to write the logic in TLA+ yourself. There is an example of a key-value store with snapshot isolation on the wikipedia article: https://en.wikipedia.org/wiki/TLA%2B#Examples

Andrew

[Markus Kuppe]

You might find inspiration on how to model various consistency levels of a key-value store at https://github.com/tlaplus/azure-cosmos-tla.

Markus

[保建国]

I think OpenTx(t),Add(t, k, v),Update(t, k, v),Remove(t, k),RollbackTx(t),CloseTx(t) in the example are the txn apis, In my spec  i can instant the example spec and use those api. 

[保建国]

Just another question:

For multiply keys  transaction access, we just wrapped  it's ops as an action which is atomic or  put in a label if using pluscal.   In my humble knowledge,  this way will impl  multiply keys  transaction  atomic. But no any concurrency control, and no any concurrency  the txns can use, so the performance will low.  Am i right?  

For some spec which use the kv/db txn api,  Why can we use this way to model the kv/db txn api?  

[保建国]

You might find inspiration on how to model various consistency levels

The cosmos db specs is just for single key consistency. 

And Look like the simple model spec which added recently can be used by other spec, because it model kv have multiply keys. 

Anyway, your suggest lead me found the update of the specs.