Partially Ordered Multisets

Introduction

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 a, b, and c concurrently, we can explicitly list all 6 possible traces (abc, bac, bca, cba, acb, and cab). In general, a program that executes n atomic actions concurrently has n! 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.

Definitions

The definitions of pomsets and pomset homomorphisms are adapted from Plotkin and Pratt's work.

Pomset

A pomset consists of the following data:

a set U of nodes,
a partial order \leq on the set of nodes,
a set L of labels, and
a label assignment \lambda : U \to L assigning each node to a label.

We write (U, \leq, L, \lambda) to denote a pomset whose set of nodes is U, partial order is \leq, set of labels is L, and label assignment is \lambda. We abbreviate this notation to (\leq_{U}, \lambda_{L}) whenever possible.

We can think of U as a set of events where \leq determines which event happens before other events. Thus, U and \leq together determine the skeleton of a program. For example, the diagram below represents a program with 6 total events.

<mxfile host="embed.diagrams.net" modified="2023-04-26T15:57:51.867Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:109.0) Gecko/20100101 Firefox/112.0" etag="NczGkN59Ni75NgzNLOfb" version="21.2.2" type="embed"><diagram id="B6VOc9gTG1b0HQLpoPe0" name="Page-1">5Zhdc6IwFIZ/jbcdIAb0stpu92ZnOuPF7l5myClkGogTouL++g0lfIRo61h1XXsl5004SZ43kIMjNM/KJ0mW6Q9BgY8Cj5Yj9DAKAt+fjvVPpWxrJYpQLSSSUdOpExbsDxjRM+qKUSisjkoIrtjSFmOR5xArSyNSio3d7UVwe9QlScARFjHhrvqTUZXW6gR7nf4dWJI2I/ueaclI09kIRUqo2PQk9DhCcymEqq+ycg68gtdwqe/7tqe1nZiEXB1yQ1DfsCZ8ZdYGJkehts1yFZQ62SxVGdeCry8LJcUrzAUXUiu5yHXP2QvjfCARzpJch7GeDmh9tgapmAZ5bxoyRmk1zGyTMgWLJYmrMTd622hNilVOoZqppyN3aWamVU4oe5JZ6hOIDJTc6i5Na4Pd7LtgauJN52JopLRnIDIaMfsmaTN3aPWFobubNHJJB7dLOvAGpPHlSI9d0ujrkEbjy5HGLunx7ZJG/3BPhy5p/HVIX3JPRy7p8IZJRwPS3uVITxzSDmfI6X1Vr1XAOCkKFtvUbR5QMvWrur4LETLx717bQ9kPtr3gGSTT868MeZ9sIVYyBqt2AmoViy7qHkq8A2WjSeBEsbVdYu7ia0Z4FkxPrqttwj1ONinqqZu7+iXhIFFbZTevuWiQSBGZgHISvdndLvugHTA93w7APf/9d/3/H70ePrX+ibxG+Gxe+/6pzd5rXD1pq0S5EuPaPM2zFR5r3GSQaHw+49xvxHMZd6UuIYzu8HE+OZUMDoepTuiU+4154061heG+s+pgn6YfvFFP6JL7ffrZUy/Xg9fHXoCbuD34qqA7+d6iD4++/hs0umrHP/NsRpGdaljUHu25Dru/8Oru3R+h6PEv</diagram></mxfile>

The partial order determines which event happens before others. In this case, e_{1} has to happen before all other events. And since e_{2} \nleq e_{3} and e_{3} \nleq e_{2}, 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 L as a set of available actions and \lambda_{L} associates each event with an atomic action. For example, suppose that L = \{\textsf{turn on stove}, \textsf{break eggs}, \textsf{fry eggs}, \textsf{cut veggies}, \textsf{fry veggies}, \textsf{turn off stove}\}, and that \lambda_{L} = \{e_{1} \mapsto \textsf{turn on stove}, e_{2} \mapsto \textsf{break eggs}, e_{3} \mapsto \textsf{cut veggies}, e_{4} \mapsto \textsf{fry eggs}, e_{5} \mapsto \textsf{fry veggies}, e_{6} \mapsto \textsf{turn off stove}\}. Then the pomset (\leq_{U}, \lambda_{L}) describes a recipe.

