Linked-List (Predicates)
Inserting into an ordered linked-list which is specified via a recursively-defined predicate. The loop invariant uses a recursively-defined list segment predicate to bookkeep permissions.
/*****************************************************************
* List Nodes
*****************************************************************/
field data: Int
field next: Ref
predicate lseg(this: Ref, end: Ref)
{
this != end ==>
acc(this.data) && acc(this.next) && acc(lseg(this.next, end)) &&
unfolding acc(lseg(this.next, end)) in this.next != end ==> this.data <= this.next.data
}
function contentNodes(this: Ref, end: Ref): Seq[Int]
requires acc(lseg(this, end))
ensures this == end ==> result == Seq[Int]()
ensures this != end ==>
0 < |result| &&
result[0] == unfolding acc(lseg(this, end)) in this.data
ensures forall i: Int, j: Int :: 0 <= i && i < j && j < |result| ==> result[i] <= result[j]
{
this == end ? Seq[Int]() :
unfolding acc(lseg(this, end)) in (
Seq(this.data) ++ contentNodes(this.next, end)
)
}
function lengthNodes(this: Ref, end: Ref): Int
requires acc(lseg(this, end))
ensures result == |contentNodes(this, end)|
{
unfolding acc(lseg(this, end)) in
this == end ? 0 :
1 + lengthNodes(this.next, end)
}
/*****************************************************************
* Lists
*****************************************************************/
field head: Ref
predicate List(this: Ref)
{
acc(this.head) && acc(lseg(this.head, null))
}
function content(this: Ref): Seq[Int]
requires acc(List(this))
ensures forall i: Int, j: Int :: 0 <= i && i < j && j < |result| ==> result[i] <= result[j]
{
unfolding acc(List(this)) in contentNodes(this.head, null)
}
function length(this: Ref): Int
requires acc(List(this))
ensures result == |content(this)|
{
unfolding acc(List(this)) in lengthNodes(this.head, null)
}
function peek(this: Ref): Int
requires acc(List(this))
requires 0 < length(this)
ensures result == content(this)[0]
{
unfolding acc(List(this)) in unfolding acc(lseg(this.head, null)) in this.head.data
}
method create() returns (this: Ref)
ensures acc(List(this))
ensures content(this) == Seq[Int]()
{
this := new(*)
this.head := null
fold acc(lseg(this.head, null))
fold acc(List(this))
}
method concat(this: Ref, ptr: Ref, end: Ref)
requires acc(lseg(this, ptr))
requires acc(lseg(ptr, end))
requires end != null ==> acc(end.next, 1/2)
requires 0 < |contentNodes(this, ptr)| && 0 < |contentNodes(ptr, end)| ==>
contentNodes(this, ptr)[|contentNodes(this, ptr)|-1] <= contentNodes(ptr, end)[0]
ensures acc(lseg(this, end))
ensures contentNodes(this, end) == old(contentNodes(this, ptr) ++ contentNodes(ptr, end))
ensures end != null ==> acc(end.next, 1/2)
{
if(this != ptr)
{
unfold acc(lseg(this, ptr))
concat(this.next, ptr, end)
fold acc(lseg(this, end))
}
}
method insert(this: Ref, elem: Int) returns (index: Int)
requires acc(List(this))
ensures acc(List(this))
ensures 0 <= index && index <= |old(content(this))|
ensures content(this) == old(content(this))[0..index] ++ Seq(elem) ++ old(content(this))[index..]
{
var tmp: Ref
index := 0
unfold acc(List(this))
if(this.head != null) {
unfold acc(lseg(this.head, null))
}
if(this.head == null || elem <= this.head.data) {
tmp := new(*)
tmp.data := elem
tmp.next := this.head
fold acc(lseg(this.head, null))
fold acc(lseg(tmp, null))
this.head := tmp
} else {
var ptr: Ref := this.head
fold acc(lseg(this.head, ptr))
index := index + 1
while(ptr.next != null && unfolding acc(lseg(ptr.next, null)) in ptr.next.data < elem)
invariant acc(this.head)
invariant acc(ptr.next) && acc(ptr.data) && ptr.data <= elem
invariant acc(lseg(ptr.next, null))
invariant acc(lseg(this.head, ptr))
invariant forall i: Int :: 0 <= i && i < |contentNodes(this.head, ptr)| ==>
contentNodes(this.head, ptr)[i] <= ptr.data
invariant forall i: Int :: 0 <= i && i < |contentNodes(ptr.next, null)| ==>
ptr.data <= contentNodes(ptr.next, null)[i]
invariant index-1 == |contentNodes(this.head, ptr)|
invariant
old(content(this)) == contentNodes(this.head, ptr) ++ Seq(ptr.data) ++ contentNodes(ptr.next, null)
{
unfold acc(lseg(ptr.next, null))
index := index + 1
var ptrn: Ref := ptr.next
fold acc(lseg(ptrn, ptrn))
fold acc(lseg(ptr, ptrn))
concat(this.head, ptr, ptrn)
ptr := ptrn
}
tmp := new(*)
tmp.data := elem
tmp.next := ptr.next
ptr.next := tmp
fold acc(lseg(ptr.next, null))
// now we need to concat the remaining segments
fold acc(lseg(ptr, null))
concat(this.head, ptr, null)
}
fold acc(List(this))
}
method dequeue(this: Ref) returns (res: Int)
requires acc(List(this))
requires 0 < length(this)
ensures acc(List(this))
ensures res == old(content(this)[0])
ensures content(this) == old(content(this)[1..])
{
unfold acc(List(this))
unfold acc(lseg(this.head, null))
res := this.head.data
this.head := this.head.next
fold acc(List(this))
}
/*****************************************************************
* CLIENT
*****************************************************************/
/* Monitor invariant:
* acc(List(lock)) && acc(lock.held) && acc(lock.changed)
* && (old[acq](content(lock)) == content(lock) || lock.changed)
*/
field held: Int
field changed: Bool
method test(lock: Ref)
ensures [true, forperm r: Ref [r.held] :: false]
{
/* Acquire lock (without deadlock checking) */
inhale acc(List(lock)) && acc(lock.held) && acc(lock.changed)
label acq
if(2 <= length(lock)) {
var r1: Int
r1 := dequeue(lock)
assert r1 <= peek(lock)
lock.changed := true
}
/* Release lock */
exhale acc(List(lock)) && acc(lock.held) && acc(lock.changed)
&& (old[acq](content(lock)) == content(lock) || lock.changed)
}