Control.Concurrent.CHP.Traces

A module that re-exports all the parts of the library related to tracing.

The idea of tracing is to record the concurrent events (i.e. channel communications and barrier synchronisations) that occur during a run of the program. You can think of it as automatically turning on a lot of debug logging.

Typically, at the top-level of your program you should have:

 main :: IO ()
 main = runCHP myMainProcess

To turn on the tracing mechanism of your choice (for example, CSP-style tracing) to automatically print out the trace after completion of your program, just use the appropriate helper function:

 main :: IO ()
 main = runCHP_CSPTraceAndPrint myMainProcess

It could hardly be easier. If you want more fine-grained control and examination of the trace, you can use the helper functions of the form runCHP_CSPTrace that give back a data structure representing the trace, which you can then manipulate.

The Doc used by the traces is from the HughesPJ module that currently comes with GHC (I think).

For more details on the theory behind the tracing, the logic behind its implementation, and example traces, see the paper "Representation and Implementation of CSP and VCR Traces", N.C.C. Brown and M.L. Smith, CPA 2008. An online version can be found at: http://twistedsquare.com/Traces.pdf

Documentation

module Control.Concurrent.CHP.Traces.CSP

module Control.Concurrent.CHP.Traces.Structural

module Control.Concurrent.CHP.Traces.TraceOff

module Control.Concurrent.CHP.Traces.VCR

type RecordedEvent u = (RecordedEventType, u)

A globally recorded event, found in CSP and VCR traces. Either a channel communication (with a unique identifier of the channel) or a barrier synchronisation (with a unique identifier of the barrier). The identifiers are per channel/barrier, not per event. Currently, channels and barriers can never have the same Unique as each other, but do not rely on this behaviour.

The type became parameterised in version 1.3.0.

type ChannelLabels u = Map u String

data RecordedEventType

The type of an event in the CSP and VCR traces.

ClockSync was added in version 1.2.0.

The extra parameter on ChannelComm and BarrierSync (which are the result of showing the value sent and phase ended respectively) was added in version 1.5.0.

Constructors

ChannelComm String

BarrierSync String

ClockSync String

Instances

Eq RecordedEventType

Ord RecordedEventType

Show RecordedEventType

data RecordedIndivEvent u

An individual record of an event, found in nested traces. Either a channel write or read, or a barrier synchronisation, each with a unique identifier for the barrier/channel. The event will be recorded by everyone involved, and a ChannelWrite will have the same channel identifier as the corresponding channel-read. The identifiers are per channel/barrier, not per event. Currently, channels and barriers can never have the same Unique as each other, but do not rely on this behaviour.

The type u item is the unique identifier of the channelbarrierclock, and the Integer is a sequence identifier for that channelbarrierclock (first sync is 0, second sync is 1, etc), and finally the String shows the value-sentphase-endedtime involved.

ClockSyncIndiv was added in version 1.2.0.

The type became parameterised, and the Show and Read instances were added in version 1.3.0.

The String parameters on ChannelWrite, ChannelRead and BarrierSyncIndiv were added in version 1.5.0.

Constructors

ChannelWrite u Integer String

ChannelRead u Integer String

BarrierSyncIndiv u Integer String

ClockSyncIndiv u Integer String

Instances

Eq u => Eq (RecordedIndivEvent u)

Ord u => Ord (RecordedIndivEvent u)

Read u => Read (RecordedIndivEvent u)

Show u => Show (RecordedIndivEvent u)

recordedIndivEventLabel :: RecordedIndivEvent u -> u

Added in version 1.3.0.

recordedIndivEventSeq :: RecordedIndivEvent u -> Integer

Added in version 1.3.0.

class Trace t where

A class representing a type of trace. The main useful function is runCHPAndTrace, but because its type is only determined by its return type, you may wish to use the already-typed functions offered in each trace module -- see the modules in Control.Concurrent.CHP.Traces.

The trace type involved became parameterised in version 1.3.0.

Methods

runCHPAndTrace :: CHP a -> IO (Maybe a, t Unique)

Runs the given CHP program, and returns its return value and the trace. The return value is a Maybe type because the process may have exited due to uncaught poison. In that case Nothing is return as the result.

emptyTrace :: t u

The empty trace.

prettyPrint :: Ord u => t u -> Doc

Pretty-prints the given trace using the Text.PrettyPrint.HughesPJ module.

labelAll :: Ord u => t u -> t String

Added in version 1.3.0.

Instances

Trace TraceOff

Trace CSPTrace

Trace StructuralTrace

Trace VCRTrace

vcrToCSP :: Eq u => VCRTrace u -> [CSPTrace u]

Takes a VCR trace and forms all the possible CSP traces (without duplicates) that could have arisen from the same execution.

This is done by taking all permutations of each set in the VCR trace (which is a list of sets) and concatenating them with the results of the same process on the rest of the trace. Thus the maximum size of the returned set of CSP traces is the product of the sizes of all the non-empty sets in the VCR trace.

This function was added in version 1.5.0.

structuralToCSP :: Ord u => StructuralTrace u -> [CSPTrace u]

Takes a structural trace and forms all the possible CSP traces (without duplicates) that could have arisen from the same execution.

This is done -- roughly speaking -- by replaying the structural trace in all possible execution orderings and pulling out the CSP trace for each ordering.

It should be the case for all structural traces t that do not use conjunction (every and '(<&>)'):

 structuralToCSP t =~= (concatMap vcrToCSP . structuralToVCR) t
   where a =~= b = or [a' == b' | a' <- permutations a, b' <- permutations  b]

This function was added in version 1.5.0.

structuralToVCR :: Ord u => StructuralTrace u -> [VCRTrace u]

Takes a structural trace and forms all the possible VCR traces (without duplicates) that could have arisen from the same execution.

This is done -- roughly speaking -- by replaying the structural trace in all possible execution orderings and pulling out the VCR trace for each ordering.

This function was added in version 1.5.0.