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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

> On Sep 7, 2022, at 5:34 AM, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
> 
> 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
> 
> 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/4C745657-18EF-406E-8471-EF4D87B9702E%40lemmster.de.