Added dune tests for currently working examples

test/concurrent/counter/counter.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./counter.rav
+  Verification successful.

test/concurrent/counter/counter_monotonic.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./counter_monotonic.rav
+  Verification successful.

test/concurrent/counter/counter_no_inv.rav

@@ -1,24 +1,66 @@
-module IntTp : Library.Type {
-  rep type T = Int
+field c: Int
+
+pred counter(x: Ref; v: Int) {
+  own(x, c, v, 1.0)
 }
 
-module IntSetRA = Library.SetRA[IntTp]
+proc incr(x: Ref, implicit ghost v: Int) 
+  atomic requires counter(x, v)
+  atomic ensures counter(x, v + 1)
+{
+  var phi: AtomicToken := bindAU();
+
+  var v1: Int;
 
-type T = Int
+  ghost var v2: Int := openAU(phi);
 
-field c: T
+  unfold counter(x, v2);
+  v1 := x.c;
+  fold counter(x, v2);
+
+  abortAU(phi);
+
+  var new_v1 : Int := v1 + 1;
 
-type Something = data { case onething(a: Int); case nothing } 
+  var v3: Int := openAU(phi);
 
-pred counter(x: Ref; v: Int) {
-  own(x, c, 0, 1.0)
+  unfold counter(x,v3);
+
+  var res: Bool := cas(x.c, v1, new_v1);
+
+  {! 
+    if (res) {
+      fold counter(x, new_v1);
+      commitAU(phi);
+    } else {
+      fold counter(x, v3);
+      abortAU(phi);
+    }
+  !}
+
+  if (!res) {
+    var v4: Int := openAU(phi);
+    incr(x);
+    commitAU(phi);
+  }
 }
 
-proc incr(x: Ref) 
-  requires counter(x, 0)
-  ensures counter(x, 1)
+proc read(x: Ref, implicit ghost v: Int)
+  returns (v2: Int)
+  atomic requires counter(x, v)
+  atomic ensures counter(x, v) && v2 == v
+  ensures v2 == v
+
 {
-  var v: Something = onething(5);
-  // var res: Bool := CAS(x.c, IntSetRA.set_constr({||}), IntSetRA.set_constr({||}));
-  var res: Bool := CAS(x.c, 0, 1);
+  var phi: AtomicToken := bindAU();
+
+  var v1: Int := openAU(phi);
+  unfold counter(x, v1);
+
+  var v3: Int := x.c;
+
+  fold counter(x, v1);
+  commitAU(phi, v3);
+
+  return v3;
 }

test/concurrent/counter/counter_no_inv.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./counter_no_inv.rav
+  Verification successful.

test/concurrent/counter/dune

@@ -0,0 +1,6 @@
+(cram
+ (deps
+  %{project_root}/bin/raven.exe
+  %{project_root}/lib/library/resource_algebra.rav
+  (:rav
+   (glob_files_rec *.rav))))

test/concurrent/lock/dune

@@ -0,0 +1,6 @@
+(cram
+ (deps
+  %{project_root}/bin/raven.exe
+  %{project_root}/lib/library/resource_algebra.rav
+  (:rav
+   (glob_files_rec *.rav))))

test/concurrent/lock/spin-lock.rav

@@ -20,38 +20,31 @@ interface Lock {
     fold lockR(l, false);
   }
 
-  /* How to prove following spec? Lob induction? */
   proc acquire(l: Ref, implicit ghost b: Bool)
     atomic requires lockR(l, b)
     atomic ensures lockR(l, true) && lockResource(l)
   {
     ghost val phi: AtomicToken = bindAU();
 
-    ghost var b1 : Bool;
-    b1 := openAU(phi);
+    ghost var b1 : Bool := openAU(phi);
     unfold lockR(l, b1);
-    // var res := cas(l.bit, false, true);
-    ghost var res: Bool;
-    {!
-      ghost var curr_val: Bool := l.bit;
 
-      if (curr_val == false) {
-        l.bit := true;
-        res := true;
+    val res: Bool := cas(l.bit, false, true);
+
+    {!
+      if (res) {
+        fold lockR(l, true);
+        commitAU(phi);
       } else {
-        res := false;
+        fold lockR(l, b1);
+        abortAU(phi);
       }
     !}
 
     if (res) {
-      l.bit := true;
-      fold lockR(l, true);
-      commitAU(phi);
       return;
-    } else {
-      fold lockR(l, b1);
-      abortAU(phi);
     }
+
     b1 := openAU(phi);
     assert lockR(l, b1);
     acquire(l);

test/concurrent/lock/spin-lock.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./spin-lock.rav
+  Verification successful.

test/concurrent/templates/ccm_instances.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./ccm_instances.rav
+  Verification successful.

test/concurrent/templates/dune

@@ -0,0 +1,6 @@
+(cram
+ (deps
+  %{project_root}/bin/raven.exe
+  %{project_root}/lib/library/resource_algebra.rav
+  (:rav
+   (glob_files_rec *.rav))))

test/concurrent/templates/flows_ra.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./flows_ra.rav
+  Verification successful.

test/concurrent/templates/give-up_sequential.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./give-up_sequential.rav
+  Verification successful.

test/concurrent/templates/single-node_working.rav

@@ -22,22 +22,10 @@ module Lock {
     atomic ensures lock(l, true) && b == false
   {
     val phi: AtomicToken := bindAU();
-    val b1: Bool;
-    b1 := openAU(phi);
+    val b1: Bool := openAU(phi);
     unfold lock(l, b1); 
 
-   	// val res = cas(l.bit, false, true); 
-    ghost var res: Bool;
-    {!
-      ghost var curr_val: Bool := l.bit;
-
-      if (curr_val == false) {
-        l.bit := true;
-        res := true;
-      } else {
-        res := false;
-      }
-    !}
+   	val res: Bool = cas(l.bit, false, true); 
 
     {!
       if (res) {
@@ -52,8 +40,7 @@ module Lock {
     !}
 
     if (!res) {
-      val b2: Bool;
-      b2 := openAU(phi);
+      val b2: Bool := openAU(phi);
 			assert lock(l, b2);
 			acquire(l);
 			commitAU(phi);
@@ -64,7 +51,7 @@ module Lock {
     atomic requires lock(l, true)
     atomic ensures lock(l, false)
   {
-    val phi: AtomicToken;
+    var phi: AtomicToken;
     {! 
       phi := bindAU();
       openAU(phi);
@@ -160,28 +147,10 @@ interface SearchStructure {
 interface SingleNodeTemplate[Node: NodeImpl] {
   field lock: Bool
 
-  // module KeyMod : Library.Type {
-  //   rep type T = Set[Node.Spec.K]
-  // }
-
-  // module FracSK = Node.Spec.K
-
-
   module Spec: SearchStructureSpec = Node.Spec
 
-  // import Node.Spec.K
-  // import Node.Spec.Op
-  // import Node.Spec.opSpec
-  // import Node.Spec.keyset
-
-  // import Spec._
   import Node.Spec._
 
-  // import Spec.K
-  // import Spec.Op
-  // import Spec.opSpec
-  // import Spec.keyset
-
   field frac: Set[K];
 
   pred cssR(r: Ref, c: Set[K]) {
@@ -207,7 +176,6 @@ interface SingleNodeTemplate[Node: NodeImpl] {
     r := new(lock:false, frac:{||});
     assert own(r, frac, {||}, 0.5) && own(r, lock, false, 1.0) && 
       (false ? true : (Node.nodeR(r, {||}) && own(r, frac, {||}, 0.5)));
-    // assert own(r, lock, false, 1.0) && (false ? true : Node.nodeR(r, {||}));
     fold cssR(r, {||});
   }
 

test/concurrent/templates/single-node_working.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./single-node_working.rav
+  Verification successful.

test/concurrent/treiber_stack/dune

@@ -0,0 +1,6 @@
+(cram
+ (deps
+  %{project_root}/bin/raven.exe
+  %{project_root}/lib/library/resource_algebra.rav
+  (:rav
+   (glob_files_rec *.rav))))

test/concurrent/treiber_stack/treiber_stack_atomics.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./treiber_stack_atomics.rav
+  Verification successful.

test/iterated-star/array-max.rav

@@ -8,84 +8,90 @@ interface IArray {
   func first(r: Ref) returns (a: T)
   func second(r: Ref) returns (i: Int)
 
-  lemma all_diff(a: T, i: Int)
-    ensures first(loc(a, i)) == a && second(loc(a, i)) == i
+  auto lemma all_diff()
+    ensures forall a:T, i: Int :: first(loc(a, i)) == a && second(loc(a, i)) == i
 
-  lemma len_nonneg(a: T)
-    ensures len(a) >= 0
+  auto lemma len_nonneg()
+    ensures forall a:T :: len(a) >= 0
 }
 
-module ArrayMax[Arr: IArray] {
-  field val: Int
+module ArrayMax[M: IArray] {
+  field value: Int
 
-  define arr(a: Arr, m: Map<Int, Int>) {
-    forall j: Int :: 0 <= j < len(a) ==> own(loc(a, j).val, (1, m[i]))
+  pred arr(a: M, m: Map[Int, Int]) {
+    forall j: Int :: 0 <= j < M.len(a) ==> own(M.loc(a, j), value, m[j], 1.0)
   }
 
-  // old keyword?
-  //define untouched(a: Arr) {
-  //  forall j: Int :: 0 <= j < len(a) ==> loc(a, j).val == old(loc(a, j).val)
-  //}
-
-  define is_max(i: Int, m: Map<Int, Int>, u: Int) {
+  pred is_max(i: Int, m: Map[Int, Int], u: Int) {
     forall j: Int :: 0 <= j && j < u ==> m[j] <= m[i]
   }
 
-  proc max(a: Arr, implicit ghost m: Map<Int, Int>) 
+  proc max(a: M, implicit ghost m: Map[Int, Int]) 
     returns (x: Int)
     requires arr(a, m)
     ensures  arr(a, m)
-    ensures  len(a) == 0 ? x == -1 : (0 <= x && x < len(a))
-    ensures  is_max(x, m, len(a))
+    ensures  M.len(a) == 0 ? x == -1 : (0 <= x && x < M.len(a))
+    ensures  is_max(x, m, M.len(a))
   {
-    if (len(a) == 0) {
-      x := -1
+    M.all_diff();
+    M.len_nonneg();
+    var z : Int;
+    if (M.len(a) == 0) {
+      x := -1;
     } else {
-      var y: Int
+      var y: Int;
       x := 0;
-      y := len(a) - 1;
+      y := M.len(a) - 1;
 
       while (x != y)
         invariant arr(a, m)
-        invariant 0 <= x && x <= y && y < len(a)
+        invariant 0 <= x && x <= y && y < M.len(a)
         invariant    (forall i: Int ::
-                            ((0 <= i && i < x) || (y < i && i < len(a)))
-                        ==> m[i] < m[x])
-                  || (forall i: Int ::
-                            ((0 <= i && i < x) || (y < i && i < len(a)))
+                            (((0 <= i && i < x) || (y < i && i < M.len(a)))
+                        ==> m[i] < m[x]) || 
+                        (((0 <= i && i < x) || (y < i && i < M.len(a)))
                         ==> m[i] <= m[y])
+                        )
       {
-        if (loc(a, x).val <= loc(a, y).val) {
-          x := x + 1
+        M.all_diff();
+        unfold arr(a,m);
+
+        var tmp1 : Int  = M.loc(a, x).value;
+        var tmp2 : Int = M.loc(a, y).value;
+
+        if (tmp1 <= tmp2) {
+          x := x + 1;
         } else {
-          y := y - 1
+          y := y - 1;
         }
+        fold arr(a,m);
       }
     }
-  }
-
-
 
+    fold is_max(x, m, M.len(a));
+  }
 
-(*
+
+/*
 method client() {
   var a: IArray
   inhale len(a) == 3
   inhale access(a)
-  inhale forall i: Int :: 0 <= i && i < len(a) ==> loc(a, i).val == i
+  inhale forall i: Int :: 0 <= i && i < len(a) ==> loc(a, i).value == i
 
   var x: Int
   x := max(a)
 
-  assert loc(a, 0).val <= x
+  assert loc(a, 0).value <= x
 
-  assert x == loc(a, len(a) - 1).val
-    /* Necessary to prove the final assertion (due to triggering) */
+  assert x == loc(a, len(a) - 1).value
+    // Necessary to prove the final assertion (due to triggering)
 
   assert x == 2
 
-  assert loc(a, 1).val < x
+  assert loc(a, 1).value < x
+}
+*/
 }
-*)
 
 

test/iterated-star/array-max.t

@@ -0,0 +1,2 @@
+  $ dune exec -- raven --shh ./array-max.rav
+  Verification successful.