From 6f99ae30743346ca2106c0aceaea8d3359ce20a1 Mon Sep 17 00:00:00 2001 From: Matt Windsor Date: Mon, 13 Feb 2017 12:19:47 +0000 Subject: [PATCH] Simplify atomic syntax. Instead of having two atomic syntaxes: ``` ; // 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. --- Examples/Errors/local_in_shared_context.cvf | 6 +-- Examples/Errors/shared_in_local_context.cvf | 6 +-- Examples/Fail/petersonArrayBadTurns.cvf | 10 ++--- Examples/Fail/petersonBadTurns.cvf | 20 ++++----- Examples/Fail/ticketLockBad.cvf | 6 +-- Examples/Fail/ticketLockBad2.cvf | 6 +-- Examples/Fail/ticketLockFlippedLoop.cvf | 6 +-- Examples/FailGH/ticketLockFlippedIf.cvf | 6 +-- Examples/Pass/arc.cvf | 8 ++-- Examples/Pass/arc2.cvf | 20 ++++----- Examples/Pass/multicounter.cvf | 2 +- Examples/Pass/peterson.cvf | 20 ++++----- Examples/Pass/petersonArray.cvf | 10 ++--- Examples/Pass/petersonInt.cvf | 20 ++++----- .../Pass/petersonIntMissingSynthesised.cvf | 20 ++++----- Examples/Pass/petersonMultiCmd.cvf | 16 +++---- Examples/Pass/seqCmd.cvf | 24 +++++----- Examples/Pass/singleWriterMultiReaderLock.cvf | 20 ++++----- Examples/Pass/spinLock.cvf | 4 +- Examples/Pass/spinLockAdvisory.cvf | 4 +- Examples/Pass/spinLockInt.cvf | 4 +- Examples/Pass/spinLockMultiCmd.cvf | 4 +- Examples/Pass/ticketLock.cvf | 6 +-- Examples/Pass/ticketLockNoIf.cvf | 6 +-- Examples/Pass/ticketLockNoInvariant.cvf | 6 +-- Examples/Pass/ticketLockNonAtomicRelease.cvf | 8 ++-- Examples/Pass/ticketLockNonAtomicRelease2.cvf | 10 ++--- Examples/PassGH/arc.cvf | 18 ++++---- Examples/PassGH/clhLock.cvf | 12 ++--- Examples/PassGH/lclist.cvf | 22 +++++----- Examples/PassGH/spinLock.cvf | 8 ++-- Examples/PassGH/ticketLock.cvf | 12 ++--- Parser.fs | 44 +++++++++++-------- ParserTests.fs | 15 +------ 34 files changed, 203 insertions(+), 206 deletions(-) diff --git a/Examples/Errors/local_in_shared_context.cvf b/Examples/Errors/local_in_shared_context.cvf index dc5d13e..ddfc2a2 100644 --- 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 |} - ; // <-- Thread-local in shared context + <| 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() |} @@ -27,7 +27,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Errors/shared_in_local_context.cvf b/Examples/Errors/shared_in_local_context.cvf index 2ce9018..94e7959 100644 --- 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 |} - ; // <-- shared in local context + <| 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() |} @@ -27,7 +27,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Fail/petersonArrayBadTurns.cvf b/Examples/Fail/petersonArrayBadTurns.cvf index 8ff8070..0c5ced6 100644 --- 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; |> {| flagUp(i) |} - ; // oops! + <| turn = (i + 1) % 2; |> // oops! {| waiting(i) |} do { {| waiting(i) |} - ; + <| oFlag = flag[(i + 1) % 2]; |> {| if (oFlag) then waiting(i) else holdLock(i) |} - ; + <| 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; |> {| flagDown(i) |} } diff --git a/Examples/Fail/petersonBadTurns.cvf b/Examples/Fail/petersonBadTurns.cvf index 3ae35b5..e8d1fe6 100644 --- 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); |> {| aFlagUp() |} - ; // oops! + <| turn = 2; |> // oops! {| aWaiting() |} do { {| aWaiting() |} - ; + <| oFlag = bFlag; |> {| if (oFlag) then aWaiting() else aHoldLock() |} - ; + <| 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); |> {| aFlagDown() |} } @@ -58,15 +58,15 @@ method unlockA() { */ method lockB() { {| bFlagDown() |} - ; + <| bFlag = true; |> {| bFlagUp() |} - ; // oops! + <| turn = 1; |> // oops! {| bWaiting() |} do { {| bWaiting() |} - ; + <| oFlag = aFlag; |> {| if (oFlag) then bWaiting() else bHoldLock() |} - ; + <| 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; |> {| bFlagDown() |} } diff --git a/Examples/Fail/ticketLockBad.cvf b/Examples/Fail/ticketLockBad.cvf index e487ab3..60a6dfb 100644 --- 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++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdLock() else holdTick(t) |} } while (s != t); {| holdLock() |} @@ -27,7 +27,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Fail/ticketLockBad2.cvf b/Examples/Fail/ticketLockBad2.cvf index 7f7cb86..7de3e46 100644 --- 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++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdLock() else holdTick(t) |} } while (s != t); {| holdLock() |} @@ -27,7 +27,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Fail/ticketLockFlippedLoop.cvf b/Examples/Fail/ticketLockFlippedLoop.cvf index add93d2..97b84d2 100644 --- 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++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdLock() else holdTick(t) |} } while (s == t); {| holdLock() |} @@ -27,7 +27,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/FailGH/ticketLockFlippedIf.cvf b/Examples/FailGH/ticketLockFlippedIf.cvf index 86073cc..3702624 100644 --- 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 index 842ac75..8f01dfe 100644 --- 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; |> {| 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; |> {| emp |} } {| emp |} diff --git a/Examples/Pass/arc2.cvf b/Examples/Pass/arc2.cvf index 05c17ea..113057a 100644 --- 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; |> {| 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; |> {| 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 index 2c29648..b5d07c5 100644 --- 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++; |> {| count(t) |} } while (t != 10); {| count(10) |} diff --git a/Examples/Pass/peterson.cvf b/Examples/Pass/peterson.cvf index 71cffe6..cd4d266 100644 --- 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; |> {| aFlagUp() |} - ; + <| turn = 1; |> {| aWaiting() |} do { {| aWaiting() |} - ; + <| oFlag = bFlag; |> {| if (oFlag) then aWaiting() else aHoldLock() |} - ; + <| 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; |> {| aFlagDown() |} } @@ -64,15 +64,15 @@ method unlockA() { */ method lockB() { {| bFlagDown() |} - ; + <| bFlag = true; |> {| bFlagUp() |} - ; + <| turn = 2; |> {| bWaiting() |} do { {| bWaiting() |} - ; + <| oFlag = aFlag; |> {| if (oFlag) then bWaiting() else bHoldLock() |} - ; + <| 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; |> {| bFlagDown() |} } diff --git a/Examples/Pass/petersonArray.cvf b/Examples/Pass/petersonArray.cvf index da1b5ea..6c5dd35 100644 --- a/Examples/Pass/petersonArray.cvf +++ b/Examples/Pass/petersonArray.cvf @@ -26,15 +26,15 @@ view holdLock(int me); // 'me' holds the lock. */ method lock(int i) { {| flagDown(i) |} - ; + <| flag[i] = true; |> {| flagUp(i) |} - ; + <| turn = i; |> {| waiting(i) |} do { {| waiting(i) |} - ; + <| oFlag = flag[(i + 1) % 2]; |> {| if (oFlag) then waiting(i) else holdLock(i) |} - ; + <| oTurn = turn; |> {| if (oFlag && oTurn == i) then waiting(i) else holdLock(i) |} } while (oFlag && (oTurn == i)); {| holdLock(i) |} @@ -45,7 +45,7 @@ method lock(int i) { */ method unlock(int i) { {| holdLock(i) |} - ; + <| flag[i] = false; |> {| flagDown(i) |} } diff --git a/Examples/Pass/petersonInt.cvf b/Examples/Pass/petersonInt.cvf index 10f457e..a04bc72 100644 --- a/Examples/Pass/petersonInt.cvf +++ b/Examples/Pass/petersonInt.cvf @@ -40,15 +40,15 @@ view bHoldLock(); // B holds the lock. */ method lockA() { {| aFlagDown() |} - ; + <| aFlag = 1; |> {| aFlagUp() |} - ; + <| turn = 0; |> {| aWaiting() |} do { {| aWaiting() |} - ; + <| oFlag = bFlag; |> {| if (oFlag == 1) then aWaiting() else aHoldLock() |} - ; + <| oTurn = turn; |> {| if (oFlag == 1 && oTurn == 0) then aWaiting() else aHoldLock() |} } while (oFlag == 1 && oTurn == 0); {| aHoldLock() |} @@ -59,7 +59,7 @@ method lockA() { */ method unlockA() { {| aHoldLock() |} - ; + <| aFlag = 0; |> {| aFlagDown() |} } @@ -68,15 +68,15 @@ method unlockA() { */ method lockB() { {| bFlagDown() |} - ; + <| bFlag = 1; |> {| bFlagUp() |} - ; + <| turn = 1; |> {| bWaiting() |} do { {| bWaiting() |} - ; + <| oFlag = aFlag; |> {| if (oFlag == 1) then bWaiting() else bHoldLock() |} - ; + <| oTurn = turn; |> {| if (oFlag == 1 && oTurn == 1) then bWaiting() else bHoldLock() |} } while (oFlag == 1 && oTurn == 1); {| bHoldLock() |} @@ -87,7 +87,7 @@ method lockB() { */ method unlockB() { {| bHoldLock() |} - ; + <| bFlag = 0; |> {| bFlagDown() |} } diff --git a/Examples/Pass/petersonIntMissingSynthesised.cvf b/Examples/Pass/petersonIntMissingSynthesised.cvf index 2cbcadc..934eb69 100644 --- a/Examples/Pass/petersonIntMissingSynthesised.cvf +++ b/Examples/Pass/petersonIntMissingSynthesised.cvf @@ -49,15 +49,15 @@ view v8(int f, int t); */ method lockA() { {| aFlagDown() |} - ; + <| aFlag = 1; |> {| v0(oFlag, oTurn) |} - ; + <| turn = 0; |> {| v2(oFlag, oTurn) |} do { {| v2(oFlag, oTurn) |} - ; + <| oFlag = bFlag; |> {| v3(oFlag, oTurn) |} - ; + <| oTurn = turn; |> {| if (oFlag == 1 && oTurn == 0) then v2(oFlag, oTurn) else aHoldLock() |} } while (oFlag == 1 && oTurn == 0); {| aHoldLock() |} @@ -68,7 +68,7 @@ method lockA() { */ method unlockA() { {| aHoldLock() |} - ; + <| aFlag = 0; |> {| aFlagDown() |} } @@ -77,15 +77,15 @@ method unlockA() { */ method lockB() { {| bFlagDown() |} - ; + <| bFlag = 1; |> {| v5(oFlag, oTurn) |} - ; + <| turn = 1; |> {| v7(oFlag, oTurn) |} do { {| v7(oFlag, oTurn) |} - ; + <| oFlag = aFlag; |> {| v8(oFlag, oTurn) |} - ; + <| oTurn = turn; |> {| if (oFlag == 1 && oTurn == 1) then v7(oFlag, oTurn) else bHoldLock() |} } while (oFlag == 1 && oTurn == 1); {| bHoldLock() |} @@ -96,7 +96,7 @@ method lockB() { */ method unlockB() { {| bHoldLock() |} - ; + <| bFlag = 0; |> {| bFlagDown() |} } diff --git a/Examples/Pass/petersonMultiCmd.cvf b/Examples/Pass/petersonMultiCmd.cvf index 342d01c..f0676a5 100644 --- a/Examples/Pass/petersonMultiCmd.cvf +++ b/Examples/Pass/petersonMultiCmd.cvf @@ -39,14 +39,14 @@ view bHoldLock(); // B holds the lock. */ method lockA() { {| aFlagDown() |} - ; + <| aFlag = true; |> {| aFlagUp() |} - ; + <| turn = 1; |> {| aWaiting() |} do { {| aWaiting() |} // This is _one_ atomic action - <{oFlag = bFlag; oTurn = turn; }>; + <| oFlag = bFlag; oTurn = turn; |> {| if (oFlag && oTurn == 1) then aWaiting() else aHoldLock() |} } while (oFlag && (oTurn == 1)); {| aHoldLock() |} @@ -57,7 +57,7 @@ method lockA() { */ method unlockA() { {| aHoldLock() |} - ; + <| aFlag = false; |> {| aFlagDown() |} } @@ -66,13 +66,13 @@ method unlockA() { */ method lockB() { {| bFlagDown() |} - ; + <| bFlag = true; |> {| bFlagUp() |} - ; + <| turn = 2; |> {| bWaiting() |} do { {| bWaiting() |} - <{ oFlag = aFlag; oTurn = turn; }>; + <| oFlag = aFlag; 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; |> {| bFlagDown() |} } diff --git a/Examples/Pass/seqCmd.cvf b/Examples/Pass/seqCmd.cvf index e618cd0..06e4da9 100644 --- a/Examples/Pass/seqCmd.cvf +++ b/Examples/Pass/seqCmd.cvf @@ -1,23 +1,23 @@ -// test variable +// test variable shared int test; // Junk variables -shared int foo; -shared int bar; +shared int foo; +shared int bar; -view isZero(); -view isThree(); +view isZero(); +view isThree(); method addThree() { {| isZero() |} - <{ test++; - test++; - test++; }>; + <| test++; + test++; + test++; |> {| isThree() |} } -constraint isZero() -> test==0; -constraint isThree() -> test==3; +constraint isZero() -> test==0; +constraint isThree() -> test==3; -// No-one else is relying on test staying zero -constraint isZero() * isZero() -> false; +// No-one else is relying on test staying zero +constraint isZero() * isZero() -> false; diff --git a/Examples/Pass/singleWriterMultiReaderLock.cvf b/Examples/Pass/singleWriterMultiReaderLock.cvf index f5bb38f..fe5b078 100644 --- a/Examples/Pass/singleWriterMultiReaderLock.cvf +++ b/Examples/Pass/singleWriterMultiReaderLock.cvf @@ -16,11 +16,11 @@ thread int m; // Hack used to make maxCount thread-local. method readAcquire() { {| emp |} - ; + <| t = ticket++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdInnerLock() else holdTick(t) |} } while (s != t); {| holdInnerLock() |} @@ -28,31 +28,31 @@ method readAcquire() { // Diverge if there are too many readers. // TODO: rescind the inner lock before spinning? {| holdInnerLock() |} - <{r = readCount; m = maxCount;}>; + <| r = readCount; m = maxCount; |> {| if r > (m - 1) then holdInnerLock() else canHoldReadLock() |} } while (r > (m - 1)); {| canHoldReadLock() |} - ; + <| readCount++; |> {| holdInnerLock() * holdReadLock() |} - ; + <| serving++; |> {| holdReadLock() |} } method readRelease() { {| holdReadLock() |} - ; + <| readCount--; |> {| emp |} } method writeAcquire() { {| emp |} - ; + <| t = ticket++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdInnerLock() else holdTick(t) |} } while (s != t); {| holdInnerLock() |} @@ -60,7 +60,7 @@ method writeAcquire() { // Diverge if there are any readers. // TODO: rescind the inner lock before spinning? {| holdInnerLock() |} - ; + <| r = readCount; |> {| if r == 0 then holdWriteLock() else holdInnerLock() |} } while (r != 0); {| holdWriteLock() |} @@ -72,7 +72,7 @@ method writeAcquire() { */ method writeRelease() { {| holdWriteLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Pass/spinLock.cvf b/Examples/Pass/spinLock.cvf index 16c7d14..f33dc65 100644 --- a/Examples/Pass/spinLock.cvf +++ b/Examples/Pass/spinLock.cvf @@ -14,7 +14,7 @@ method lock() { {| emp |} test = false; {| if test == false then emp else False() |} - ; + <| CAS(lock, test, true); |> {| if test == false then holdLock() else emp |} } while (test == true); {| holdLock() |} @@ -25,7 +25,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| lock = false; |> {| emp |} } diff --git a/Examples/Pass/spinLockAdvisory.cvf b/Examples/Pass/spinLockAdvisory.cvf index a98cbe7..93282fa 100644 --- a/Examples/Pass/spinLockAdvisory.cvf +++ b/Examples/Pass/spinLockAdvisory.cvf @@ -14,7 +14,7 @@ method lock() { {| emp |} test = false; {| if test == false then emp else False() ? |} - ; + <| CAS(lock, test, true); |> {| if test == false then holdLock() else emp |} } while (test == true); {| holdLock() |} @@ -25,7 +25,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| lock = false; |> {| emp |} } diff --git a/Examples/Pass/spinLockInt.cvf b/Examples/Pass/spinLockInt.cvf index 734a9aa..bd270d0 100644 --- a/Examples/Pass/spinLockInt.cvf +++ b/Examples/Pass/spinLockInt.cvf @@ -15,7 +15,7 @@ method lock() { {| emp |} test = 0; {| if test == 0 then emp else False() |} - ; + <| CAS(lock, test, 1); |> // Starling can't infer that test is always 0 or 1. // Thus, we need to flip the condition here. {| if test == 1 then emp else holdLock() |} @@ -28,7 +28,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| lock = 0; |> {| emp |} } diff --git a/Examples/Pass/spinLockMultiCmd.cvf b/Examples/Pass/spinLockMultiCmd.cvf index ec66452..bb51c1b 100644 --- a/Examples/Pass/spinLockMultiCmd.cvf +++ b/Examples/Pass/spinLockMultiCmd.cvf @@ -14,7 +14,7 @@ method lock() { do { {| emp |} test = false; - ; + <| CAS(lock, test, true); |> {| if test == false then holdLock() else emp |} } while (test == true); {| holdLock() |} @@ -25,7 +25,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| lock = false; |> {| emp |} } diff --git a/Examples/Pass/ticketLock.cvf b/Examples/Pass/ticketLock.cvf index e85264f..3ab25a7 100644 --- a/Examples/Pass/ticketLock.cvf +++ b/Examples/Pass/ticketLock.cvf @@ -12,11 +12,11 @@ thread int s; // The thread's current view of serving. */ method lock() { {| emp |} - ; + <| t = ticket++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdLock() else holdTick(t) |} } while (s != t); {| holdLock() |} @@ -27,7 +27,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Pass/ticketLockNoIf.cvf b/Examples/Pass/ticketLockNoIf.cvf index b1ed002..21f1dfe 100644 --- a/Examples/Pass/ticketLockNoIf.cvf +++ b/Examples/Pass/ticketLockNoIf.cvf @@ -12,11 +12,11 @@ thread int s; // The thread's current view of serving. */ method lock() { {| emp |} - ; + <| t = ticket++; |> {| holdTickLock(t, false) |} do { {| holdTickLock(t, false) |} - ; + <| s = serving; |> {| holdTickLock(t, s == t) |} } while (s != t); {| holdTickLock(t, true) |} @@ -27,7 +27,7 @@ method lock() { */ method unlock() { {| holdTickLock(t, true) |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Pass/ticketLockNoInvariant.cvf b/Examples/Pass/ticketLockNoInvariant.cvf index 4f16802..27b185c 100644 --- a/Examples/Pass/ticketLockNoInvariant.cvf +++ b/Examples/Pass/ticketLockNoInvariant.cvf @@ -14,11 +14,11 @@ thread int s; // The thread's current view of serving. */ method lock() { {| emp |} - ; + <| t = ticket++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdLock() else holdTick(t) |} } while (s != t); {| holdLock() |} @@ -29,7 +29,7 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| serving++; |> {| emp |} } diff --git a/Examples/Pass/ticketLockNonAtomicRelease.cvf b/Examples/Pass/ticketLockNonAtomicRelease.cvf index 8a6c556..9aef687 100644 --- a/Examples/Pass/ticketLockNonAtomicRelease.cvf +++ b/Examples/Pass/ticketLockNonAtomicRelease.cvf @@ -12,11 +12,11 @@ thread int s; // The thread's current view of serving. */ method lock() { {| emp |} - ; + <| t = ticket++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdLock() else holdTick(t) |} } while (s != t); {| holdLock() |} @@ -27,9 +27,9 @@ method lock() { */ method unlock() { {| holdLock() |} - ; + <| s = serving; |> {| relLock(s) |} - ; + <| serving = s + 1; |> {| emp |} } diff --git a/Examples/Pass/ticketLockNonAtomicRelease2.cvf b/Examples/Pass/ticketLockNonAtomicRelease2.cvf index 762b0e5..c764f12 100644 --- a/Examples/Pass/ticketLockNonAtomicRelease2.cvf +++ b/Examples/Pass/ticketLockNonAtomicRelease2.cvf @@ -12,11 +12,11 @@ thread int s; // The thread's current view of serving. */ method lock() { {| emp |} - ; + <| t = ticket++; |> {| holdTick(t) |} do { {| holdTick(t) |} - ; + <| s = serving; |> {| if s == t then holdLock() else holdTick(t) |} } while (s != t); {| holdLock() |} @@ -27,9 +27,9 @@ method lock() { */ method unlock() { {| holdLock() |} - ; - {| /*relLock(s)*/ holdLock() |} - ; + <| s = serving; |> + {| holdLock() |} + <| serving = s + 1; |> {| emp |} } diff --git a/Examples/PassGH/arc.cvf b/Examples/PassGH/arc.cvf index b7b6eb0..b4f7d9f 100644 --- a/Examples/PassGH/arc.cvf +++ b/Examples/PassGH/arc.cvf @@ -19,41 +19,41 @@ thread Int c, pval; method init() { {| emp |} - <{ ret = %{new ArcNode}; - %{[|ret|].count := 1}; }>; + <| ret = %{ new ArcNode }; + %{ [|ret|].count := 1 }; |> {| arc(ret) |} } method clone(ArcNode x) { {| arc(x) |} - <%{[|x|].count := [|x|].count + 1}>; + <| %{ [|x|].count := [|x|].count + 1 }; |> {| arc(x) * arc(x) |} } method print(ArcNode x) { {| arc(x) |} - ; + <| pval = %{ [|x|].val }; |> {| arc(x) |} } method drop(ArcNode x) { {| arc(x) |} - <{ 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) |} - < %{ free([|x|]) } >; + <| %{ free([|x|]) }; |> {| emp |} } {| emp |} } constraint iter[n] arc(x) -> - n > 0 => %{ [|x|] in ArcFoot && [|n|] <= [|x|].count}; + n > 0 => %{ [|x|] in ArcFoot && [|n|] <= [|x|].count }; constraint countCopy(x, c) -> - c == 1 => %{ [|x|] in ArcFoot && [|x|].count == 0}; + c == 1 => %{ [|x|] in ArcFoot && [|x|].count == 0 }; constraint countCopy(x, m) * countCopy(y, n) -> x == y => ((m != 1) || (n != 1)); diff --git a/Examples/PassGH/clhLock.cvf b/Examples/PassGH/clhLock.cvf index aa55048..0d7574a 100644 --- a/Examples/PassGH/clhLock.cvf +++ b/Examples/PassGH/clhLock.cvf @@ -15,15 +15,15 @@ view holdLock(Node x, Node xp); method lock(Node mynode) { {| loose(mynode, false) |} - < %{ [|mynode|].lock := true } >; + <| %{ [|mynode|].lock := true }; |> {| loose(mynode, true) |} - <{ mypred = tail; + <| mypred = tail; tail = mynode; - %{[|tail|].pred := [|mypred|]}; }>; // Ghost code + %{[|tail|].pred := [|mypred|]}; |> // Ghost code {| queued(mynode, mypred) |} do { {| queued(mynode, mypred) |} - ; + <| test = %{ [|mypred|].lock }; |> {| if test then queued(mynode, mypred) else holdLock(mynode, mypred) |} } while (test); {| holdLock(mynode, mypred) |} @@ -31,10 +31,10 @@ method lock(Node mynode) { method unlock(Node mynode, Node mypred) { {| holdLock(mynode, mypred) |} - <{ %{ [|mynode|].lock := false }; + <| %{ [|mynode|].lock := false }; %{ [|mynode|].pred := null }; // Ghost code head = mynode; // Ghost code - }>; + |> {| loose(mypred, false) |} mynode = mypred; {| loose(mynode, false) |} diff --git a/Examples/PassGH/lclist.cvf b/Examples/PassGH/lclist.cvf index 17f9ab9..52c4331 100644 --- a/Examples/PassGH/lclist.cvf +++ b/Examples/PassGH/lclist.cvf @@ -17,24 +17,24 @@ view has1Lock(Node x, Node y), has1LockAnon(Node x), has2Lock(Node x, Node y); method deleteVal(int v) { {| wf(v) |} - ; + <| prev = head; |> {| wf(v) * isHead(prev) |} - <{ %{ waitLock([|prev|]); takeLock([|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|]) }; }>; + <| %{ 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) |} - <%{ releaseLock([|prev|]) }>; + <| %{ releaseLock([|prev|]) }; |> {| wf(v) * wf(cv) * has1LockAnon(curr) * isVal(curr, cv) |} prev = curr; curr = %{ [|curr|].next }; {| wf(v) * wf(cv) * has1Lock(prev, curr) * isVal(prev,cv) |} - <{ %{ waitLock([|curr|]); takeLock([|curr|]) }; }>; + <| %{ waitLock([|curr|]); takeLock([|curr|]) }; |> {| wf(v) * has2Lock(prev, curr) |} cv = %{ [|curr|].val }; {| wf(v) * has2Lock(prev, curr) * isVal(curr,cv) |} @@ -43,17 +43,17 @@ method deleteVal(int v) { if (cv == v) { {| wf(cv) * has2Lock(prev, curr) * isVal(curr, cv) |} // Merged these two to avoid dangling nodes - <{ %{ [|prev|].next := [|curr|].next }; - %{ disposeNode([|curr|]) }; }>; + <| %{ [|prev|].next := [|curr|].next }; + %{ disposeNode([|curr|]) }; |> {| has1LockAnon(prev) |} } else { {| has2Lock(prev, curr) |} - <%{ releaseLock([|curr|])}>; + <| %{ releaseLock([|curr|])}; |> {| has1LockAnon(prev) |} } {| has1LockAnon(prev) |} - <%{ releaseLock([|prev|]) }>; + <| %{ releaseLock([|prev|]) }; |> {| emp |} } diff --git a/Examples/PassGH/spinLock.cvf b/Examples/PassGH/spinLock.cvf index c6c2860..32f5d3e 100644 --- a/Examples/PassGH/spinLock.cvf +++ b/Examples/PassGH/spinLock.cvf @@ -13,9 +13,9 @@ view newLock(Lock x), holdLock(Lock x), isLock(Lock x); method newLock() { {| emp |} - ; + <| ret = %{new Lock}; |> {| newLock(ret) |} - <%{[|ret|].lock := false}>; + <| %{[|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|]) }; |> {| if test == false then isLock(x) else holdLock(x) |} } while (test == false); {| holdLock(x) |} @@ -33,7 +33,7 @@ method lock(Lock x) { method unlock(Lock x) { {| holdLock(x) |} - <%{[|x|].lock := false}>; + <| %{[|x|].lock := false}; |> {| isLock(x) |} } diff --git a/Examples/PassGH/ticketLock.cvf b/Examples/PassGH/ticketLock.cvf index eac0617..d1b2782 100644 --- a/Examples/PassGH/ticketLock.cvf +++ b/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}; |> {| 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 }; }>; + <| t = %{ [|x|].ticket }; + %{ [|x|].ticket := [|x|].ticket + 1 }; |> {| holdTick(x, t) |} do { {| holdTick(x, t) |} - ; + <| s = %{ [|x|].serving }; |> {| if s == t then holdLock(x) else holdTick(x, t) |} } while (s != t); {| holdLock(x) |} @@ -34,7 +34,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/Parser.fs b/Parser.fs index bf6ef45..f9f34b8 100644 --- a/Parser.fs +++ b/Parser.fs @@ -58,22 +58,35 @@ let parseIdentifier = // Bracket parsers. -/// Parser for items in a pair of matching brackets. -/// Automatically parses any whitespace after `bra`, and before `ket`. +/// +/// Parser for items in a pair of matching brackets. +/// Automatically parses any whitespace after `bra`, and before `ket`. +/// let inBrackets bra ket = between (pstring bra .>> ws) (ws >>. pstring ket) -/// Parser for items in (parentheses). +/// +/// Parser for items in (parentheses). +/// let inParens p = inBrackets "(" ")" p -/// Parser for items in [brackets]. +/// +/// Parser for items in [brackets]. +/// let inSquareBrackets p = inBrackets "[" "]" p -/// Parser for items in {braces}. +/// +/// Parser for items in {braces}. +/// let inBraces p = inBrackets "{" "}" p -/// Parser for items in {|view braces|}. +/// +/// Parser for items in {|view braces|}. +/// let inViewBraces p = inBrackets "{|" "|}" p -/// Parser for items in {|interpolate braces|}. +/// +/// Parser for items in [|interpolate braces|]. +/// let inInterpBraces p = inBrackets "[|" "|]" p -/// Parser for items in . -let inAngles p = inBrackets "<" ">" p - +/// +/// Parser for items in <|atomic braces|>. +/// +let inAtomicBraces p = inBrackets "<|" "|>" p (* * Forwards. @@ -330,12 +343,7 @@ let parseAtomic = /// Parser for a collection of atomic actions. let parseAtomicSet = - inAngles ( - // Either one atomic... - (parseAtomic |>> List.singleton) - <|> - // ...or an atomic{} block. - (inBraces (many (parseAtomic .>> wsSemi .>> ws)))) + inAtomicBraces (many1 (parseAtomic .>> wsSemi .>> ws)) /// Parses a Func given the argument parser argp. let parseFunc argp = @@ -540,7 +548,7 @@ let parsePrimSet = 2 is easier to spot, so we try it first. *) let parseAtomicFirstPrimSet = pipe2 - (parseAtomicSet .>> wsSemi .>> ws) + (parseAtomicSet .>> ws) (many (attempt (parseAssign .>> wsSemi .>> ws))) (fun atom rassigns -> Prim { PreAssigns = []; Atomics = atom; PostAssigns = rassigns } ) @@ -549,7 +557,7 @@ let parsePrimSet = pipe2 (many1 (parseAssign .>> wsSemi .>> ws)) (opt - (parseAtomicSet .>> wsSemi .>> ws + (parseAtomicSet .>> ws .>>. many (parseAssign .>> wsSemi .>> ws))) (fun lassigns tail -> let (atom, rassigns) = withDefault ([], []) tail diff --git a/ParserTests.fs b/ParserTests.fs index d24cfe0..21e609f 100644 --- a/ParserTests.fs +++ b/ParserTests.fs @@ -231,27 +231,16 @@ module AtomicActionTests = module AtomicSetTests = - [] - let ````() = - check parseAtomicSet "" - [ node "" 1L 2L <| Postfix - (node "" 1L 2L (Identifier "foo"), - Increment) ] - - [] - let ``Multiple outside block invalid``() = - checkFail parseAtomicSet "" - [] let ``Single atomic block``() = - check parseAtomicSet "<{ foo++; }>" + check parseAtomicSet "<| foo++; |>" [ node "" 1L 4L <| Postfix (node "" 1L 4L (Identifier "foo"), Increment) ] [] let ``Multiple in block valid``() = - check parseAtomicSet "<{ foo++; bar--; }>" + check parseAtomicSet "<| foo++; bar--; |>" [ node "" 1L 4L <| Postfix (node "" 1L 4L (Identifier "foo"), Increment)