treiber_stack_atomics.rav

import Library.Type
import Library.Option
import Library.List

module Stack[T: Type] {

  module TOption = Option[T]
  module TList = List[T]
  import TList._
  import TOption._

  field top: Ref
  field next: Ref
  field value: T


  pred list(x: Ref; xs: TList) {
    x == null ? 
      xs == nil : 
      (xs != nil && (exists tl0: Ref, q: Real ::  q > 0.0 && (own(x.value, xs.head, q) && own(x.next, tl0, q) && list(tl0, xs.tail))))
  }

  pred stack(s: Ref; xs: TList) {
    exists x: Ref :: own(s.top, x, 1.0) && list(x, xs)
  }

  proc push(s: Ref, x: T, implicit ghost xs: TList)
    atomic requires stack(s, xs)
    atomic ensures stack(s, cons(x, xs))
  {
    ghost val phi := bindAU();
    ghost val xs0: TList := openAU(phi);

    unfold stack(s);
    var topv := s.top;
    fold stack(s, xs0);

    abortAU(phi);

    var s0 : Ref;
    s0 := new(value: x, next: topv);

    ghost val xs1: TList := openAU(phi);

    ghost val top1: Ref;
    unfold stack(s)[top1 := x];
    
    var res := cas(s.top, topv, s0);

    if (!res) { 
      fold stack(s, xs1);
      abortAU(phi);
      ghost val xs2: TList := openAU(phi);
      push(s, x);
      commitAU(phi);
    } else {
      fold list(s0, cons(x, xs1))[q := 1.0]; 
      fold stack(s, cons(x, xs1));
      commitAU(phi);
    }
  }

  proc pop(s: Ref, implicit ghost xs: TList)
    returns (result: TOption)
    atomic requires stack(s, xs)
    atomic ensures 
      xs == nil ? 
        (stack(s, xs) && result == none) : 
        (stack(s, xs.tail) && result == some(xs.head))
  {
    ghost val phi := bindAU();
    ghost val xs0: TList := openAU(phi);

    unfold stack(s);

    var topv := s.top;
  
    ghost val q: Real; ghost val tl0: Ref;
    
    if (topv == null) {
      unfold list(topv)[q := q];
      fold list(topv, xs0)[q := q];
      fold stack(s, xs0);
      commitAU(phi, none);
    } else {
      unfold list(topv)[tl0 := tl0, q := q];
      fold list(topv, xs0)[q := q/2.0];
      fold stack(s, xs0);
      abortAU(phi);
    }
    
    if (topv == null) {
      return none;
    }

    val top_next := topv.next;
    val top_value := topv.value;

    ghost val xs1: TList := openAU(phi);
    ghost val top1: Ref;
    unfold stack(s)[top1 := x];

    var res := cas(s.top, topv, top_next);

    if (res) {
      unfold list(top1);
      fold stack(s, xs1.tail);
      commitAU(phi, some(top_value));
      return some(top_value);
    } else { 
      fold stack(s, xs1);
      abortAU(phi);
      ghost val xs2: TList := openAU(phi);
      val ret := pop(s);
      commitAU(phi, ret);

      return ret;
    }
  }
}