[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: How to implement compare-and-swap in PlusCal?
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.
On Thursday, July 11, 2013 6:53:32 AM UTC-8, marc magrans de abril wrote:
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;
(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
Is it possible to encapsulate a compare-and-swap routine/macro/define in a better way?