A deterministic program exhibits a single trace, which may be modeled as a string (linearly ordered multiset) where each character represents an atomic action. Concurrency deals with nondeterministic composition of programs. Hence, a concurrent program can exhibit multiple traces. To accommodate this, we can extend the trace model to a set of traces. For example, to model a program that executes 3 atomic actions , , and concurrently, we can explicitly list all 6 possible traces (, , , , , and ). In general, a program that executes atomic actions concurrently has traces. A drawback of this model is that it obscures the happens-before relation. Given a set of traces, it is not immediately obvious which event must happen before another event. Partially ordered multisets (pomsets) offer a compact alternative by relaxing the linear order to a partial order. The partial order corresponds to the happens-before relation, making it explicit.
The definitions of pomsets and pomset homomorphisms are adapted from Plotkin and Pratt's work.
A pomset consists of the following data:
We write to denote a pomset whose set of nodes is , partial order is , set of labels is , and label assignment is . We abbreviate this notation to whenever possible.
We can think of as a set of events where determines which event happens before other events. Thus, and together determine the skeleton of a program. For example, the diagram below represents a program with 6 total events.
The partial order determines which event happens before others. In this case, has to happen before all other events. And since and , they can happen concurrently. The underlying partial order only tells half of the story. We would like to know what atomic action to perform for each event. We can think of the label set as a set of available actions and associates each event with an atomic action. For example, suppose that , and that . Then the pomset describes a recipe.
This program can exhibit a few different traces. For example, the cook can do all the preliminary preparations first (break eggs and cut veggies), and then fry them separately. Alternatively, the cook can prepare eggs (break eggs and fry eggs) first, and then prepare veggies.
A pomset homomorphism consists of the following data:
We write to denote a pomset homomorphism where and .
We are rarely interested in the underlying sets representing events and labels. For example, the events and may as well be represented as the set or . Thus, what we have just defined is technically a labeled partial order. And a pomset is defined as an isomorphism class of labeled partial orders. We continue to use our definitions for its simplicity. However, we must keep in mind the implicit proof obligation that constructions on pomsets need to be stable under isomorphisms.
We alluded to the notion of a trace of a pomset in the example given below the definition of pomsets. Intuitively, a trace of a pomset is a string such that is "compatible" with . We can describe this intuition in terms of pomset homomorphisms.
First, recall that a string is a linearly ordered multiset and a linear order is a partial order. Thus, a string is also a pomset. A trace of a pomset is a string for which is a pomset homomorphism.
Below, the string on the right depicts a valid trace of the pomset on the left.
However, the string on the right below is not a trace of the pomset on the left because is not monotone: the order of "cut veggies" and "fry veggies" has been inverted.
The following constructions are adapted from the work of Kappé et al.
Given two programs and , there are two ways to compose them: concurrent composition and sequential composition. Their composition is another program. To support its interpretation as a pomset, we need to define some suitable constructions on pomsets.
Given two programs and , we can compose them concurrently, yielding a new program that allows any arbitrary interleaving of the two programs. When viewed as a pomset, ought to have the following properties:
This pomset contains all the events in , all the events in , and all the order contraints imposed by and but nothing else.
The label assignment is given by
For example,
Given two programs and , the sequential composition is simply a program that executes first and then executes . Thus, when viewed as a pomset, ought to satisfy:
contains all the events in , all the events in , all the order contraints imposed by and , and new order contraints requiring events in to precede those in but nothing else. For example,
Reasoning about concurrent programs is hard. To tame its complexity, researchers turn to mathematical structures such as event structures, petri nets, and pomsets. By making the happens-before relation explicit, pomsets offer a compact representation of concurrent programs and a simple construction for concurrent composition. To see this, consider two sequential programs and , exhibiting traces and , respectively. To represent the concurrent composition of and in the trace model we need to construct a set of all interleaving of and , while the construction in the pomset model is relatively trivial. A more compact model with simpler constructions could reduce the complexity of analyzing concurrent programs.
Of course, this short wiki on pomsets only covers the tip of the iceberg. We briefly survey a number of works on pomsets in the literature.
Plotkin, G., & Pratt, V. (1997). Teams Can See Pomsets (Preliminary Version). Proceedings of the DIMACS Workshop on Partial Order Methods in Verification, 117–128.
@inproceedings{10.5555/266557.266600,
author = {Plotkin, Gordon and Pratt, Vaughan},
title = {Teams Can See Pomsets (Preliminary Version)},
year = {1997},
isbn = {0821805797},
publisher = {AMS Press, Inc.},
address = {USA},
booktitle = {Proceedings of the DIMACS Workshop on Partial Order Methods in Verification},
pages = {117–128},
numpages = {12},
location = {Princeton, New Jersey, USA},
series = {POMIV '96}
}
Kappé, T., Brunet, P., Luttik, B., Silva, A., & Zanasi, F. (2017). Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages. In R. Meyer & U. Nestmann (Eds.), 28th International Conference on Concurrency Theory (CONCUR 2017) (Vol. 85, p. 25:1-25:16). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.25
@InProceedings{kapp_et_al:LIPIcs:2017:7791,
author = {Tobias Kapp{\'e} and Paul Brunet and Bas Luttik and Alexandra Silva and Fabio Zanasi},
title = {{Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Roland Meyer and Uwe Nestmann},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7791},
URN = {urn:nbn:de:0030-drops-77913},
doi = {10.4230/LIPIcs.CONCUR.2017.25},
annote = {Keywords: Kleene theorem, Series-rational expressions, Automata, Brzozowski derivatives, Concurrency, Pomsets}
}
Gischer, J. L. (1988). The Equational Theory of Pomsets. Theor. Comput. Sci., 61(2–3), 199–224. https://doi.org/10.1016/0304-3975(88)90124-7
@article{10.1016/0304-3975(88)90124-7,
author = {Gischer, Jay L.},
title = {The Equational Theory of Pomsets},
year = {1988},
issue_date = {Nov. 1988},
publisher = {Elsevier Science Publishers Ltd.},
address = {GBR},
volume = {61},
number = {2–3},
issn = {0304-3975},
url = {https://doi.org/10.1016/0304-3975(88)90124-7},
doi = {10.1016/0304-3975(88)90124-7},
journal = {Theor. Comput. Sci.},
month = {nov},
pages = {199–224},
numpages = {26}
}
Edixhoven, L., Jongmans, S.-S., Proença, J., & Cledou, G. (2022). Branching Pomsets for Choreographies. Electronic Proceedings in Theoretical Computer Science, 365, 37–52. https://doi.org/10.4204/eptcs.365.3
@article{Edixhoven_2022,
doi = {10.4204/eptcs.365.3},
url = {https://doi.org/10.4204%2Feptcs.365.3},
year = 2022,
month = {aug},
publisher = {Open Publishing Association},
volume = {365},
pages = {37--52},
author = {Luc Edixhoven and Sung-Shik Jongmans and Jos{\'{e}
} Proen{\c{c}}a and Guillermina Cledou},
title = {Branching Pomsets for Choreographies},
journal = {Electronic Proceedings in Theoretical Computer Science}
}
Cattani, G., & Winskel, G. (11 1996). Presheaf Models for Concurrency. 3. doi:10.1007/3-540-63172-0_32
@inproceedings{inproceedings,
author = {Cattani, Gian and Winskel, Glynn},
year = {1996},
month = {11},
pages = {},
title = {Presheaf Models for Concurrency},
volume = {3},
isbn = {978-3-540-63172-9},
journal = {Lecture Notes in Computer Science},
doi = {10.1007/3-540-63172-0_32}
}