[tlaplus] how to improve concurrency of process

[陈云星 <chen.yack@xxxxxxxxx>]

each Label is an atomic action.

but in general programming language, each _expression_/statement concurrency with other thread.

so, how to express fine-grain atomic action unit in PlusCal ?

for example in a CAS style while loop. each statement/_expression_ is concurrency with other thread:

while(!lock.get() && lock.compareAndSet(false, true)) {
   // do action 1
   // do action 2
   // ...
}

I want each one is atomic (concurrency unit). 

add a label to each statement/_expression_ will be very tedious.

can any cleaner manner ?

-- 
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/2967a186-d501-4e78-b97c-d6d9f30183db%40googlegroups.com.