[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Why multiply keys ops transaction can simply be modeled in high level spec by an action or atomic label?
Dear inevity,
the best way to understand the atomicity of TLA actions from PlusCal is to translate the PlusCal code and see the output.
Each label is associated with a variable that changes from one PlusCal step to the next.
Assignments and transactions in PlusCal will be transpiled into the specific TLA+ description, which is quite different from
what one might expect from a programming language.
Each action is atomic and simply describes the current state (unprimed) and the next state (primed).
E.g.
Action == var1 = 1 /\ var2 = "label 1" /\ var3 = "content1" /\
var1' = var1 + 2 /\ var2 = "label 2" /\ var3' = "next content"
Remember, each "=" is not an assignment, just a description. Whenever "Action" happens, the system is in the state
described by
var1 = 1 /\ var2 = "label 1" /\ var3 = "content1" and the next state of the variables is
var1' = var1 + 2 /\ var2 = "label 2" /\ var3' = "next content" . In the next state var1' becomes var1 etc.
This is how atomicity is modeled.
In addition: concurrency is modeled serially, but with the possibility of non-determinism to model random order of operations.
I hope this could answer your question.
Kind regards
Andreas
ine...@xxxxxxxxx schrieb am Dienstag, 20. September 2022 um 04:52:45 UTC+2:
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?
Or this way is the 1 phase transaction commit?
Can some one explain the concurrency control this way provide?
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/eacf29d2-82ec-4e1d-a8bd-38d460838223n%40googlegroups.com.