<mxfile host="embed.diagrams.net" modified="2023-04-26T17:36:27.936Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:109.0) Gecko/20100101 Firefox/112.0" etag="svv_gTzkEyNrWWfQyD_c" version="21.2.2" type="embed"><diagram id="xDXJjQnMv8ta7F46lmY5" name="Page-1">5VhNj9owEP01XKskdhY4LrDdXipV4tD26MaTxFonRo4Dob++DnFIYoOKELCr7AU8z+Ox5z1/ZoKWWfUqySb9LijwSeDRaoJWkyDw/TnWfzWyb5DpFDVAIhk1Th2wZn/BgJ5BS0ahGDgqIbhimyEYiTyHSA0wIqXYDd1iwYe9bkgCDrCOCHfRn4yqtEFnodfh34Aladuz75majLTOBihSQsWuB6GXCVpKIVRTyqol8Jq8lpem3dcztceBScjVJQ2CpsGW8NLkpkqZa0TUP4USWzADVfs2ewWVjr1IVcY14OtioaR4g6XgQmokF7n2XMSMcwsinCW5NiM9OtD4YgtSMc3rs6nIGKV1N4tdyhSsNySq+9zpWaQxKcqcQj1wT1tupib5OiZUPchk/goiAyX32qWtnRkVzDRET8bedaK2UNrTExmMmGmUHCN3TOuCIfs08cgh/o8E8qYhSJJivJwHFufB/HGcY4fz+DC0cTOOg/djPHQYj0p1GH2SMBgx6fY0x+hxpD+dmeajJ92e6Y8kfXr2II3j8Z+kof9+J+nMYd7hGXL6XF/7asI4KQoWDVm/kA+gg2uhy0Yv2/BEti0mgRPFtsPL5CkKTA8/BMtVb2/BZ8huQxSilBGYVv3Lnx1obgXyrUCKyASUE+igyDHti0RqI99OJS2O3P/qG79r44s+c4y9qvq1q/3/5G2yHRxcH0VxZAk1v1Zx+8aL76e4f2vFP/q6RPa6tJfTpSpheze947p0H4CfTCUc3kglJ9ANVXJfiyNXCdsb1bVrKbTuhOiOKrnvy0+mEraPk2tVwt6tVNJm9zWtce++SaKXfw==</diagram></mxfile>

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.

Pomset Homomorphism

A pomset homomorphism \phi : (\leq_{U}, \lambda_{L}) \to (\leq'_{U'}, \lambda'_{L'}) consists of the following data:

a function f : U \to U', and
a function g : L \to L'
satisfying the following axioms:
f is monotone: for all u_{1}, u_{2} \in U, if u_{1} \leq u_{2}, then f(u_{1}) \leq' f(u_{2}), and
f and g are compatible with the label assignments: for all u \in U, g(\lambda(u)) = \lambda'(f(u)).

We write (f, g) : (\leq_{U}, \lambda_{L}) \to (\leq'_{U'}, \lambda'_{L'}) to denote a pomset homomorphism where f : U \to U' and g : L \to L'.

We are rarely interested in the underlying sets representing events and labels. For example, the events e_{1}, e_{2}, and e_{3} may as well be represented as the set \{1, 2, 3\} or \{4, 5, 6\}. 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.

