chp-1.8.0: An implementation of concurrency ideas from Communicating Sequential Processes



A module containing barriers.

A barrier is a synchronisation primitive. When N processes are enrolled on a barrier, all N must synchronise on the barrier before any synchronisations may complete, at which point they all complete. That is, when a single process synchronises on a barrier, it must then wait until all the other enrolled processes also synchronise before it can finish.

Only processes enrolled on a barrier may synchronise on it. Enrolled barriers should not be passed around between processes, or used twice in a parallel composition. Instead, each process should enroll on the barrier itself.

Barriers support choice (alting). This can lead to a lot of non-determinism and some confusion. Consider these two processes, both enrolled on barriers a and b:

 (sync a <-> sync b)
 (sync b <-> sync a)

Which barrier completes is determined by the run-time, and will be an arbitrary choice. This is even the case when priority is involved:

 (sync a </> sync b)
 (sync b </> sync a)

Clearly there is no way to resolve this to satisfy both priorities; the run-time will end up choosing.

Barrier poison can be detected when syncing, enrolling or resigning. You may only poison a barrier that you are currently enrolled on.

Barriers can also support phases. The idea behind a phased barrier is that a barrier is always on a certain phase P. Whenever a barrier successfully completes, the phase is incremented (but it does not have to be an integer). Everyone is told the new phase once they complete a synchronisation, and may query the current phase for any barrier that they are currently enrolled on.



type Barrier = PhasedBarrier ()Source

A special case of the PhasedBarrier that has no useful phases, i.e. a standard barrier.

type EnrolledBarrier = Enrolled PhasedBarrier ()Source

A useful type synonym for enrolled barriers with no phases

Added in 1.1.0

newBarrier :: CHP BarrierSource

Creates a new barrier with no processes enrolled

newBarrierWithLabel :: String -> CHP BarrierSource

Creates a new barrier with no processes enrolled and labels it in traces using the given label. See newBarrier.

data PhasedBarrier phase Source

A phased barrier that is capable of being poisoned and throwing poison. You will need to enroll on it to do anything useful with it. For the phases you can use any type that satisfies Enum, Bounded and Eq. The phase increments every time the barrier completes. Incrementing consists of: if p == maxBound then minBound else succ p. Examples of things that make sense for phases:

  • The () type (see the Barrier type). This effectively has a single repeating phase, and acts like a non-phased barrier.
  • A bounded integer type. This increments the count every time the barrier completes. But don't forget that the count will wrap round when it reaches the end. You cannot use Integer for a phase because it is unbounded. If you really want to have an infinitely increasing count, you can wrap Integer in a newtype and provide a Bounded instance for it (with minBound and maxBound set to -1, if you start on 0).
  • A boolean. This implements a simple black-white barrier, where the state flips on each iteration.
  • A custom data type that has only constructors. For example, data MyPhases = Discover | Plan | Move. Haskell supports deriving Enum, Bounded and Eq automatically on such types.

newPhasedBarrier :: (Enum phase, Bounded phase, Eq phase, Show phase) => phase -> CHP (PhasedBarrier phase)Source

Creates a new barrier with no processes enrolled, that will be on the given phase. You will often want to pass in the last value in your phase cycle, so that the first synchronisation moves it on to the first

The Show constraint was added in version 1.5.0

newPhasedBarrier' :: phase -> BarOpts phase -> CHP (PhasedBarrier phase)Source

Like newPhasedBarrier but allows you to customise the options.

data BarOpts phase Source

Options for barrier creation; a function to show the inner data, and an optional label (both only affect tracing). These options can be passed to newPhasedBarrier'.

Added in version 1.7.0.




barIncPhase :: phase -> phase

Aside from the standard defaultIncPhase, you can use succ or (+1) with Integer as the inner type to get a barrier that never cycles. You can also do things like supplying (+2) as the incrementing function, or even using lists as the phase type to do crazy things.

barOptsShow :: phase -> String
barOptsLabel :: Maybe String

defaultIncPhase :: (Enum phase, Bounded phase, Eq phase) => phase -> phaseSource

The default phase incrementing function. If the phase is already at maxBound, it sets it to minBound; otherwise it uses succ to increment the phase.

defaultBarOpts :: (Enum phase, Bounded phase, Eq phase) => BarOpts phaseSource

The default: don't show anything, don't label anything, use Enum+Bounded+Eq to work out the phase increment.

Added in version 1.7.0.

barLabel :: (Enum phase, Bounded phase, Eq phase, Show phase) => String -> BarOpts phaseSource

Uses the Show instance for showing the data in traces, and the given label.

Added in version 1.7.0.

currentPhase :: Enrolled PhasedBarrier phase -> CHP phaseSource

Finds out the current phase a barrier is on.

waitForPhase :: Eq phase => phase -> Enrolled PhasedBarrier phase -> CHP ()Source

If the barrier is not in the given phase, synchronises on the barrier repeatedly until it is in the given phase.

syncAndWaitForPhase :: Eq phase => phase -> Enrolled PhasedBarrier phase -> CHP ()Source

Synchronises on the barrier at least once, until it is in the given phase.

Note that syncAndWaitForPhase ph bar == syncBarrier bar >> waitForPhase ph bar.

Added in version 1.7.0.

syncBarrier :: Enrolled PhasedBarrier phase -> CHP phaseSource

Synchronises on the given barrier. You must be enrolled on a barrier in order to synchronise on it. Returns the new phase, following the synchronisation.

getBarrierIdentifier :: PhasedBarrier ph -> UniqueSource

Gets the identifier of a Barrier. Useful if you want to identify it in the trace later on.