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).
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
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.
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?