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

[tlaplus] Re: How do we use the transaction api in spec?

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?  

在2022年9月8日星期四 UTC+8 10:45:24<保建国> 写道:
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. 

在2022年9月7日星期三 UTC+8 20:34:30<andrew...@xxxxxxxxx> 写道:
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


On Tuesday, September 6, 2022 at 10:53:51 PM UTC-4 ine...@xxxxxxxxx wrote:
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?

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/947b7cbc-8fd6-48a8-a9bb-f86cc42ef53dn%40googlegroups.com.