Implemented -noDeadlockChecks mode. With this mode, it is possible to give some demos that use locks before explaining the global order on locks.

2 files changed, 11 insertions, 3 deletions

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 11481741..8b36e367 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -24,6 +24,7 @@ object Chalice {
     var defaults = 0

     var autoFold = false

     var autoMagic = false

+    var skipDeadlockChecks = false

     var boogieArgs = " ";

     var gen = false;

 

@@ -32,6 +33,7 @@ object Chalice {
       else if (a == "-noTranslate") doTranslate = false

       else if (a == "-noTypecheck") doTypecheck = false

       else if (a == "-checkLeaks") checkLeaks = true

+      else if (a == "-noDeadlockChecks") skipDeadlockChecks = true

       else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)

       else if (a == "-defaults") defaults = 3

       else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument"); } }

@@ -83,6 +85,7 @@ object Chalice {
                 TranslationOptions.defaults = defaults;

                 TranslationOptions.autoFold = autoFold;

                 TranslationOptions.autoMagic = autoMagic;

+                TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;

                 val bplProg = translator.translateProgram(prog);

                 // write to out.bpl

                 val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };

@@ -110,6 +113,6 @@ object Chalice {
 

   def CommandLineError(msg: String) = {

     Console.err.println("Error: " + msg)

-    Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] inputFile")

+    Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")

   }

 }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 95f46dc3..50ffca51 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -19,6 +19,7 @@ object TranslationOptions {
   var autoFold = false: Boolean;

   var checkLeaks = false: Boolean;

   var autoMagic = false: Boolean;

+  var skipDeadlockChecks = false: Boolean;

 }

 

 class Translator {

@@ -713,8 +714,12 @@ class Translator {
     val (lastAcquireVar, lastAcquire) = Boogie.NewBVar("lastAcquire", Boogie.ClassType(IntClass), true)

     val (lastSeenHeldV, lastSeenHeld) = Boogie.NewBVar("lastSeenHeld", tint, true)

     val (lastSeenMuV, lastSeenMu) = Boogie.NewBVar("lastSeenMu", tmu, true)

-    bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the acquire statement might not be readable.") ::

-    bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above maxlock.") ::

+    (if (skipDeadlockChecks)

+       bassume(CanRead(o, "mu")) ::

+       bassume(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")))

+     else

+       bassert(CanRead(o, "mu"), s.pos, "The mu field of the target of the acquire statement might not be readable.") ::

+       bassert(etran.MaxLockIsBelowX(etran.Heap.select(o,"mu")), s.pos, "The mu field of the target of the acquire statement might not be above maxlock.")) :::

     bassume(etran.Heap.select(o,"mu") !=@ bLockBottom) ::  // this isn't strictly necessary, it seems; but we might as well include it

     // remember the state right before releasing

     BLocal(lastSeenMuV) :: (lastSeenMu := etran.Heap.select(o, "mu")) ::