Program4Or5DependingOnWhoIsAskingButWithOnlyLayerOfRefinement.bpl.tumblr.com

// RUN: -typeEncoding:m -useArrayTheory
var {:layer 0,1} a:[int]int;

procedure {:yields} {:layer 1} main()
{
    var {:layer 0} {:linear "tid"} tid:int;
    var i: int;

    yield;
    while (true)
    {
        call tid := Allocate();
        async call P(tid);
	yield;
    }
    yield;
}

procedure {:yields} {:layer 1} P({:layer 0} {:linear "tid"} tid: int)
ensures {:layer 1} a[tid] == old(a)[tid] + 1;
{ 
    var t:int;

    yield;
    assert {:layer 1} a[tid] == old(a)[tid];
    call t := Read(tid);
    yield;
    assert {:layer 1} a[tid] == t;
    call Write(tid, t + 1);
    yield;
    assert {:layer 1} a[tid] == t + 1;
}

procedure {:yields} {:layer 0,1} Allocate() returns ({:layer 0} {:linear "tid"} tid: int);
ensures {:atomic}
|{A:
  return true;
}|;

procedure {:yields} {:layer 0,1} Read({:layer 0} {:linear "tid"} tid: int) returns (val: int);
ensures {:atomic}
|{A:
  val := a[tid]; return true;
}|;

procedure {:yields} {:layer 0,1} Write({:layer 0} {:linear "tid"} tid: int, val: int);
ensures {:atomic}
|{A:
  a[tid] := val; return true;
}|;

function {:builtin "MapConst"} MapConstBool(bool): [int]bool;
function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
{
  MapConstBool(false)[x := true]
}