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!