How to implement compare-and-swap in PlusCal?

[marc magrans de abril <marcmagra...@xxxxxxxxx>]

Hi,

I'm new with the PlusCal language. I have done a couple of examples and I have somewhat more experience using TLA+. However, I am not able to implement a compare-and-swap macro/procedure/definition using PlusCal. 

I see that you could do something similar by writing a macro:

macro CAS(succes, current,old,new) begin 
  succes := FALSE; 
  if (current=old) then 
    current := new; 
    succes:=TRUE 
  end if; 
end macro

(BTW, as far as I understand the PlusCal User manual, a macro is executed within the same step is it called. Therefore, it is atomic, right?)

If I use this macro to increment z atomically w/o locking I have the following code:

CAS(done,z,z_old,z_new);
while (~ done) do
  CAS(done,z,z_old,z_new);
end while

Is it possible to encapsulate a compare-and-swap routine/macro/define in a better way?

Thanks,
marc