Re: [tlaplus] how to improve concurrency of process

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

On 18.11.19 23:18, 陈云星 wrote:
> 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 ?

Hi,

since you mention CAS, the spec at [1] models a multithreaded,
shared-memory algorithm including CAS.

Best
Markus

[1]
https://github.com/tlaplus/tlaplus/blob/da85c32ab840e932419cbd3ff608861d07f530bf/tlatools/src/tlc2/tool/fp/OpenAddressing.tla

-- 
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/8a591769-e96d-b25a-e71f-be648d9c6159%40lemmster.de.