non-atomic assignments (noob question)

[Michael Slominski]

I’m new to TLA+ and formal specs in general and I’m playing around with generating a spec for a simple lock-free concurrent data structure as a means to learn TLA+ & PlusCal. My question concerns non-atomic assignment and if there is an idiomatic way to specify that an assignment be non-atomic? The only thing I came up with was to split the assignment up with a temporary as in the following PlusCal snippet:

                  ...

         shared_global_var_intermediate’ := new_val;

  label: shared_global_var’ := shared_global_val_intermediate;

         assert shared_global_var = new_val;

         ...

How do others handle this?

Thanks in advance!

[Stephan Merz]

Transitions in TLA+ are atomic, as are groups of PlusCal statements in between two labels. Your approach of splitting assignments into two separate statements, using an auxiliary variable, is the idiomatic way of modeling non-atomic assignments.

Stephan 

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Leslie Lamport]

For a different way of representing non-atomic assignments, see
the specification of the Bakery algorithm at

   http://lamport.azurewebsites.net/tla/boulangerie.html

That way captures the semantics of safe registers, defined in

   http://lamport.azurewebsites.net/pubs/pubs.html#interprocess

Leslie