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

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

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/906c268e-3fc9-4add-9928-9866809dd831n%40googlegroups.com.