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.

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

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

    Equations
      Instances For

        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
          Instances For