Simplify atomic syntax.

Instead of having two atomic syntaxes: ``` <x = y++>; // single atomic action <{ x = y; y = y + 1; }>; // multiple atomic actions ``` We now have a single syntax: ``` <| x = y++; |> // single atomic action <| x = y; y = y + 1; |> // multiple atomic actions ``` Note that the new syntax behaves exactly like a block: it requires semicolons to terminate inner actions, but has no semicolon at the end. This is in preparation for making atomic syntax richer.
septract · Feb 13, 2017 · 6f99ae3 · 6f99ae3
1 parent cc137e1
commit 6f99ae3
Show file tree

Hide file tree

Showing 34 changed files with 203 additions and 206 deletions.
diff --git a/Examples/Errors/local_in_shared_context.cvf b/Examples/Errors/local_in_shared_context.cvf
@@ -12,11 +12,11 @@ thread int s;  // The thread's current view of serving.
  */
 method lock() {
   {| emp |}
-    <t = s++>; // <-- Thread-local in shared context
+    <| t = s++; |> // <-- Thread-local in shared context
   {| holdTick(t) |}
     do {
       {| holdTick(t) |}
-        <s = serving>;
+        <| s = serving; |>
       {| if s == t then holdLock() else holdTick(t) |}
     } while (s != t);
   {| holdLock() |}
@@ -27,7 +27,7 @@ method lock() {
  */
 method unlock() {
   {| holdLock() |}
-    <serving++>;
+    <| serving++; |>
   {| emp |}
 }
 

diff --git a/Examples/Errors/shared_in_local_context.cvf b/Examples/Errors/shared_in_local_context.cvf
@@ -12,11 +12,11 @@ thread int s;  // The thread's current view of serving.
  */
 method lock() {
   {| emp |}
-    <ticket = ticket++>; // <-- shared in local context
+    <| ticket = ticket++; |> // <-- shared in local context
   {| holdTick(t) |}
     do {
       {| holdTick(t) |}
-        <s = serving>;
+        <| s = serving; |>
       {| if s == t then holdLock() else holdTick(t) |}
     } while (s != t);
   {| holdLock() |}
@@ -27,7 +27,7 @@ method lock() {
  */
 method unlock() {
   {| holdLock() |}
-    <serving++>;
+    <| serving++; |>
   {| emp |}
 }
 

diff --git a/Examples/Fail/petersonArrayBadTurns.cvf b/Examples/Fail/petersonArrayBadTurns.cvf
@@ -27,15 +27,15 @@ view holdLock(int me);  // 'me' holds the lock.
  */
 method lock() {
   {| flagDown(i) |}
-    <flag[i] = true>;
+    <| flag[i] = true; |>
   {| flagUp(i) |}
-    <turn = (i + 1) % 2>; // oops!
+    <| turn = (i + 1) % 2; |> // oops!
   {| waiting(i) |}
     do {
       {| waiting(i) |}
-        <oFlag = flag[(i + 1) % 2]>;
+        <| oFlag = flag[(i + 1) % 2]; |>
       {| if (oFlag) then waiting(i) else holdLock(i) |}
-        <oTurn = turn>;
+        <| oTurn = turn; |>
       {| if (oFlag && oTurn == i) then waiting(i) else holdLock(i) |}
     } while (oFlag && (oTurn == i));
   {| holdLock(i) |}
@@ -46,7 +46,7 @@ method lock() {
  */
 method unlock() {
   {| holdLock(i) |}
-    <flag[i] = false>;
+    <| flag[i] = false; |>
   {| flagDown(i) |}
 }
 

diff --git a/Examples/Fail/petersonBadTurns.cvf b/Examples/Fail/petersonBadTurns.cvf
@@ -30,15 +30,15 @@ view bHoldLock();       // B holds the lock.
  */
 method lockA() {
   {| aFlagDown() |}
-    <aFlag = (true)>;
+    <| aFlag = (true); |>
   {| aFlagUp() |}
-    <turn = 2>;  // oops!
+    <| turn = 2; |>  // oops!
   {| aWaiting() |}
     do {
       {| aWaiting() |}
-        <oFlag = bFlag>;
+        <| oFlag = bFlag; |>
       {| if (oFlag) then aWaiting() else aHoldLock() |}
-        <oTurn = turn>;
+        <| oTurn = turn; |>
       {| if (oFlag && oTurn == 1) then aWaiting() else aHoldLock() |}
     } while (oFlag && (oTurn == 1));
   {| aHoldLock() |}
@@ -49,7 +49,7 @@ method lockA() {
  */
 method unlockA() {
   {| aHoldLock() |}
-    <aFlag = (false)>;
+    <| aFlag = (false); |>
   {| aFlagDown() |}
 }
 
@@ -58,15 +58,15 @@ method unlockA() {
  */
 method lockB() {
   {| bFlagDown() |}
-    <bFlag = true>;
+    <| bFlag = true; |>
   {| bFlagUp() |}
-    <turn = 1>;  // oops!
+    <| turn = 1; |>  // oops!
   {| bWaiting() |}
     do {
       {| bWaiting() |}
-        <oFlag = aFlag>;
+        <| oFlag = aFlag; |>
       {| if (oFlag) then bWaiting() else bHoldLock() |}
-        <oTurn = turn>;
+        <| oTurn = turn; |>
       {| if (oFlag && oTurn == 2) then bWaiting() else bHoldLock() |}
     } while (oFlag && (oTurn == 2));
   {| bHoldLock() |}
@@ -77,7 +77,7 @@ method lockB() {
  */
 method unlockB() {
   {| bHoldLock() |}
-    <bFlag = false>;
+    <| bFlag = false; |>
   {| bFlagDown() |}
 }
 

diff --git a/Examples/Fail/ticketLockBad.cvf b/Examples/Fail/ticketLockBad.cvf
@@ -12,11 +12,11 @@ thread int s;  // The thread's current view of serving.
  */
 method lock() {
   {| emp |}
-    <t = ticket++>;
+    <| t = ticket++; |>
   {| holdTick(t) |}
     do {
       {| holdTick(t) |}
-        <s = serving>;
+        <| s = serving; |>
       {| if s == t then holdLock() else holdTick(t) |}
     } while (s != t);
   {| holdLock() |}
@@ -27,7 +27,7 @@ method lock() {
  */
 method unlock() {
   {| holdLock() |}
-    <serving++>;
+    <| serving++; |>
   {| emp |}
 }
 

diff --git a/Examples/Fail/ticketLockBad2.cvf b/Examples/Fail/ticketLockBad2.cvf
@@ -12,11 +12,11 @@ thread int s;  // The thread's current view of serving.
  */
 method lock() {
   {| emp |}
-    <t = ticket++>;
+    <| t = ticket++; |>
   {| holdTick(t) |}
     do {
       {| holdTick(t) |}
-        <s = serving>;
+        <| s = serving; |>
       {| if s == t then holdLock() else holdTick(t) |}
     } while (s != t);
   {| holdLock() |}
@@ -27,7 +27,7 @@ method lock() {
  */
 method unlock() {
   {| holdLock() |}
-    <serving++>;
+    <| serving++; |>
   {| emp |}
 }
 

diff --git a/Examples/Fail/ticketLockFlippedLoop.cvf b/Examples/Fail/ticketLockFlippedLoop.cvf
@@ -12,11 +12,11 @@ thread int s;  // The thread's current view of serving.
  */
 method lock() {
   {| emp |}
-    <t = ticket++>;
+    <| t = ticket++; |>
   {| holdTick(t) |}
     do {
       {| holdTick(t) |}
-        <s = serving>;
+        <| s = serving; |>
       {| if s == t then holdLock() else holdTick(t) |}
     } while (s == t);
   {| holdLock() |}
@@ -27,7 +27,7 @@ method lock() {
  */
 method unlock() {
   {| holdLock() |}
-    <serving++>;
+    <| serving++; |>
   {| emp |}
 }
 

diff --git a/Examples/FailGH/ticketLockFlippedIf.cvf b/Examples/FailGH/ticketLockFlippedIf.cvf
@@ -21,14 +21,14 @@ method newLock() {
   {| emp |}
     ret = %{new Lock};
   {| newLock(ret) |} 
-    <%{[|ret|].ticket := 0; [|ret|].serving := 0}>;
+    <| %{[|ret|].ticket := 0; [|ret|].serving := 0}; |>
   {| isLock(ret) |}
 }
 
 method lock(Lock x) {
   {| isLock(x) |}
     t = %{ [|x|].ticket };
-    <%{ [|x|].ticket := [|x|].ticket + 1 }>;
+    <| %{ [|x|].ticket := [|x|].ticket + 1 }; |>
   {| holdTick(x, t) |}
     do {
       {| holdTick(x, t) |}
@@ -40,7 +40,7 @@ method lock(Lock x) {
 
 method unlock(Lock x) {
   {| holdLock(x) |}
-    <%{[|x|].serving := [|x|].serving + 1}>;
+    <| %{[|x|].serving := [|x|].serving + 1}; |>
   {| isLock(x) |}
 }
 

diff --git a/Examples/Pass/arc.cvf b/Examples/Pass/arc.cvf
@@ -10,14 +10,14 @@ thread int c;
 
 // Assumption: clone() cannot be called when there are no references
 method clone() {
-  {| arc() |} < count++ >; {| arc() * arc() |}
+  {| arc() |} <| count++; |> {| arc() * arc() |}
 }
 
 // Try to prove that print() when holding a reference is always valid
 // i.e. free can never be true when {| arc() |} is held
 method print() {
   {| arc() |}
-    <f = free>;
+    <| f = free; |>
   {| arc() * specialViewForFree(f) |}
     // Test for disposal
     if (f == true) {
@@ -28,11 +28,11 @@ method print() {
 
 method drop() {
   {| arc() |}
-    < c = count-- >;
+    <| c = count--; |>
   {| specialViewForC(c) |}
     if (c == 1) {
       {| noCnt() |}
-        <free = (true)>;
+        <| free = true; |>
       {| emp |}
     }
   {| emp |}

diff --git a/Examples/Pass/arc2.cvf b/Examples/Pass/arc2.cvf
@@ -17,39 +17,39 @@ view error();
 constraint error() -> false;
 
 method clone() {
-  {| arc() |} 
-    < count++ >; 
+  {| arc() |}
+    <| count++ ; |>
   {| arc() * arc() |}
 }
 
 method print() {
   {| arc() |}
-    <f = free>;
+    <| f = free; |>
   {| if f == true then error() else arc() |}
     if (f == true) {
-      {| error() |} 
+      {| error() |}
     }
   {| arc() |}
 }
 
 method drop() {
   {| arc() |}
-    < c = count-- >;
+    <| c = count--; |>
   {| countCopy(c) |}
     if (c == 1) {
       {| countCopy(1) |}
-        <free = (true)>;
+        <| free = true; |>
       {| emp |}
     }
   {| emp |}
 }
 
-constraint iter[n] arc() -> 
+constraint iter[n] arc() ->
     n > 0 => (free == false && n <= count);
 
-constraint countCopy(c) ->  
+constraint countCopy(c) ->
     c == 1 => (free == false && count == 0);
 
-constraint countCopy(m) * countCopy(n) -> 
-    (m != 1) || (n != 1);  
+constraint countCopy(m) * countCopy(n) ->
+    (m != 1) || (n != 1);
 
diff --git a/Examples/Pass/multicounter.cvf b/Examples/Pass/multicounter.cvf
@@ -13,7 +13,7 @@ method multiIncrement() {
     {| count(t) |}
        t=t+1;
     {| count(t-1) |}
-       <counter++>; 
+       <| counter++; |>
     {| count(t) |}
   } while (t != 10);
   {| count(10) |}

diff --git a/Examples/Pass/peterson.cvf b/Examples/Pass/peterson.cvf
@@ -36,15 +36,15 @@ view bHoldLock();       // B holds the lock.
  */
 method lockA() {
   {| aFlagDown() |}
-    <aFlag = true>;
+    <| aFlag = true; |>
   {| aFlagUp() |}
-    <turn = 1>;
+    <| turn = 1; |>
   {| aWaiting() |}
     do {
       {| aWaiting() |}
-        <oFlag = bFlag>;
+        <| oFlag = bFlag; |>
       {| if (oFlag) then aWaiting() else aHoldLock() |}
-        <oTurn = turn>;
+        <| oTurn = turn; |>
       {| if (oFlag && oTurn == 1) then aWaiting() else aHoldLock() |}
     } while (oFlag && (oTurn == 1));
   {| aHoldLock() |}
@@ -55,7 +55,7 @@ method lockA() {
  */
 method unlockA() {
   {| aHoldLock() |}
-    <aFlag = false>;
+    <| aFlag = false; |>
   {| aFlagDown() |}
 }
 
@@ -64,15 +64,15 @@ method unlockA() {
  */
 method lockB() {
   {| bFlagDown() |}
-    <bFlag = true>;
+    <| bFlag = true; |>
   {| bFlagUp() |}
-    <turn = 2>;
+    <| turn = 2; |>
   {| bWaiting() |}
     do {
       {| bWaiting() |}
-        <oFlag = aFlag>;
+        <| oFlag = aFlag; |>
       {| if (oFlag) then bWaiting() else bHoldLock() |}
-        <oTurn = turn>;
+        <| oTurn = turn; |>
       {| if (oFlag && oTurn == 2) then bWaiting() else bHoldLock() |}
     } while (oFlag && (oTurn == 2));
   {| bHoldLock() |}
@@ -83,7 +83,7 @@ method lockB() {
  */
 method unlockB() {
   {| bHoldLock() |}
-    <bFlag = false>;
+    <| bFlag = false; |>
   {| bFlagDown() |}
 }