Skip to content

Commit

Permalink
complete lclist example with recursive predicates
Browse files Browse the repository at this point in the history
  • Loading branch information
@nisarg-certora
nisarg-certora committed Dec 23, 2024
1 parent 41844ef commit 56efd71
Showing 1 changed file with 237 additions and 34 deletions.
271 changes: 237 additions & 34 deletions test/comparison/lclist.rav
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,18 @@
include "../concurrent/lock/lock.rav"

interface LCList {


// definitions

interface Ref_Type: Library.Type {
rep type T = Ref
}
module Agree = Library.Agree[Ref_Type]

field next: Ref
field lock: Ref
field value: Int
ghost field agr: Agree

module NodeResource: LockResource {
rep type T = (Ref, Int)
Expand All @@ -21,65 +29,260 @@ interface LCList {
requires resource(r) && resource(r)
ensures false
{
// unfold resource(r);
// unfold resource(r);
assume false;
unfold resource(r);
unfold resource(r);
}
}

module LCLock = Lock[NodeResource]

import NodeResource._
import LCLock._
import NodeResource.resource
import NodeResource.exclusive
import LCLock.is_lock

pred is_list(n: Ref, v: Int) {
inv is_list(n: Ref, v: Int) {
n == null ? true :
(exists b: Bool, l: Ref :: own(n.lock, l, 1.0) && is_lock(l, (n, v), b))
(exists b: Bool, l: Ref :: own(n.lock, l, 1.0) && own(n.agr, Agree.agree(l)) && is_lock(l, (n, v), b))
}

proc create()
returns (r: Ref)
ensures is_list(r, 0)
// helper functions

proc release_lock_high(n: Ref, vn: Int)
requires is_list(n, vn) && n != null
requires resource((n, vn))
ensures is_list(n, vn)
{
// below fold generates an error "Internal Error: Expected inv function call (e/own)."
//fold is_list(null, 0);
unfold is_list(n, vn);
var l: Ref := n.lock;
fold is_list(n, vn);

// below assume makes it vacuous
// assume is_list(null, 0);
unfold is_list(n, vn);
{!
ghost var b: Bool;
b :| is_lock(l, (n, vn), b);
if (b == false) {
unfold is_lock(l, (n, vn), b);

// below works as expected
inhale is_list(null, 0);

r := new(next: null, value: 0, lock: null);
// Below should work, instead we get an error:
// Verification Error: Cannot call exclusive. The invariant
// is_list required by exclusive is not available in the current mask.
// NodeResource.exclusive((n, vn));

assert own(r.next, null, 1.0)
&& own(r.value, (r, 0)#1, 1.0)
&& (0 <= 0)
&& is_list(null, 0);
unfold resource((n, vn));
unfold resource((n, vn));
}
!}
LCLock.release(l);
fold is_list(n, vn);
}

// below fold generates "Internal Error: Expected inv function call (e/own)."
// fold resource((r, 0));
proc create_node(nx: Ref, v: Int, vx: Int)
returns (n: Ref)
requires is_list(nx, vx) && v <= vx
ensures is_list(n, v) && n != null
{
n := new(next: nx, value: v, lock: null);
fold resource((n, v))[nx := nx, vx := vx];
var l: Ref;
l := LCLock.create((n,v));
n.lock := l;
n := new(agr: Agree.agree(l));
fold is_list(n, v);
}

// below assert also makes it vacuous
// assume resource((r, 0));
// algorithms

// below works as expected
exhale own(r.next, null, 1.0) && own(r.value, 0, 1.0);
inhale resource((r,0));
proc create_buggy()
returns (r: Ref)
ensures is_list(r, 0) && r != null
{
fold is_list(null, 0);

r := new(next: null, value: 0, lock: null, agr: Agree.agree(null));

fold resource((r, 0))[nx := null, vx := 0];

var l: Ref;
l := LCLock.create((r,0));
r.lock := l;
assert is_lock(l, (r,0), false);
assert r != null;
assert r == null ? true : (own(r.lock, l, 1.0) && is_lock(l, (r, 0), false));

// this fold should generate an error, but it does not
fold is_list(r, 0);
// assert false;
return r;
}

proc create()
returns (r: Ref)
ensures is_list(r, 0) && r != null
{
fold is_list(null, 0);
r := create_node(null, 0, 0);
return r;
}

proc traverse(p: Ref, c: Ref, k: Int, vp: Int, implicit ghost vc: Int)
returns (p': Ref, c': Ref, vp': Int, vc': Int)
requires is_list(p, vp) && is_list(c, vc) && c != null
requires own(p.next, c, 1.0) && own(p.value, vp, 1.0) && (vp < k) && (vp <= vc)
ensures is_list(p', vp') && is_list(c', vc')
ensures own(p'.next, c', 1.0) && own(p'.value, vp', 1.0) && (vp' < k)
ensures c' != null ==> resource((c', vc')) && (k <= vc')
{
unfold is_list(c, vc);
var cl: Ref := c.lock;
fold is_list(c, vc);

unfold is_list(c, vc);
LCLock.acquire(cl);
fold is_list(c, vc);

ghost var vcn: Int;
unfold resource((c, vc))[vcn := vx];
var cn: Ref := c.next;
var vcc: Int := c.value;

if (k <= vcc) {
fold resource((c, vc))[nx := cn, vx := vcn];
return (p, c, vp, vcc);
} else {
fold resource((p, vp))[nx := c, vx := vc];
release_lock_high(p, vp);

if (cn == null) {
fold is_list(null, 0);
return (c, null, vcc, 0);
} else {
p', c', vp', vc' := traverse(c, cn, k, vcc, vcn);
return (p', c', vp', vc');
}
}
}

proc find(r: Ref, k: Int)
returns (p: Ref, c: Ref, vp: Int, vc: Int)
requires k > 0
requires is_list(r, 0) && r != null
ensures is_list(p, vp) && is_list(c, vc)
ensures own(p.next, c, 1.0) && own(p.value, vp, 1.0) && (vp < k)
ensures c != null ==> resource((c, vc)) && (k <= vc)
{
unfold is_list(r, 0);
var rl: Ref := r.lock;
fold is_list(r, 0);

unfold is_list(r, 0);
LCLock.acquire(rl);
fold is_list(r, 0);

ghost var vn: Int;
unfold resource((r, 0))[vn := vx];
var n: Ref := r.next;

if (n == null) {
var rv: Int := r.value;
fold is_list(null, k);
return (r, null, rv, k);
} else {
p, c, vp, vc := traverse(r, n, k, 0, vn);
}
}

proc search(r: Ref, k: Int)
returns (res: Bool)
requires k > 0
requires is_list(r, 0) && r != null
ensures true
{
var p: Ref; var c: Ref; var vp: Int; var vc: Int;
p, c, vp, vc := find(r, k);

if (c == null) {
fold is_list(null, vp);
fold resource((p, vp))[nx := null, vx := vp];
release_lock_high(p, vp);
return false;
} else {
fold resource((p, vp))[nx := c, vx := vc];
release_lock_high(p, vp);
release_lock_high(c, vc);
return (vc == k);
}
}

proc insert(r: Ref, k: Int)
returns (res: Bool)
requires k > 0
requires is_list(r, 0) && r != null
ensures true
{
var p: Ref; var c: Ref; var vp: Int; var vc: Int;
p, c, vp, vc := find(r, k);

if (c == null) {
fold is_list(null, k);
var n: Ref;
n := create_node(null, k, k);
p.next := n;
fold resource((p, vp))[nx := n, vx := k];
release_lock_high(p, vp);

return true;
} else {
if (vc == k) {
fold resource((p, vp))[nx := c, vx := vc];
release_lock_high(p, vp);
release_lock_high(c, vc);

return false;
} else {
var n: Ref;
n := create_node(c, k, vc);
p.next := n;
fold resource((p, vp))[nx := n, vx := k];
release_lock_high(p, vp);
release_lock_high(c, vc);

return true;
}
}
}

proc delete(r: Ref, k: Int)
returns (res: Bool)
requires k > 0
requires is_list(r, 0) && r != null
ensures true
{
var p: Ref; var c: Ref; var vp: Int; var vc: Int;
p, c, vp, vc := find(r, k);

if (c == null) {
fold is_list(null, vp);
fold resource((p, vp))[nx := null, vx := vp];
release_lock_high(p, vp);

return false;
} else {
if (vc == k) {
ghost var vcn: Int;
unfold resource((c, vc))[vcn := vx];
var cn: Ref := c.next;
fold resource((c, vc))[nx := cn, vx := vcn];
p.next := cn;
fold resource((p, vp))[nx := cn, vx := vcn];

release_lock_high(p, vp);
release_lock_high(c, vc);

return true;
} else {
fold resource((p, vp))[nx := c, vx := vc];
release_lock_high(p, vp);
release_lock_high(c, vc);

return false;
}
}
}
}

0 comments on commit 56efd71

Please sign in to comment.