septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Conditionals in atomic sections #141

Open septract opened 7 years ago

septract commented 7 years ago

(This is pulled out from the broader issue #105)

Conditionals in atomic sections would be very useful in the MCS queue (see #133) where we need a compareAndSet operation over Starling variables. I want to write something like the following:

method unlock (Node qnode) { 
  ...
  < if (qnode == tail) { 
        tail = null;
        test = true; 
     } else { 
        test = false
     }  > ;  
  ...
} 

The only way to do this at the moment is (I think) to piggyback on GRASShopper's if statement, which is dumb:

method unlock (Node qnode) { 
  ...
  < test = ( tail == qnode ); 
    tail = %{ if ( [|test|] ) { null } else { [|tail|] } }; > ;  
  ...
} 

I think @MattWindsor91 also ran into this when he was trying to encode the Treiber stack.