Merge pull request #139 from septract/bjs-cav

Shared symbols can take thread-locals, and other environment fixes

Examples/Errors/local_in_shared_context.cvf

@@ -0,0 +1,47 @@
+/*
+ * Linux-style ticket lock.
+ */
+
+shared int ticket;  // The next ticket to hand out.
+shared int serving; // The current ticket holding the lock.
+thread int t;  // The thread's current ticket.
+thread int s;  // The thread's current view of serving.
+
+/*
+ * Locks the ticket lock.
+ */
+method lock() {
+  {| emp |}
+    <t = s++>; // <-- Thread-local in shared context
+  {| holdTick(t) |}
+    do {
+      {| holdTick(t) |}
+        <s = serving>;
+      {| if s == t then holdLock() else holdTick(t) |}
+    } while (s != t);
+  {| holdLock() |}
+}
+
+/*
+ * Unlocks the ticket lock.
+ */
+method unlock() {
+  {| holdLock() |}
+    <serving++>;
+  {| emp |}
+}
+
+view holdTick(int t);
+view holdLock();
+
+// Invariant
+constraint emp                         -> ticket >= serving;
+
+// Predicate definitions
+constraint holdTick(t)                 -> ticket > t;
+constraint holdLock()                  -> ticket != serving;
+
+// Interactions
+constraint holdLock()   * holdTick(t)  -> serving != t;
+constraint holdTick(ta) * holdTick(tb) -> ta != tb;
+constraint holdLock()   * holdLock()   -> false;

Examples/Errors/shared_in_local_context.cvf

@@ -0,0 +1,47 @@
+/*
+ * Linux-style ticket lock.
+ */
+
+shared int ticket;  // The next ticket to hand out.
+shared int serving; // The current ticket holding the lock.
+thread int t;  // The thread's current ticket.
+thread int s;  // The thread's current view of serving.
+
+/*
+ * Locks the ticket lock.
+ */
+method lock() {
+  {| emp |}
+    <ticket = ticket++>; // <-- shared in local context
+  {| holdTick(t) |}
+    do {
+      {| holdTick(t) |}
+        <s = serving>;
+      {| if s == t then holdLock() else holdTick(t) |}
+    } while (s != t);
+  {| holdLock() |}
+}
+
+/*
+ * Unlocks the ticket lock.
+ */
+method unlock() {
+  {| holdLock() |}
+    <serving++>;
+  {| emp |}
+}
+
+view holdTick(int t);
+view holdLock();
+
+// Invariant
+constraint emp                         -> ticket >= serving;
+
+// Predicate definitions
+constraint holdTick(t)                 -> ticket > t;
+constraint holdLock()                  -> ticket != serving;
+
+// Interactions
+constraint holdLock()   * holdTick(t)  -> serving != t;
+constraint holdTick(ta) * holdTick(tb) -> ta != tb;
+constraint holdLock()   * holdLock()   -> false;

Examples/PassGH/arc.cvf

@@ -19,9 +19,8 @@ thread Int c, pval;
 
 method init() {
   {| emp |}
-    // TODO: broken local command syntax.
-    ret = %{new ArcNode};
-    <%{[|ret|].count := 1}>;
+    <{ ret = %{new ArcNode};
+       %{[|ret|].count := 1}; }>;
   {| arc(ret) |}
 }
 
@@ -33,16 +32,14 @@ method clone(ArcNode x) {
 
 method print(ArcNode x) {
   {| arc(x) |}
-    // TODO: broken local command syntax.
-    pval = %{ [|x|].val };
+    <pval = %{ [|x|].val }>;
   {| arc(x) |}
 }
 
 method drop(ArcNode x) {
   {| arc(x) |}
-    // TODO: broken local command syntax.
-    c = %{ [|x|].count };
-    <%{ [|x|].count := [|x|].count - 1 }>;
+    <{ c = %{ [|x|].count };
+       %{ [|x|].count := [|x|].count - 1 }; }>;
   {| countCopy(x, c) |}
     if (c == 1) {
       {| countCopy(x, 1) |}

Examples/PassGH/clhLock.cvf

@@ -23,7 +23,7 @@ method lock(Node mynode) {
   {| queued(mynode, mypred) |}
     do {
       {| queued(mynode, mypred) |}
-        test = %{ [|mypred|].lock };
+        <test = %{ [|mypred|].lock }>;
       {| if test then queued(mynode, mypred) else holdLock(mynode, mypred) |}
     } while (test);
   {| holdLock(mynode, mypred) |}

Examples/PassGH/lclist.cvf

@@ -21,11 +21,11 @@ method deleteVal(int v) {
   {| wf(v) * isHead(prev) |}
    <{ %{ waitLock([|prev|]); takeLock([|prev|]) }; }>;
   {| wf(v) * has1LockAnon(prev) * isHead(prev) |}
-   curr = %{ [|prev|].next };
+   < curr = %{ [|prev|].next } >;
   {| wf(v) * has1Lock(prev, curr) * isHead(prev) |}
    <{ %{ waitLock([|curr|]); takeLock([|curr|]) }; }>;
   {| wf(v) * has2Lock(prev, curr) |}
-   cv = %{ [|curr|].val };
+   < cv = %{ [|curr|].val } >;
   {| wf(v) * has2Lock(prev,curr) * isVal(curr, cv) |}
     while (cv < v ) {
       {| wf(v) * wf(cv) * has2Lock(prev, curr) * isVal(curr, cv) |}

Examples/PassGH/spinLock.cvf

@@ -13,7 +13,7 @@ view newLock(Lock x), holdLock(Lock x), isLock(Lock x);
 
 method newLock() {
   {| emp |}
-    ret = %{new Lock};
+    <ret = %{new Lock}>;
   {| newLock(ret) |}
     <%{[|ret|].lock := false}>;
   {| isLock(ret) |}
@@ -25,7 +25,7 @@ method lock(Lock x) {
       {| isLock(x) |}
         test = false;
       {| if test == false then isLock(x) else False() |}
-        test = %{ CAS_to_true([|x|]) };
+        <test = %{ CAS_to_true([|x|]) }>;
       {| if test == false then isLock(x) else holdLock(x) |}
     } while (test == false);
   {| holdLock(x) |}

Examples/PassGH/ticketLock.cvf

@@ -13,20 +13,20 @@ view newLock(Lock x), holdTick(Lock x, int t), holdLock(Lock x), isLock(Lock x);
 
 method newLock() {
   {| emp |}
-    ret = %{new Lock};
+    <ret = %{new Lock}>;
   {| newLock(ret) |} 
     <%{[|ret|].ticket := 0; [|ret|].serving := 0}>;
   {| isLock(ret) |}
 }
 
 method lock(Lock x) {
   {| isLock(x) |}
-    t = %{ [|x|].ticket };
-    <%{ [|x|].ticket := [|x|].ticket + 1 }>;
+    <{ t = %{ [|x|].ticket };
+       %{ [|x|].ticket := [|x|].ticket + 1 }; }>;
   {| holdTick(x, t) |}
     do {
       {| holdTick(x, t) |}
-        s = %{ [|x|].serving };
+        <s = %{ [|x|].serving }>;
       {| if s == t then holdLock(x) else holdTick(x, t) |}
     } while (s != t);
   {| holdLock(x) |}