Merge branch 'next'

code/Peterson.hny

@@ -1,5 +1,7 @@
-sequential flags, turn
+in_cs = 0
+invariant in_cs in { 0, 1 }
 
+sequential flags, turn
 flags = [ False, False ]
 turn = choose({0, 1})
 
@@ -8,11 +10,11 @@ def thread(self):
         # Enter critical section
         flags[self] = True
         turn = 1 - self
-
         await (not flags[1 - self]) or (turn == self)
 
-        # Critical section is here
-        cs: assert countLabel(cs) == 1
+        atomically in_cs += 1
+        # Critical section
+        atomically in_cs -= 1
 
         # Leave critical section
         flags[self] = False

code/PetersonBroken.hny

@@ -1,5 +1,7 @@
-sequential flags, turn
+in_cs = 0
+invariant in_cs in { 0, 1 }
 
+sequential flags, turn
 flags = [ False, False ]
 turn = choose({0, 1})
 
@@ -8,11 +10,11 @@ def thread(self):
         # Enter critical section
         turn = 1 - self
         flags[self] = True
-
         await (not flags[1 - self]) or (turn == self)
 
-        # Critical section is here
-        cs: assert countLabel(cs) == 1
+        atomically in_cs += 1
+        # Critical section
+        atomically in_cs -= 1
 
         # Leave critical section
         flags[self] = False

code/PetersonInductive.hny

@@ -1,17 +1,19 @@
-sequential flags, turn
+at_gate = 0
 
+sequential flags, turn
 flags = [ False, False ]
 turn = choose({0, 1})
 
 def thread(self):
     while choose({ False, True }):
         # Enter critical section
         flags[self] = True
-        gate: turn = 1 - self
+        atomically at_gate += 1
+        atomically at_gate -= 1
         await (not flags[1 - self]) or (turn == self)
 
         # Critical section
-        cs: assert (not flags[1 - self]) or (turn == self) or (countLabel(gate) == 1)
+        assert (not flags[1 - self]) or (turn == self) or (at_gate == 1)
 
         # Leave critical section
         flags[self] = False

code/PetersonMethod.hny

@@ -11,13 +11,20 @@ def P_mutex() returns result:
 
 #### The code above can go into its own Harmony module ####
 
+in_cs = 0
+invariant in_cs in { 0, 1 }
+
 sequential mutex
 mutex = P_mutex()
 
 def thread(self):
     while choose({ False, True }):
         P_enter(?mutex, self)
-        cs: assert countLabel(cs) == 1
+
+        atomically in_cs += 1
+        # Critical section
+        atomically in_cs -= 1
+
         P_exit(?mutex, self)
 
 spawn thread(0)

code/RWbtest.hny

@@ -10,15 +10,15 @@ def thread(self):
             print(self, "enter ra")
             RW.read_acquire(?rw)
             print(self, "exit ra")
-            rcs: assert (countLabel(rcs) >= 1) and (countLabel(wcs) == 0)
+
             print(self, "enter rr")
             RW.read_release(?rw)
             print(self, "exit rr")
         else:                       # write
             print(self, "enter wa")
             RW.write_acquire(?rw)
             print(self, "exit wa")
-            wcs: assert (countLabel(rcs) == 0) and (countLabel(wcs) == 1)
+
             print(self, "enter wr")
             RW.write_release(?rw)
             print(self, "enter wr")

code/RWtest.hny

@@ -1,5 +1,9 @@
 import RW
 
+nreaders = nwriters = 0
+invariant ((nreaders >= 0) and (nwriters == 0)) or
+            ((nreaders == 0) and (0 <= nwriters <= 1))
+
 const NOPS = 3
 
 rw = RW.RWlock()
@@ -8,11 +12,13 @@ def thread():
     while choose({ False, True }):
         if choose({ "read", "write" }) == "read":
             RW.read_acquire(?rw)
-            rcs: assert (countLabel(rcs) >= 1) and (countLabel(wcs) == 0)
+            atomically nreaders += 1
+            atomically nreaders -= 1
             RW.read_release(?rw)
         else:                       # write
             RW.write_acquire(?rw)
-            wcs: assert (countLabel(rcs) == 0) and (countLabel(wcs) == 1)
+            atomically nwriters += 1
+            atomically nwriters -= 1
             RW.write_release(?rw)
 
 for i in {1..NOPS}:

code/UpEnter.hny

@@ -1,7 +1,5 @@
 count = 0
 
-finally count == 2
-
 entered = done = [ False, False ]
 
 def incrementer(self):

code/Upr.hny

@@ -2,9 +2,9 @@ count = 0
 done = [ False, False ]
 
 def incrementer(self):
-    var register = count    # load count
-    register += 1           # increment
-    count = register        # store count
+    var register = count    # load shared variable count into a private register
+    register += 1           # increment the register
+    count = register        # store its value into variable count
     done[self] = True
     await done[1 - self]
     assert count == 2

code/boundedbuffer.hny

