Chalice: Re-designed lockchange on methods and loops. The lockchange clause is now required to list all objects whose held or rdheld field has changed since the _method_ prestate. It seems desirable to exclude objects that were not allocated in the prestate, but this feature is not implemented yet.

4 files changed, 167 insertions, 11 deletions

diff --git a/Chalice/examples/Answer b/Chalice/examples/Answer
index e8ca406d..5df00502 100644
--- a/Chalice/examples/Answer
+++ b/Chalice/examples/Answer
@@ -6,10 +6,10 @@ Boogie program verifier finished with 31 verified, 1 error
 ------ Running regression test counter.chalice 

   69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.

   80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.

-  119.5: The target of the release statement might be not be locked by the current thread.

+  119.5: The target of the release statement might not be locked by the current thread.

   128.7: The mu field of the target of the acquire statement might not be above waitlevel.

   136.7: The mu field of the target of the acquire statement might not be above waitlevel.

-  145.5: The target of the release statement might be not be locked by the current thread.

+  145.5: The target of the release statement might not be locked by the current thread.

 

 Boogie program verifier finished with 24 verified, 6 errors

 ------ Running regression test dining-philosophers.chalice 

@@ -201,12 +201,14 @@ Boogie program verifier finished with 24 verified, 4 errors
 Boogie program verifier finished with 51 verified, 4 errors

 ------ Running regression test prog4.chalice 

   5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.

-  15.7: The target of the release statement might be not be locked by the current thread.

-  15.7: Release might fail because the current thread might hold the read lock.

-  27.7: The target of the release statement might be not be locked by the current thread.

-  27.7: Release might fail because the current thread might hold the read lock.

-

-Boogie program verifier finished with 6 verified, 5 errors

+  17.7: The target of the release statement might not be locked by the current thread.

+  17.7: Release might fail because the current thread might hold the read lock.

+  30.7: The target of the release statement might not be locked by the current thread.

+  30.7: Release might fail because the current thread might hold the read lock.

+  34.5: The target of the release statement might not be locked by the current thread.

+  34.5: Release might fail because the current thread might hold the read lock.

+

+Boogie program verifier finished with 6 verified, 7 errors

 ------ Running regression test ImplicitLocals.chalice 

 

 Boogie program verifier finished with 8 verified, 0 errors

@@ -232,6 +234,12 @@ Boogie program verifier finished with 5 verified, 0 errors
   123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.

 

 Boogie program verifier finished with 19 verified, 4 errors

+------ Running regression test LoopLockChange.chalice 

+  10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.

+  35.5: The loop might lock/unlock more than the lockchange clause allows.

+  65.5: The loop might lock/unlock more than the lockchange clause allows.

+

+Boogie program verifier finished with 14 verified, 3 errors

 ------ Running regression test cell-defaults.chalice 

   96.5: The heap of the callee might not be strictly smaller than the heap of the caller.

   102.5: The heap of the callee might not be strictly smaller than the heap of the caller.

diff --git a/Chalice/examples/HandOverHand.chalice b/Chalice/examples/HandOverHand.chalice
index 8318a77c..307b653c 100644
--- a/Chalice/examples/HandOverHand.chalice
+++ b/Chalice/examples/HandOverHand.chalice
@@ -48,6 +48,7 @@ class List {
     while (p.next != null && p.next.val < x)

       invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)

       invariant holds(p) && waitlevel == p.mu

+      invariant !old(holds(p)) && !old(rd holds(p))

       invariant p.next != null ==> acc(p.next.mu,50) && p << p.next

       invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val

       invariant acc(p.sum, 50)

@@ -88,6 +89,7 @@ class List {
     while (p.next != null && p.next.val < x)

       invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)

       invariant holds(p) && waitlevel == p.mu && !assigned(c)

+      invariant !old(holds(p)) && !old(rd holds(p))

       invariant p.next != null ==> acc(p.next.mu,50) && p << p.next

       invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val

       invariant acc(p.sum, 50)

