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

[tlaplus] 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?

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/cc943fe1-e1fc-42c9-b65e-57eae30579f8n%40googlegroups.com.