@@ -1,13 +1,11 @@
-import list
-
 def BoundedBuffer(size) returns buffer:
     buffer = { .buffer: [], .size: size }
 
 def put(bb, v):
     atomically when len(bb->buffer) < bb->size:
-        bb->buffer = list.append(bb->buffer, v)
+        bb->buffer += [v,]
 
 def get(bb) returns next:
     atomically when bb->buffer != []:
-        next = list.head(bb->buffer)
-        bb->buffer = list.tail(bb->buffer)
+        next = bb->buffer[0]
+        del bb->buffer[0]

code/cs.hny

@@ -1,11 +1,17 @@
+# number of threads in the critical section
+in_cs = 0
+invariant in_cs in { 0, 1 }
+
 def thread():
-    while choose({ False, True }):
+    while choose { False, True }:
         # Enter critical section
+        atomically in_cs += 1
 
         # Critical section is here
-        cs: assert countLabel(cs) == 1
+        pass
 
         # Exit critical section
+        atomically in_cs -= 1
 
 spawn thread()
 spawn thread()

code/csbarebones.hny

@@ -1,11 +1,7 @@
 def thread():
     while True:
-        # Enter critical section
-
         # Critical section is here
-        cs: assert countLabel(cs) == 1
-
-        # Exit critical section
+        pass
 
 spawn thread()
 spawn thread()

code/csonebit.hny

@@ -1,5 +1,7 @@
-sequential flags
+in_cs = 0
+invariant in_cs in { 0, 1 }
 
+sequential flags
 flags = [ False, False ]
 
 def thread(self):
@@ -10,8 +12,9 @@ def thread(self):
             flags[self] = False
             flags[self] = True
 
+        atomically in_cs += 1
         # Critical section
-        cs: assert countLabel(cs) == 1
+        atomically in_cs -= 1
 
         # Leave critical section
         flags[self] = False

code/cssynch.hny

@@ -1,14 +1,21 @@
-from synch import Lock, acquire, release
+import synch
 
-const NTHREADS = 3
+const NTHREADS = 2
 
-the_lock = Lock()
+in_cs = 0
+invariant in_cs in { 0, 1 }
+
+lock = synch.Lock()
 
 def thread():
     while choose({ False, True }):
-        acquire(?the_lock)
-        cs: assert countLabel(cs) == 1
-        release(?the_lock)
+        synch.acquire(?lock)
+
+        atomically in_cs += 1
+        # Critical section
+        atomically in_cs -= 1
+
+        synch.release(?lock)
 
 for i in {1..NTHREADS}:
     spawn thread()

code/naiveFlags.hny

@@ -1,3 +1,6 @@
+in_cs = 0
+invariant in_cs in { 0, 1 }
+
 flags = [ False, False ]
 
 def thread(self):
@@ -6,8 +9,9 @@ def thread(self):
         flags[self] = True
         await not flags[1 - self]
 
+        atomically in_cs += 1
         # Critical section
-        cs: assert countLabel(cs) == 1
+        atomically in_cs -= 1
 
         # Leave critical section
         flags[self] = False

code/naiveLock.hny

@@ -1,3 +1,6 @@
+in_cs = 0
+invariant in_cs in { 0, 1 }
+
 lockTaken = False
 
 def thread(self):
@@ -6,8 +9,9 @@ def thread(self):
         await not lockTaken
         lockTaken = True
 
+        atomically in_cs += 1
         # Critical section
-        cs: assert countLabel(cs) == 1
+        atomically in_cs -= 1
 
         # Leave critical section
         lockTaken = False

code/naiveTurn.hny

@@ -1,3 +1,6 @@
+in_cs = 0
+invariant in_cs in { 0, 1 }
+
 turn = 0
 
 def thread(self):
@@ -6,8 +9,9 @@ def thread(self):
         turn = 1 - self
         await turn == self
 
+        atomically in_cs += 1
         # Critical section
-        cs: assert countLabel(cs) == 1
+        atomically in_cs -= 1
 
         # Leave critical section
 

code/queuespec.hny

@@ -1,15 +1,13 @@
-import list
-
 def Queue() returns empty:
     empty = []
 
 def put(q, v):
-    !q = list.append(!q, v)
+    !q += [v,]
+
 
 def get(q) returns next:
     if !q == []:
         next = None
     else:
-        next = list.head(!q)
-        !q = list.tail(!q)
-
+        next = (!q)[0]
+        del (!q)[0]

code/spinlock.hny

@@ -1,8 +1,10 @@
 const N = 3
 
+in_cs = 0
+invariant in_cs in { 0, 1 }
+
 shared = False
 private = [ True, ] * N
-
 invariant len(x for x in [shared,] + private where not x) <= 1
 
 def test_and_set(s, p):
@@ -20,8 +22,9 @@ def thread(self):
         while private[self]:
             test_and_set(?shared, ?private[self])
 
-        # Critical section
-        cs: assert (not private[self]) and (countLabel(cs) == 1)
+        atomically in_cs += 1
+        assert not private[self]
+        atomically in_cs -= 1
 
         # Leave critical section
         private[self] = True