diff --git a/Chalice/examples/LoopLockChange.chalice b/Chalice/examples/LoopLockChange.chalice
new file mode 100644
index 00000000..5ccce089
--- /dev/null
+++ b/Chalice/examples/LoopLockChange.chalice
@@ -0,0 +1,142 @@
+class LoopLockChange {
+
+  method Test0()
+    requires rd(mu) && waitlevel << mu
+    lockchange this;
+  {
+    acquire this;
+
+    var b := true;
+    while(b)  // error: lockchange clause of loop must include all lock changes that happened before the loop
+    {
+      b := false;
+    }
+  }
+
+  method Test1()
+    requires rd(mu) && waitlevel << mu
+    lockchange this;
+  {
+    acquire this;
+
+    var b := true;
+    while(b)
+      lockchange this;  
+    {
+      b := false;
+    }
+  }
+
+  method Test2()
+    requires rd(mu) && waitlevel << mu
+    lockchange this;
+  {
+    var b := true;
+    while(b)  // error: insufficient lockchange clause
+      invariant rd(mu);
+      invariant b ==> waitlevel << mu
+    {
+      acquire this;
+      b := false;
+    }
+  }
+
+  method Test3()
+    requires rd(mu) && waitlevel << mu
+    lockchange this;
+  {
+    var b := true;
+    while(b)
+      invariant rd(mu);
+      invariant b ==> waitlevel << mu
+      lockchange this;
+    {
+      acquire this;
+      b := false;
+    }
+  }
+
+  method Test4(p: LoopLockChange)
+    requires rd(p.mu) && waitlevel << p.mu
+    requires rd(mu) && waitlevel << mu
+  {
+    var current: LoopLockChange := this;
+    var b := true;
+    while(b)
+      invariant rd(current.mu)
+      invariant b ==> rd(p.mu);
+      invariant b ==> waitlevel << current.mu
+      lockchange current;  // error: after the loop body, current does no longer point to the object whose lock was acquired
+    {
+      acquire current;
+      current := p;
+      b := false;
+    }
+    assume false;  // to prevent complaint about method's lockchange clause
+  }
+
+
+  method Test5(p: LoopLockChange)
+    requires rd(p.mu) && waitlevel << p.mu
+    requires rd(mu) && waitlevel << mu
+    lockchange this;
+  {
+    var current: LoopLockChange := this;
+    var b := true;
+    while(b)
+      invariant rd(current.mu)
+      invariant b ==> rd(p.mu);
+      invariant b ==> current == this;
+      invariant b ==> waitlevel << current.mu
+      lockchange this;
+    {
+      acquire current;
+      current := p;
+      b := false;
+    }
+  }
+
+
+  method Test6()
+    requires rd(mu) && waitlevel << mu
+  {
+    var b := true;
+    while(b)
+      invariant rd(mu);
+      invariant b ==> waitlevel << mu
+      invariant b ==> !(rd holds(this))
+      invariant !b ==> holds(this)
+      lockchange this;
+    {
+      acquire this;
+      b := false;
+    }
+    release this;
+  }
+
+
+  method Test7()
+    requires rd(mu) && waitlevel << mu
+  {
+    acquire this;
+    release this;
+  }
+
+
+// The following test requires a better treatment of allocation, which we don't have yet 
+/*  method Test8()
+  {
+    var tmp : LoopLockChange := this;
+    var b := false;
+    while(b)
+    {
+      tmp := new LoopLockChange;
+      share tmp;
+      acquire tmp;
+      b := false;
+    }
+    assert !holds(tmp);
+  }
+*/
+}
+
diff --git a/Chalice/examples/prog4.chalice b/Chalice/examples/prog4.chalice
index bc6aef99..3c655c71 100644
--- a/Chalice/examples/prog4.chalice
+++ b/Chalice/examples/prog4.chalice
@@ -11,7 +11,9 @@ class LoopTargets {
     share t

     acquire t

     var s := true

-    while (s) {

+    while (s) 

+      lockchange t 

+    {

       release t  // error: loop invariant does not say holds(t) (252)

       s := false

     }

@@ -21,8 +23,9 @@ class LoopTargets {
     share t

     acquire t

     var s := true

-    while (s)

+    while (s) 

       invariant acc(t.mu) && waitlevel == t.mu

+      lockchange t

     {

       release t  // error: loop invariant does not say holds(t) (414)

       acquire t

@@ -35,9 +38,10 @@ class LoopTargets {
     share t

     acquire t

     var s := true

-    while (s)

+    while (s) 

       invariant rd(t.mu)

       invariant holds(t) && waitlevel == t.mu

+      lockchange t

     {

       release t

       acquire t