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

How to implement compare-and-swap in PlusCal?


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; 
  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:

while (~ done) do
end while

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