From Pomsets to Traces

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 (\leq_{U}, \lambda_{L}) is a string (\leq'_{U}, \lambda_{L}) such that \leq'_{U} is "compatible" with \leq_{U}. 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 (\leq_{U}, \lambda_{L}) is a string (\leq'_{U}, \lambda_{L}) for which (id_{U}, id_{L}) : (\leq_{U}, \lambda_{L}) \to (\leq'_{U}, \lambda_{L}) is a pomset homomorphism.

Below, the string on the right depicts a valid trace of the pomset on the left.

<mxfile host="embed.diagrams.net" modified="2023-04-26T18:21:47.807Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:109.0) Gecko/20100101 Firefox/112.0" etag="OzxzDSYohgykO66h2m8-" version="21.2.2" type="embed"><diagram id="oQDAGaKUVMW4XbmnUEji" name="Page-1">5VpNk6IwEP01XqfkI4LH0ZmdvWzVVM1hd45ZiJAaJFaIivvrN0gQSGON4wKLclHyCJ3kvU7SaZhYy3X6wvEm/MF8Ek3MqZ9OrKeJaRrG3JZ/GXLIEcexciDg1FeVSuCN/iEKnCp0S32S1CoKxiJBN3XQY3FMPFHDMOdsX6+2YlG91Q0OCADePBxB9Cf1RZijLpqW+HdCg7Bo2ZiqO2tcVFZAEmKf7SuQ9TyxlpwxkV+t0yWJMvIKXvLnvp25e+oYJ7G45AEzf2CHo60am9jyWCIs+0kE2xHVUXEoRi9IKm0vQrGOJGDIy0Rw9kGWLGJcIjGLZc3FikaRBuGIBrEserJ3ROKLHeGCSl4f1Y019f2smcU+pIK8bbCXtbmXXiQxzraxT7KOT2UJjlQNPrNJ0gqkRv5C2JoIfpBVirszpYJyQ9tV5X0palElrOhpKQwrNwpOlkum5YUiu5l4CxD/mxP8ISESBMn9cu5olJv9UW4Dyr2tOHY+CCi5Y85N3c97JB0B0lfHro3Ky815f4TPzhA+Oi/vk3Tn7Da6Wo1vHzV6ZN4FzAOeSew/ZkFfRliEk4R6ddYv5IP4taAQslEZLWoYbYFxEmFBd/VQsokC1cIro7GouLlZJxtNNRYTtuUeUU9VQz/dkL4VI82QwDwgAhg6KnIa9kUizdsWSWrDD7+ywgMqiu+q5rHwlFZrPh0+Ezcfay00G4jeIEidX6u3oRmyO9O7aOlGBEfDEnx6Jlr7quAGqhuynO4EN25K8NmgBD8FKv8quGX3JzhMHLQnuNm+4s6gFNenuHntmq5PcbPDNR1mLNpT3J05X5H8WHolnMr+Z/HvrfqBPvOv9gN95nfpBzCNAvwgCfEmu1xFJFUOsfiabxT8y6X6+KjKAaMbCNAtLa62ZleKas8+MdSiqDBNM6I8MNKOVH3mgQ2YOhhJVlJn/TRv+mAdpg3GkJbUKT/x2wflMAkwksQkcPQe0+9FUyPNTOrU95mZNNs/E6dUVI7EsvReuVPGylmhFiq3eY7OoxcFqYN0NcI2hhViI3v+gOq7uy7upfEY0g5bttFZPNbwevjufGfe4DvusHxHD8CvPZ4BQ91F8g1vue/Oc1zoOcU6PxTP0d+tXPuSRjfUYUqv4VX9f/CcyzwANawdw0rqgs3CHf6uY8BvB8bxURJIAFg9homQ9HtYsIcyDUH4B1bQiyciNNVallUWy28+8+rll7PW818=</diagram></mxfile>

However, the string on the right below is not a trace of the pomset on the left because id_{U} is not monotone: the order of "cut veggies" and "fry veggies" has been inverted.

<mxfile host="embed.diagrams.net" modified="2023-04-26T18:26:00.626Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:109.0) Gecko/20100101 Firefox/112.0" etag="vWPba4JyLrxj1mpVWjHP" version="21.2.2" type="embed"><diagram id="oQDAGaKUVMW4XbmnUEji" name="Page-1">5Vpdc6IwFP01vnaEGMDHarvdl53pTB92+5iFC2SKxAlRcX/9BgkKiU7VIkV9UXII+TjnBG4uDNB0lr9wMo9/sQCSgT0M8gF6Gti2ZY1H8q9A1iXiuqgEIk4DVWkHvNF/oMChQhc0gKxRUTCWCDpvgj5LU/BFAyOcs1WzWsiSZq9zEoEBvPkkMdHfNBBxiXp4uMN/Ao3iqmdrqM7MSFVZAVlMAraqQeh5gKacMVEezfIpJAV5FS/ldT8OnN0OjEMqjrnALi9YkmSh5iYWPJUIK34ywZagBirW1ewF5LLtSSxmiQQseZgJzj5gyhLGJZKyVNachDRJNIgkNEpl0ZejA4lPlsAFlbw+qhMzGgRFN5NVTAW8zYlf9LmSLpIYZ4s0gGLgQ1kyZ6omX7QJeQ1SM38BNgPB17JKddZRKigbjjxVXu1ErarENT2RwoiyUbRtece0PFBk7yceGcT/5UA+JARRlN0u565Gud0d5SODcn8hNoOPIgo3zLmt+7xD0rFBergZ2l253B53R7hzgPC7c3mXpLsHH6NheH/PUatD5j2DeYNnSIPHIugrCEtIllG/yfqRfEDQCApNNmqzxXtmW2EcEiLoshlK7qNA9fDKaCpqNrebZOOhxmLGFtwHdVU99NMb0h/FWGtIEB6BMBraKLKd9lEijdsWSWrD13+KwgOuiu+q5qbwlNdrPq0/E7ecayM064neRpA6PldvS2todDG9q56uRHDcL8GHB6K1UwW3cLMh5F5OcOuqBHd6Jfg2UPmq4GjUneBm4qA9we32FXd7pbi+xO1z7+n6ErcveE83MxbtKe457imSb0qvwKkcfxH/XqsP9JV/tg/0lX9JH5hpFMMHWUzmxWGYQK4MMTnNGxX/8la9uVTlgPEVBOhIi6uRc6aoI+eThloU1UzT3FEeGGtbqi7zwJaZOvhaVnJgo78eLjZzTeolHno++H7/+UdWh/ybCYR7SFDqlG/57YJyMx3wtRTlLVje7Y7/qus7zVbq1HeZrbTb3yfnVNS2ybL0Xjuzi5+LQiN8bnNvXUY0ClKb63rUXa34nkRoeDR+wM0nvi7usTGaowXeF0yi7nllfHPecfd4x+uVdxx9y3ZudO/oT2B979eic47Ysl27czzTORXBPXEO1t+3nPviRm/ogmm+Pa/vv8E5xzkA77l39CvRi7Vs3XafebID9IasiznAMr8nuI8PlYykAOowTDRJv6Ib9qEt2OFN20G5tIWrrW73WxezEUQa9+FzQwHUWhApi7tvScvquy9y0fN/</diagram></mxfile>

Constructions

The following constructions are adapted from the work of Kappé et al.

Given two programs P and Q, 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.

Concurrent Composition

Given two programs P and Q, we can compose them concurrently, yielding a new program P \parallel Q that allows any arbitrary interleaving of the two programs. When viewed as a pomset, P \parallel Q ought to have the following properties:

contains all of P,
contains all of Q, and
imposes no additional ordering.
We define P \parallel Q to be the pomset (U, \leq, L, \lambda), where U = U_{P} \uplus U_{Q}, and L = L_{P} \uplus L_{Q}. The partial order is given by

u \leq v \iff
  \begin{cases}
    u \leq_{P} v & \text{if } u, v \in U_{P}\\
    u \leq_{Q} v & \text{if } u, v \in U_{Q}
  \end{cases}

This pomset contains all the events in P, all the events in Q, and all the order contraints imposed by P and Q but nothing else.

The label assignment is given by

  \lambda(u) =
  \begin{cases}
    \textsf{inl } \lambda_{P}(u) & \text{if } u \in U_{P}\\
    \textsf{inr } \lambda_{Q}(u) & \text{o.w.}
  \end{cases}

For example,

<mxfile host="embed.diagrams.net" modified="2023-04-26T19:29:35.975Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:109.0) Gecko/20100101 Firefox/112.0" etag="q8xwjIAhn4fJxu6DT7Gu" version="21.2.2" type="embed"><diagram id="oQDAGaKUVMW4XbmnUEji" name="Page-1">7VxLj5swEP41ObYCzCvH3eyjl0orbdXHkQaHWEtwapxXf30NmCSMkzZB4CXQSxIPZrC/b8Yez6CM0GSxfWbBcv6ZhjgeWUa4HaGHkWWZ5tgWX5lkV0g8DxWCiJFQdjoIXslvLIWGlK5IiNNKR05pzMmyKpzSJMFTXpEFjNFNtduMxtWnLoMIK4LXaRCr0m8k5PNC6jvGQf4Jk2hePtk05JVFUHaWgnQehHRzJEKPIzRhlPLi12I7wXEGXolLcd/Tmav7gTGc8EtusIob1kG8knPjK5YICc0+Uk7XWA6U78rZc7wVuu/nfBELgSl+ppzRNzyhMWVCktBE9LyfkTgGoiAmUSKaUzE6LOT3a8w4EbjeyQsLEobZY+43c8Lx6zKYZs/cCCsSMkZXSYizgRuipc5UTj7TibdHIjnzZ0wXmLOd6LI3RMmCNEPbl+3NgVRXiuZHfCIpC6QZRXvNB6TFDwn2aeCRAvxPhoM3IcJRlPYXcwtAbumD3FYgn654PvgoIrjPmEM71wi6o4A+y4c2KCu3xvoAd88APjgr1wm6d3Ybnc2Gt4+aGpH3FeQVnHES3mVBXwZYHKQpmVZRvxAPHFaCQhWNo9k6J2ZbyhiOA07W1VDyFATyCS+UJPwIbK8KtmMAFFO6YlMs7zoO/YAiZSt2gCIesAhzRVHOyH7aF5E0bpokwQ3bfc8aH52y+UP2zBsP2+OeD7t/kVvMtRKadYVvuHmPa/JtukCR3Rrf5ZBvhHCnU4Q7Z4K1q/k2qoqQ1x7f5k3x7XaKb8tuiPB9wKOBcDVv0BzhVvOMe51iHHi4VXtFBx5utbiiq/mK5gj3Xe8axvPWC2ZEjD+Lfm/VDKDj17YD6Pht2oGaRPmbHcjzys0G2wgGX3WDbagItRdsm2rKpdcUwWNMbYosfRSpSZrjtPuXrwphvckVoLFTpatcqzTkCszzaZrs424yHNgtjaUOs/EcTeOng46sZXZZoyidA8J/6VoGFSGoqMG17FRyx40zt5nRfEwHmt1fK1pe+JDmZd070cE2ltucnfK6+BXl3/lNcSF6KtTJK7311L1nlvk9V5+nIjW6G1A5eA+hRH5sakReDdqGUQ82wSFo/xKFDtDVMGwgFWGE3hF1NQobQkkYGrqnsQiP1AhsIEVhaOhaUVcjoyFVheF26up81afxAtRZQDpydIA5wHHdowOCG7IPFDV3dLBvq2yEulUnVMLV2nUjcOLw26sb2dZtMd6tggF89cOHGcq6r374MGfaIONtFo5aYNzvFOPIbYhx29TH+HUlonevDZdhWkcoh07u1V7WgZO7LS7r15WcOlod7pghQN+vbQjQ99s0hOEWtmyvWmHxNeZt7eEWtiDsnqER9v+FrQvXMseo1qNqxzFQkddekd5W0zckifvrSSbIIOjM15QsDgZr48zergNrNevSa6xhekMr1mq+o9dYQ7vWWVdy1ExDr7GGGV+tWKtn/F5jDfdGna8GOOrhmiSsv1jb1vtF9I56fh0U1i0eWkXz8LcWRTh++HMQ9PgH</diagram></mxfile>

Sequential Composition

Given two programs P and Q, the sequential composition P;Q is simply a program that executes P first and then executes Q. Thus, when viewed as a pomset, P;Q ought to satisfy:

contains all of P,
contains all of Q,
all events in P precedes all events in Q, and
imposes no other additional ordering.
The definition of P;Q is identical to that of P \parallel Q except that we need to augment the partial order as follows:

u \leq v \iff
  \begin{cases}
    u \leq_{P} v & \text{if } u, v \in U_{P}\\
    u \leq_{Q} v & \text{if } u, v \in U_{Q}\\
    u \in P \text{ and } v \in Q
  \end{cases}

P;Q contains all the events in P, all the events in Q, all the order contraints imposed by P and Q, and new order contraints requiring events in P to precede those in Q but nothing else. For example,

<mxfile host="embed.diagrams.net" modified="2023-04-26T19:31:01.324Z" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:109.0) Gecko/20100101 Firefox/112.0" etag="wAUricgpZAZdOw9GSQbn" version="21.2.2" type="embed"><diagram id="oQDAGaKUVMW4XbmnUEji" name="Page-1">7Vxbk6I4FP41Ps4WEAL62NpzeZmqqeqp2Z1HViKmBokTYqv76zdAonCitbYFaYR9UXISQvJ9J8m5oBO02Bw+82i7/spikk48Jz5M0PPE81x35suvQnKsJGGIKkHCaawanQUv9B+ihI6S7mhM8kZDwVgq6LYpXLIsI0vRkEWcs32z2Yqlzaduo4QYgpdllJrSP2ks1pV0ip2z/AuhyVo/2XVUzSbSjZUgX0cx29dE6OMELThjorraHBYkLcDTuFT3fbpSexoYJ5m45QavuuE1SndqbmLHMylhxUcu2CtRAxVHPXtBDrLv+VpsUilw5WUuOPtFFixlXEoylsmW8xVNUyCKUppksriUoyNSPn8lXFCJ65Oq2NA4Lh4z36+pIC/baFk8cy+1SMo422UxKQbuyJI5UzX5ok9yqInUzD8TtiGCH2WTkyIqFpQa+lNV3p9JDZRoXeMTKVmk1Cg59XxGWl4osC8Djwzg/+Yk+iVFJEny4WLuAcg9e5D7BuTLnSgHnySUDBlzqOcWQccG6KtyaKPScm9mD/DgCuCj03KboIdXj9HVanznqGsR+amBvIEzyeKnwugrAEujPKfLJuo34kHihlFoolGbLb4wWy3jJI0EfW2akpcgUE/4xmgmamCHTbCxA1DM2Y4vibqrbvqBjoyjGIOORMQTIoyOSkZO076JpFnbJElu+PGvovAH1sWfqmVZeD7UWz4f/4vcaq4N06wvfMPDe3Yn324AOvI741sP+UEIx70iHF8x1t7Mt9PsCIXd8e0+FN9Br/j2/JYIPxk8Fgg34wbtEe61z3jYK8bBCvfu3tHBCvc63NHNeEV7hE+D8C2Ml6VvhFM5/sL6fVQ1gAv/bj2AC79LPTDdy3rA8PsPQysG4+WgGW7u0xplC16Oe93BLD6eFuOB3bMYpHVb9y5bt2t6spf5OrqqFweE/9a9DHaEYEct7mWX3NIgLZbNipVjOtMc/N4xXfEhLxNST7KB72wPJTu6Xl4l5Xd5U1qJPlXdqZrBrtTTytSRicDeSkVmcH9EiSwELAnXRRahN0P8I0llATvedUKLqJuG2EiyWT5Udquwm4bYKPJZQNVnFm1fZBphI8loQU23irppHI0ppQVP1KlF6PWjxpPT8h1ov8Bc1M3uAzyTXZgea89/8B8r6o36leYwbVYYtbqVczSDBgEMpLXIufdYnPcs4jm9Zrq9mXMEe4JZkxY57zL23QHn015x7odtcY49i5yb8YT2OO8gwaXNtZ6QDhf67O69HazzaYdbuxnHaI9yaymunikCXP13KwJc/F0qwnhzXNhpJltCrQY23J7x5rgg7NjiC5T+/zmuG/cyjJqpqfDuvQx0FHSXr/fNMA7N0uGuJAQiCTbjNlrNxoI1fOHeZngSm7GXQWMNYxxWsTZjHoPGGuq11QQTNoMNgwbbCP1aBdv08gcNNjwdrb4ngE3/mmZ8uGD7+P2Memy6sMPG2n8/vxWbfmuLr5HNH/E1MoO4C/Re36TA8YtsHghd/lLtbWFfcqCi5kTL0s9azfmmotD0oIG7fHFpVa6qti0rWT2MWMXA3s3T1j/r1Nbuvb9xDEBgZdpaxkAWz//SUTU//9cJ+vgv</diagram></mxfile>

Pomsets in the Literature

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 A and B, exhibiting traces abc and def, respectively. To represent the concurrent composition of A and B in the trace model we need to construct a set of all interleaving of abc and def, 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.

Gischer's work investigates the algebraic properties of pomsets and shows that the equational theory is not finitely axiomatizable when certain operations are added.
Cattani's PhD thesis. Traditional models of concurrency, such as pomsets, can be embedded in the presheaf model. A contribution of this work shows how to use the presheaf model to deduce some properties of the traditional models.
Kappé et al. generalizes a language (a set of strings) to a pomset language (a set of pomsets) as a denotational model of series-rational expressions. Additionally, they introduce an operational model and make a step towards a Concurrent Kleene Algebra version of the Kleene's theorem, bridging the gap between denotational and operational models.
Recently (as of 2023), Edixhoven et al. extended pomsets to compactly represent nondeterministic choice.

References

The definitions are adapted from Plotkin's work.
For a syntactic treatment of pomsets, read Kappé et al. and Gischer's work.

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}
}

Pomsets have been extended to represent nondeterministic choice.

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}
}

Cattani's PhD thesis.

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}
}