[tlaplus] Re: Why multiply keys ops transaction can simply be modeled in high level spec by an action or atomic label?

[Andreas Recke <Andreas.Recke@xxxxxxx>]

Dear inevity,

what primarily proposed was to look what the PlusCal transpiler makes from your code. Normally, code belonging to one label is transpiled to a single action operation and is therefore atomic.

But surprises may always happen, which is why I would suggest to review the resulting TLA+ spec. You should see that the critical action contains what you expect.

Concerning concurrency: maybe you ask for this "I see pink elephants" situation in read-write race conditions?!

There are several TLA+ examples e.g. for mutexes you can find, e.g.this here http://tla.msr-inria.inria.fr/tlaps/doc/IFM2010/Peterson_IFM2010.pdf .

You can actually model concurrency in the degree of abstraction you need. Likewise the type of your variables, which is not implicit.

I case of read-write race conditions, you typically have the problem that there are multiple writes and multiple reads that are intertwined. But also here, parallel atomic [!] actions can

always be modeled as serial atomic actions, just by making the order of actions random or non-determined.

I have a similar problem with concurrency I am trying to specify to check validity of a CUDA kernel. The number of possible parallel threads is so huge that TLC suffers from

state space explosion if I do not use abstraction. Fortunately, CUDA kernels typically use data parallelization which is not too difficult to simplify.

Kind regards

Andreas

ine...@xxxxxxxxx schrieb am Mittwoch, 21. September 2022 um 02:17:40 UTC+2:

In addition: concurrency is modeled serially, but with the possibility of non-determinism to model random order of operations.

The concurrency modeled by the action or label in pluscal look like linearazilibity in txn granularity viewpoint, because the txn complete in an instance point which implied by the atomic semantic of the action or label? Or in txn consistency term, the concurrency should be strict serialization, or external consistency, or even more strong than strict serialization/external consistency.

As for single op consistency in the txn,  it is linearizalibility, though tla model as random order of operations.

Can someone  review in detail my comment about the txn modeled by tla action/label  to make my understandering clear?

 

Thanks 

在2022年9月20日星期二 UTC+8 15:22:17<Andrea...@xxxxxxx> 写道：

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/4ff42d34-be3c-4c81-86a1-8ca665025344n%40googlegroups.com.