[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

non-atomic assignments (noob question)

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!