Documentation

Std.Sync.Barrier

structure Std.Barrier :

A Barrier will block n - 1 threads which call Barrier.wait and then wake up all threads at once when the n-th thread calls Barrier.wait.

def Std.Barrier.new (numThreads : Nat) :

Creates a new barrier that can block a given number of threads.

Equations
  • One or more equations did not get rendered due to their size.

Blocks the current thread until all threads have rendezvoused here.

Barriers are re-usable after all threads have rendezvoused once, and can be used continuously.

A single (arbitrary) thread will receive true when returning from this function, and all other threads will receive false.

Equations
  • One or more equations did not get rendered due to their size.