In mathematics and computer science, a history monoid is a way of representing the histories of concurrently running computer processes as a collection of strings, each string representing the individual history of a process.
The history monoid provides a set of synchronization primitives (such as locks, mutexes or thread joins) for providing rendezvous points between a set of independently executing processes or threads.
History monoids occur in the theory of concurrent computation, and provide a low-level mathematical foundation for process calculi, such as CSP the language of communicating sequential processes, or CCS, the calculus of communicating systems.
As such, they are free objects and are universal.
The history monoid is a type of semi-abelian categorical product in the category of monoids.
Let denote an n-tuple of (not necessarily pairwise disjoint) alphabets
denote all possible combinations of one finite-length string from each alphabet: (In more formal language,
is the Cartesian product of the free monoids of the
Composition in the product monoid is component-wise, so that, for and then for all
, separating it into components in each free monoid: For every
is called the elementary history of a.
It serves as an indicator function for the inclusion of a letter a in an alphabet
is the submonoid of the product monoid
generated by the elementary histories:
(where the superscript star is the Kleene star applied with a component-wise definition of composition as given above).
The use of the word history in this context, and the connection to concurrent computing, can be understood as follows.
An individual history is a record of the sequence of states of a process (or thread or machine); the alphabet
is the set of states of the process.
A letter that occurs in two or more alphabets serves as a synchronization primitive between the various individual histories.
That is, if such a letter occurs in one individual history, it must also occur in another history, and serves to "tie" or "rendezvous" them together.
In this example, an individual history of the first process might be
while the individual history of the second machine might be
can be considered to commute with the letters
, in that these can be rearranged without changing the individual histories.
Such commutation is simply a statement that the first and second processes are running concurrently, and are unordered with respect to each other; they have not (yet) exchanged any messages or performed any synchronization.
serves as a synchronization primitive, as its occurrence marks a spot in both the global and individual histories, that cannot be commuted across.
with the dependency relation given by In simple terms, this is just the formal statement of the informal discussion given above: the letters in an alphabet
can be commutatively re-ordered past the letters in an alphabet
Thus, traces are exactly global histories, and vice versa.
, one can construct an isomorphic history monoid by taking a sequence of alphabets