spin-lock.rav

include "lock.rav"

module SpinLock[R: LockResource] : Lock {
  field bit: Bool
  
  import R.resource
  
  auto pred lock_rep(l: Ref; b: Bool) {
    own(l.bit, b, 1.0)
  }

  proc create(r: R)
    returns (l: Ref)
    requires resource(r)
    ensures is_lock(l, r, false)
  {
    l := new (bit: false, agr: Agree.agree(r));
  }

  proc acquire(l: Ref, implicit ghost r: R, implicit ghost b: Bool)
    atomic requires is_lock(l, r, b)
    atomic ensures is_lock(l, r, true) && b == false && resource(r)
  {
    ghost val phi := bindAU();
        
    ghost var b1: Bool;
    r, b1 := openAU(phi);
    val res: Bool := cas(l.bit, false, true);
    
    if (res) {
      commitAU(phi);
      return;
    } else {
      abortAU(phi);
    }

    r, b1 := openAU(phi);
    acquire(l, r, b1);
    commitAU(phi);
  }
  
  proc release(l: Ref, implicit ghost r: R)
    atomic requires is_lock(l, r, true) && resource(r)
    atomic ensures is_lock(l, r, false)
  {
    ghost val phi := bindAU();  
    r := openAU(phi);
    l.bit := false;
    commitAU(phi);
  }
}