Re: How to implement compare-and-swap in PlusCal?

[Leslie Lamport <tlapl...@xxxxxxxxx>]

Hi Marc,

 

In PlusCal, an atomic action is the execution of code (within a single
process) from one label to the next.  Since a macro cannot contain a
label, its execution is part of an atomic action.

 

Your macro should cause a translator error because it contains two
assignments to the same variable (the one substituted for `succes')
without an intervening label.  (The error will occur at a use of the
macro.)  You can fix that by simply moving the `succes := FALSE'
statement to a `then' clause of the `if' statement.

 

I don't know what you mean by "incrementing" z atomically. In the code
you wrote, the `while' must have a label.  (I suggest not using the option
of letting the translator add labels, since you should insert the labels
yourself if you're not sure what's going on.)  With the fix I suggested
above, your CAS macro looks fine to me.  I don't know if there's a better
way since I don't know what you're trying to do.

 

Leslie Lamport

 

On Thursday, July 11, 2013 6:53:32 AM UTC-8, marc magrans de abril wrote:

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