Latest

harmonylang · Nov 13, 2024 · e06cb80 · e06cb80
1 parent 72ac820
commit e06cb80
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git a/code/barrier_test1.hny b/code/barrier_test1.hny
@@ -3,15 +3,20 @@ import barrier
 const NTHREADS = 3
 const NROUNDS = 4
 
+barr = barrier.Barrier(NTHREADS)
 round = [0,] * NTHREADS
-invariant (max(round) - min(round)) <= 1
+in_b = [False,] * NTHREADS
 
-barr = barrier.Barrier(NTHREADS)
+invariant all((in_b[i] and in_b[j]) => (round[i] == round[j])
+        for i in { 0 .. NTHREADS - 1 } for j in { 0 .. NTHREADS - 1 })
 
 def thread(self):
     for r in {0..NROUNDS-1}:
-        barrier.bwait(?barr)
         round[self] += 1
+        barrier.bwait(?barr)
+        in_b[self] = True
+        pass
+        in_b[self] = False
 
 for i in {0..NTHREADS-1}:
     spawn thread(i)
diff --git a/code/barrier_test2.hny b/code/barrier_test2.hny
@@ -3,18 +3,16 @@ import barrier
 const NTHREADS = 3
 const NROUNDS = 4
 
+barr = barrier.Barrier(NTHREADS)
 round = [0,] * NTHREADS
-invariant (max(round) - min(round)) <= 1
-
 phase = 0
-barr = barrier.Barrier(NTHREADS)
 
 def thread(self):
     for r in {0..NROUNDS-1}:
+        round[self] += 1
         if self == 0:                # coordinator prepares
             phase += 1
         barrier.bwait(?barr)         # enter parallel work
-        round[self] += 1
         assert round[self] == phase
         barrier.bwait(?barr)         # exit parallel work