The Combinatorics of Barrier Synchronization

TL;DR

This paper explores the combinatorial aspects of barrier synchronization, providing formulas and algorithms for counting and randomly generating process executions without explicit state-space construction.

Contribution

It introduces a systematic combinatorial approach and efficient algorithms for counting and sampling process executions in barrier synchronization.

Findings

Developed a symbolic integral formula for counting executions

Created a generic algorithm for uniform random sampling

Proposed efficient algorithms for specific process subclasses

Abstract

In this paper we study the notion of synchronization from the point of view of combinatorics. As a first step, we address the quantitative problem of counting the number of executions of simple processes interacting with synchronization barriers. We elaborate a systematic decomposition of processes that produces a symbolic integral formula to solve the problem. Based on this procedure, we develop a generic algorithm to generate process executions uniformly at random. For some interesting sub-classes of processes we propose very efficient counting and random sampling algorithms. All these algorithms have one important characteristic in common: they work on the control graph of processes and thus do not require the explicit construction of the state-space.

Tables

Table 1. Table 1. A proof system for fork-join processes.

$\begin{array}{c}\\ \overline{\sigma {⊢}_{FJ}0}\end{array}$

$\begin{array}{c}\sigma {⊢}_{FJ}P\\ \overline{\sigma {⊢}_{FJ}\alpha .P}\end{array}$

$\begin{array}{c}\sigma {⊢}_{FJ}P\hspace{1em}\sigma {⊢}_{FJ}Q\\ \overline{\sigma {⊢}_{FJ}P\parallel Q}\end{array}$

$\begin{array}{c}B::\sigma {⊢}_{FJ}P\\ \overline{\sigma {⊢}_{FJ}\nu \left(B\right)P}\end{array}$

$\begin{array}{c}\sigma {⊢}_{FJ}P\\ \overline{B::\sigma {⊢}_{FJ}⟨B⟩.P}\end{array}$

Table 2. Table 2. A proof system for promises.

$\begin{array}{c}\\ \overline{\varnothing {⊢}_{ctrl}0}\end{array}$

$\begin{array}{c}\pi {⊢}_{ctrl}P\\ \overline{\pi {⊢}_{ctrl}\alpha .P}\end{array}$

$\begin{array}{c}\pi {⊢}_{ctrl}P\\ \overline{\pi \cup \left\{B\right\}{⊢}_{ctrl}⟨B⟩.P}\end{array}$

$\begin{array}{c}B\notin \pi \hspace{1em}\pi \cup \left\{B\right\}{⊢}_{ctrl}P\hspace{1em}Q{\uparrow }_B\\ \overline{\pi {⊢}_{ctrl}\nu \left(B\right)(P\parallel Q)}\end{array}$

Table 3. Table 3. Summary of counting and uniform random sampling algorithms (time complexity figures with n 𝑛 n : number of atomic actions).

Algorithm	Class	Count.	Unif. Rand. Gen.	Reference
FJ	Fork-join	$O\left(n\right)$	$O\left(n\cdot \sqrt{n}\right)$ on average	[6]
Arch	Arch-processes	$O\left(n^2\right)$	$O\left(n^4\right)$ worst case	[7]/Theorem 19
bit	BIT-decomposable	?	?	Theorem 10
cftp666The cftp algorithm is the only one we did not design, but only implement. Its complexity is $O\left(n^3\cdot logn\right)$ (randomized) expected time.	All processes	–	$O\left(n^3\cdot logn\right)$ expected	[14]

Table 4. Table 4. Benchmark results for BIT-decomposable classes: FJ and Arch.

FJ size	$♯ℒℰ$	FJ gen	(count)	bit gen	(count)	cftp gen
10	19	0.00001 s	(0.0002 s)	0.0006 s	(0.03 s)	0.04 s
30	${10}^9$	0.00002 s	(0.0002 s)	0.02 s	(0.03 s)	1.8 s
40	$6\cdot {10}^6$	0.00004 s	(0.0003 s)	3.5 s	(5.2 s)	5.6 s
63	$4\cdot {10}^{29}$	0.0005 s	(0.03 s)	Mem. crash	(Crash)	55 s
217028	$2\cdot {10}^{292431}$	8.11 s	(3.34 s)	Mem. crash	(Crash)	Timeout

Equations

$$\nu (B)\left[{\mathsf{a}}_1.⟨B⟩{\mathsf{a}}_2.0\parallel ⟨B⟩{\mathsf{b}}_1.0\parallel {\mathsf{c}}_1.⟨B⟩0\right]$$

$$\nu (B)\left[⟨B⟩{\mathsf{a}}_2.0\parallel ⟨B⟩{\mathsf{b}}_1.0\parallel ⟨B⟩0\right]$$

$$P_{\alpha }=⟨B_{\alpha }⟩\alpha .\left[⟨B_{{\beta }_1}⟩0\parallel \dots \parallel ⟨B_{{\beta }_k}⟩0\right].$$

$$\Psi$$

$$\left(\text{mathbbm}{1}_{\mid x_4\prec x_3}\cdot {\int }_{x_1=0}^{x_2}1\cdot \mathrm{d}{x}_1+\text{mathbbm}{1}_{\mid x_3\prec x_4}\cdot {\int }_{x_1=0}^{x_2}1\cdot \mathrm{d}{x}_1\right)\mathrm{d}{x}_7\mathrm{d}{x}_5\mathrm{d}{x}_8\mathrm{d}{x}_6\mathrm{d}{x}_3\mathrm{d}{x}_4\mathrm{d}{x}_2=\frac{8+6}{8!}.$$

$$C_p=\bigcap _{x_i\prec x_j\in P}{S}_{i,j}\cap C$$

$$V={\int }_{[0,1{]}^n}\text{mathbbm}{1}_P(\mathbf{x})\mathrm{d}\mathbf{x}={\int }_{[0,1]}\cdots {\int }_{[0,1]}\text{mathbbm}{1}_P((x,y,z,\dots ))\mathrm{d}x\mathrm{d}y\mathrm{d}z\dots ,$$

$${\int }_a^b\underset{f(y_i)}{\underbrace{\left(\int \cdots \int 1\mathrm{d}{y}_n\cdots \mathrm{d}{y}_{i+1}\right)}}\mathrm{d}{y}_i.$$

$${\int }_0^1\left({\int }_{x_2}^1{\int }_{x_4}^1{\int }_{x_3}^1{\int }_{x_6}^1{\int }_{x_4}^{x_8}{\int }_{x_3}^{x_8}{\int }_0^{x_2}\mathrm{d}{x}_1\mathrm{d}{x}_5\mathrm{d}{x}_7\mathrm{d}{x}_8\mathrm{d}{x}_6\mathrm{d}{x}_3\mathrm{d}{x}_4\right)\mathrm{d}{x}_2=\frac{8}{8!}.$$

$$\left\{\begin{array}[]{lllllll}X_{1}=0.064\dots,&&X_{2}=0.081\dots,&&X_{3}=0.541\dots,&&X_{4}=0.323\dots,\\ X_{5}=0.770\dots,&&X_{6}=0.625\dots,&&X_{7}=0.582\dots,&&X_{8}=0.892\dots\\ \end{array}\right.$$

$$(x_1,x_2,x_4,x_3,x_7,x_6,x_5,x_8).$$

$$T::=0\mid \alpha .(T\parallel T)\text{or e.g.}T::=0\mid \nu B\left(\alpha .⟨B⟩0\parallel ⟨B⟩T\parallel ⟨B⟩T\right)$$

Full text

1. Introduction

The objective of our (rather long-term) research project is to study the combinatorics of concurrent processes. Because the mathematical toolbox of combinatorics imposes strong constraints on what can be modeled, we study process calculi with a very restricted focus. For example in  [5] the processes we study can only perform atomic actions and fork child processes, and in [4] we enrich this primitive language with non-determinism. In the present paper, our objective is to isolate another fundamental “feature” of concurrent processes: synchronization. For this, we introduce a simple process calculus whose only non-trivial concurrency feature is a principle of barrier synchronization. This is here understood intuitively as the single point of control where multiple processes have to “meet” before continuing. This is one of the important building blocks for concurrent and parallel systems [13].

Combinatorics is about “counting things”, and what we propose to count in our study is the number of executions of processes wrt. their “syntactic size”. This is a symptom of the so-called “combinatorial explosion”, a defining characteristic of concurrency. As a first step, we show that counting executions of concurrent processes is a difficult problem, even in the case of our calculus with limited expressivity. Thus, one important goal of our study is to investigate interesting sub-classes for which the problem becomes “less difficult”. To that end, we elaborate in this paper a systematic decomposition of arbitrary processes, based on only four rules: (B)ottom, (I)ntermediate, (T)op and (S)plit. Each rule explains how to “remove” one node from the control graph of a process while taking into account its contribution in the number of possible executions. Indeed, one main feature of this BITS-decomposition is that it produces a symbolic integral formula to solve the counting problem. Based on this procedure, we develop a generic algorithm to generate process executions uniformly at random. Since the algorithm is working on the control graph of processes, it provides a way to statistically analyze processes without constructing their state-space explicitly. In the worst case, the algorithm cannot of course overcome the hardness of the problem it solves. However, depending on the rules allowed during the decomposition, and also on the strategy adopted, one can isolate interesting sub-classes wrt. the counting and random sampling problem. We identify well-known “structural” sub-classes such as fork-join parallelism [11] and asynchronous processes with promises [15]. For some of these sub-classes we develop dedicated and efficient counting and random sampling algorithms. A large sub-class that we find particularly interesting is what we call the “BIT-decomposable” processes, i.e. only allowing the three rules (B), (I) and (T) in the decomposition. The counting formula we obtain for such processes is of a linear size (in the number of atomic actions in the processes, or equivalently in the number of vertices in their control graph). We also discuss informally the typical shape of “BIT-free” processes.

The outline of the paper is as follows. In Section 2 we introduce a minimalist calculus of barrier synchronization. We show that the control graphs of processes expressed in this language are isomorphic to arbitrary partially ordered sets (Posets) of atomic actions. From this we deduce our rather “negative” starting point: counting executions in this simple language is intractable in the general case. In Section 3 we define the BITS-decomposition, and we use it in Section 4 to design a generic uniform random sampler. In Section 5 we discuss various sub-classes of processes related to the proposed decomposition, and for some of them we explain how the counting and random sampling problem can be solved efficiently. In Section 6 we propose an experimental study of the algorithm toolbox discussed in the paper.

Note that some technical complement and proof details are deferred to an external “companion” document. Moreover we provide the full source code developed in the realm of this work, as well as the benchmark scripts. All these complement informations are available online222cf. https://gitlab.com/ParComb/combinatorics-barrier-synchro.git.

Related work

Our study intermixes viewpoints from concurrency theory, order-theory as well as combinatorics (especially enumerative combinatorics and random sampling). The heaps combinatorics (studied in e.g. [1]) provides a complementary interpretation of concurrent systems. One major difference is that this concerns “true concurrent” processes based on the trace monoid, while we rely on the alternative interleaving semantics. A related uniform random sampler for networks of automata is presented in [3]. Synchronization is interpreted on words using a notion of “shared letters”. This is very different from the “structural” interpretation as joins in the control graph of processes. For the generation procedure [1] requires the construction of a “product automaton”, whose size grows exponentially in the number of “parallel” automata. By comparison, all the algorithms we develop are based on the control graph, i.e. the space requirement remains polynomial (unlike, of course, the time complexity in some cases). Thus, we can interpret this as a space-time trade-of between the two approaches. A related approach is that of investigating the combinatorics of lassos, which is connected to the observation of state spaces through linear temporal properties. A uniform random sampler for lassos is proposed in [16]. The generation procedure takes place within the constructed state-space, whereas the techniques we develop do not require this explicit construction. However lassos represent infinite runs whereas for now we only handle finite (or finite prefixes) of executions.

A coupling from the past (CFTP) procedure for the uniform random generation of linear extensions is described, with relatively sparse details, in [14]. The approach we propose, based on the continuous embedding of Posets into the hypercube, is quite complementary. A similar idea is used in [2] for the enumeration of Young tableaux using what is there called the density method. The paper [12] advocates the uniform random generation of executions as an important building block for statistical model-checking. A similar discussion is proposed in [18] for random testing. The leitmotiv in both cases is that generating execution paths without any bias is difficult. Hence a uniform random sampler is very likely to produce interesting and complementary tests, if comparing to other test generation strategies.

Our work can also be seen as a continuation of the algorithm and order studies [17] orchestrated by Ivan Rival in late 1980’s only with powerful new tools available in the modern combinatorics toolbox.

2. Barrier synchronization processes

The starting point of our study is the small process calculus described below.

Definition 1** (Syntax of barrier synchronization processes).**

We consider countably infinite sets $\mathcal{A}$ of (abstract) atomic actions, and $\mathcal{B}$ of barrier names. The set $\mathcal{P}$ of processes is defined by the following grammar:

[TABLE]

The language has very few constructors and is purposely of limited expressivity. Processes in this language can only perform atomic actions, fork child processes and interact using a basic principle of synchronization barrier. A very basic process is the following one:

[TABLE]

This process can initially perform the actions $\mathsf{a_{1}}$ and $\mathsf{c_{1}}$ in an arbitrary order. We then reach the state in which all the processes agrees to synchronize on $B$:

[TABLE]

The possible next transitions are: $\xrightarrow{\mathsf{a_{2}}}\mathsf{b_{1}}.0\xrightarrow{\mathsf{b_{1}}}0,~{}\text{alternatively}\xrightarrow{\mathsf{b_{1}}}\mathsf{a_{2}}.0\xrightarrow{\mathsf{a_{2}}}0$

In the resulting states, the barrier $B$ has been “consumed”.

The operational semantics below characterize processes transitions of the form $P\xrightarrow{\alpha}P^{\prime}$ in which $P$ can perform action $\alpha$ to reach its (direct) derivative $P^{\prime}$.

Definition 2** (Operational semantics).**

[TABLE]

with: \begin{array}[]{ll}\left[\begin{array}[]{l}{\scriptstyle\small{\textsf{sync}}_{B}(0)=0}\\ {\scriptstyle\small{\textsf{sync}}_{B}(\alpha.P)=\alpha.P}\\ {\scriptstyle\small{\textsf{sync}}_{B}(P\parallel Q)=\small{\textsf{sync}}_{B}(P)\parallel\small{\textsf{sync}}_{B}(Q)}\\ {\scriptstyle\small{\textsf{sync}}_{B}(\nu(B)P)=\nu(B)P}\\ {\scriptstyle\forall C\neq B,~{}\small{\textsf{sync}}_{B}(\nu(C)P)=\nu(C)~{}\small{\textsf{sync}}_{B}(P)}\\ {\scriptstyle\small{\textsf{sync}}_{B}(\langle B\rangle P)=P}\\ {\scriptstyle\forall C\neq B,~{}\small{\textsf{sync}}_{B}(\langle C\rangle P)=\langle C\rangle P}\end{array}\right.&\left[\begin{array}[]{l}{\scriptstyle\small{\textsf{wait}}_{B}(0)=\small{\textsf{false}}}\\ {\scriptstyle\small{\textsf{wait}}_{B}(\alpha.P)=\small{\textsf{wait}}_{B}(P)}\\ {\scriptstyle\small{\textsf{wait}}_{B}(P\parallel Q)=\small{\textsf{wait}}_{B}(P)\lor\small{\textsf{wait}}_{B}(Q)}\\ {\scriptstyle\small{\textsf{wait}}_{B}(\nu(B)P)=\small{\textsf{false}}}\\ {\scriptstyle\forall C\neq B,~{}\small{\textsf{wait}}_{B}(\nu(C)P)=\small{\textsf{wait}}_{B}(P)}\\ {\scriptstyle\small{\textsf{wait}}_{B}(\langle B\rangle P)=\small{\textsf{true}}}\\ {\scriptstyle\forall C\neq B,~{}\small{\textsf{wait}}_{B}(\langle C\rangle P)=\small{\textsf{wait}}_{B}(P)}\\ \end{array}\right.\end{array}

The rule (sync) above explains the synchronization semantics for a given barrier $B$. The rule is non-trivial given the broadcast semantics of barrier synchronization. The definition is based on two auxiliary functions. First, the function $\small{\textsf{sync}}_{B}(P)$ produces a derivative process $Q$ in which all the possible synchronizations on barrier $B$ in $P$ have been effected. If $Q$ has a sub-process that cannot yet synchronize on $B$, then the predicate $\small{\textsf{wait}}_{B}(Q)$ is true and the synchronization on $B$ is said incomplete. In this case the rule (sync) does not apply, however the transitions within $P$ can still happen through (lift).

2.1. The control graph of a process

We now define the notion of a (finite) execution of a process.

Definition 3** (execution).**

An execution $\sigma$ of $P$ is a finite sequence $\langle\alpha_{1},\ldots,\alpha_{n}\rangle$ such that there exist a set of processes $P^{\prime}_{\alpha_{1}},\ldots,P^{\prime}_{\alpha_{n}}$ and a path $P\xrightarrow{\alpha_{1}}P^{\prime}_{\alpha_{1}}\ldots\xrightarrow{\alpha_{n}}P^{\prime}_{\alpha_{n}}$ with $P^{\prime}_{\alpha_{n}}\nrightarrow$ (no transition is possible from $P^{\prime}_{\alpha_{n}}$).

We assume that the occurrences of the atomic actions in a process expression have all distinct labels, $\alpha_{1},\ldots,\alpha_{n}$. This is allowed since the actions are uninterpreted in the semantics (cf. Definition 2). Thus, each action $\alpha$ in an execution $\sigma$ can be associated to a unique position, which we denote by $\sigma(\alpha)$. For example if $\sigma=\langle\alpha_{1},\ldots,\alpha_{k},\ldots,\alpha_{n}\rangle$, then $\sigma(\alpha_{k})=k$.

The behavior of a process can be abstracted by considering the causal ordering relation wrt. its atomic actions.

Definition 4** (cause, direct cause).**

Let $P$ be a process. An action $\alpha$ of $P$ is said a cause of another action $\beta$, denoted by $\alpha<\beta$, iff for any execution $\sigma$ of $P$ we have $\sigma(\alpha)<\sigma(\beta)$. Moreover, $\alpha$ is a direct cause of $\beta$, denoted by $\alpha\prec\beta$ iff $\alpha<\beta$ and there is no $\gamma$ such that $\alpha<\gamma<\beta$. The relation $<$ obtained from $P$ is denoted by ${\mathscr{P}\!\mathscr{O}}(P)$.

Obviously ${\mathscr{P}\!\mathscr{O}}(P)$ is a partially ordered set (poset) with covering $\prec$, capturing the causal ordering of the actions of $P$. The covering of a partial order is by construction an intransitive directed acyclic graph (DAG), hence the description of ${\mathscr{P}\!\mathscr{O}}(P)$ itself is simply the transitive closure of the covering, yielding $O(n^{2})$ edges over $n$ elements. The worst case (maximizing the number of edges) is a complete bipartite graph with two sets of $2n$ vertices connected by $n^{2}$ edges (cf. Fig. 1).

For most practical concerns we will only consider the covering, i.e. the intransitive DAG obtained by the transitive reduction of the order. It is possible to direclty construct this control graph, according to the following definition.

Definition 5** (Construction of control graphs).**

Let $P$ be a process term. Its control graph is $\small{\textsf{ctg}}(P)=\langle V,E\rangle$, constructed inductively as follows:

\left[\begin{array}[]{l|l}\small{\textsf{ctg}}(0)=\langle\emptyset,\emptyset\rangle&\phantom{i}\small{\textsf{ctg}}(\nu(B)P)=\bigotimes_{\langle B\rangle}\small{\textsf{ctg}}(P)\\[2.0pt] \begin{array}[]{l}\small{\textsf{ctg}}(\alpha.P)=\alpha\leadsto\small{\textsf{ctg}}(P)\\ \small{\textsf{ctg}}(\langle B\rangle P)=\langle B\rangle\leadsto\small{\textsf{ctg}}(P)\phantom{i}\end{array}&\phantom{i}\begin{array}[t]{l}\small{\textsf{ctg}}(P\parallel Q)=\small{\textsf{ctg}}(P)\cup\small{\textsf{ctg}}(Q)\\ \text{ with }\langle V_{1},E_{1}\rangle\cup\langle V_{2},E_{2}\rangle=\langle V_{1}\cup V_{2},E_{1}\cup E_{2}\rangle\end{array}\\[2.0pt] \end{array}\right.

with \left\{\begin{array}[]{l}x\leadsto\langle V,E\rangle=\langle V\cup\{x\},\{(x,y)\mid y\in\small{\textsf{srcs}}(E)\lor(E=\emptyset\land y\in V)\}\rangle\\ \small{\textsf{srcs}}(E)=\{y\mid(y,z)\in E\land\nexists x,~{}(x,y)\in E\}\\ \bigotimes_{\langle B\rangle}\langle V,E\rangle=\langle V\setminus\{\langle B\rangle\},E\setminus\begin{array}[t]{l}\{(x,y)\mid x\neq y\land(x=\langle B\rangle\lor y=\langle B)\rangle\}\\ \cup~{}\{(\alpha,\beta)\mid\{(\alpha,\langle B\rangle),~{}(\langle B\rangle,\beta)\}\subseteq E\}\rangle\end{array}\end{array}\right.

Given a control graph $\Gamma$, the notation $x\leadsto\Gamma$ corresponds to prefixing the graph by a single atomic action. The set $\small{\textsf{srcs}}(E)$ corresponds to the sources of the edges in $E$, i.e. the vertices without an incoming edge. And $\bigotimes_{\langle B\rangle}\Gamma$ removes an explicit barrier node and connect all the processes ending in $B$ to the processes starting from it. In effect, this realizes the synchronization described by the barrier $B$. We illustrate the construction on a simple process below:

\begin{array}[t]{l}\small{\textsf{ctg}}(\nu(B)\nu(C)[\langle B\rangle\langle C\rangle a.0||\langle B\rangle\langle C\rangle b.0])\\ =\bigotimes_{\langle B\rangle}\bigotimes_{\langle C\rangle}\left(\small{\textsf{ctg}}(\langle B\rangle\langle C\rangle a.0)\cup\small{\textsf{ctg}}(\langle B\rangle\langle C\rangle b.0)\right)\\ =\bigotimes_{\langle B\rangle}\bigotimes_{\langle C\rangle}\begin{array}[t]{l}\langle\{\langle B\rangle,\langle C\rangle,a\},\{(\langle B\rangle,\langle C\rangle),(\langle C\rangle,a)\}\rangle\}\\ \cup\langle\{\langle B\rangle,\langle C\rangle,b\},\{(\langle B\rangle,\langle C\rangle),(\langle C\rangle,b)\}\rangle\end{array}\\ =\bigotimes_{\langle B\rangle}\bigotimes_{\langle C\rangle}\langle\{\langle B\rangle,\langle C\rangle,a,b\},\{(\langle B\rangle,\langle C\rangle),(\langle C\rangle,a),(\langle C\rangle,b)\}\rangle\\ =\bigotimes_{\langle B\rangle}\langle\{\langle B\rangle,a,b\},\{(\langle B\rangle,a),(\langle B\rangle,b)\}\rangle\\ =\langle\{a,b\},\emptyset\rangle\end{array}

The graph with only two unrelated vertices and no edge is the correct construction. Now, slightly changing the process we see how the construction fails for deadlocked processes.

\begin{array}[t]{l}\small{\textsf{ctg}}(P)=\bigotimes_{\langle B\rangle}\bigotimes_{\langle C\rangle}\left(\small{\textsf{ctg}}(\langle B\rangle\langle C\rangle a.0)\cup\small{\textsf{ctg}}(\langle C\rangle\langle B\rangle b.0)\right)\\ =\bigotimes_{\langle B\rangle}\bigotimes_{\langle C\rangle}\begin{array}[t]{l}\langle\{\langle B\rangle,\langle C\rangle,a\},\{(\langle B\rangle,\langle C\rangle),(\langle C\rangle,a)\}\rangle\}\\ \cup\langle\{\langle C\rangle,\langle B\rangle,b\},\{(\langle C\rangle,\langle B\rangle),(\langle B\rangle,b)\}\rangle\end{array}\\ =\bigotimes_{\langle B\rangle}\bigotimes_{\langle C\rangle}\langle\{\langle B\rangle,\langle C\rangle,a,b\},\{(\langle B\rangle,\langle C\rangle),(\langle C\rangle,a),(\langle C\rangle,\langle B\rangle),(\langle B\rangle,b)\}\rangle\\ =\bigotimes_{\langle B\rangle}\langle\{\langle B\rangle,a,b\},\{(\langle B\rangle,\langle B\rangle),(\langle B\rangle,a),(\langle B\rangle,b)\}\rangle\\ =\langle\{a,b\},\{(\langle B\rangle,\langle B\rangle),(\langle B\rangle,a),(\langle B\rangle,b)\}\rangle\end{array}

In the final step, the barrier $\langle B\rangle$ cannot be removed because of the self-loop. So there are two witnesses of the fact that the construction failed: there is still a barrier name in the process, and there is a cycle in the resulting graph.

Theorem 6**.**

Let $P$ be a process, then $P$ has a deadlock iff $\small{\textsf{ctg}}(P)$ has a cycle. Moreover, if $P$ is deadlock-free (hence it is a DAG) then $(\alpha,\beta)\in\small{\textsf{ctg}}(P)$ iff $\alpha\prec\beta$ (hence the DAG is intransitive).

idea.

The proof is not difficult but slightly technical. The idea is to extend the notion of execution to go “past” deadlocks, thus detecting cycles in the causal relation. The details are given in companion document. ∎∎

In Fig. 2 (left) we describe a system $Sys$ written in the proposed language, together with the covering of ${\mathscr{P}\!\mathscr{O}}(Sys)$, i.e. its control graph (right). We also indicate the number of its possible executions, a question we address next.

2.2. The counting problem

One may think that in such a simple setting, any behavioral property, such as the counting problem that interests us, could be analyzed efficiently e.g. by a simple induction on the syntax. However, the devil is well hidden inside the box because of the following fact.

Theorem 7**.**

Let $U$ be a partially ordered set. Then there exists a barrier synchronization process $P$ such that ${\mathscr{P}\!\mathscr{O}}(P)$ is isomorphic to $U$.

Proof.

(sketch). Consider $G$ the (intransitive) covering DAG of a poset $U$. We suppose each vertex of $G$ to be uniquely identified by a label ranging over $\alpha_{1},\alpha_{2},\ldots,\alpha_{n}$. The objective is to associate to each such vertex labeled $\alpha$ a process expression $P_{\alpha}$. The construction is done backwards, starting from the sinks (vertices without outgoing edges) of $G$ and bubbling-up until its sources (vertices without incoming edges).

There is a single rule to apply, considering a vertex labeled $\alpha$ whose children have already been processed, i.e. in a situation depicted as follows:

[TABLE]

In the special case $\alpha$ is a sink we simply define $P_{\alpha}=\langle B_{\alpha}\rangle\alpha.0$. In this construction it is quite obvious that $\alpha\prec\beta_{i}$ for each of the $\beta_{i}$’s, provided the barriers $B_{\alpha},B_{\beta_{1}},\ldots,B_{\beta_{k}}$ are defined somewhere in the outer scope.

At the end we have a set of processes $P_{\alpha_{1}},\ldots,P_{\alpha_{n}}$ associated to the vertices of $G$ and we finally define $P=\nu(B_{\alpha_{1}})\ldots\nu(B_{\alpha_{n}})\left[P_{\alpha_{1}}\parallel\ldots\parallel P_{\alpha_{n}}\right]$.

That ${\mathscr{P}\!\mathscr{O}}(P)$ has the same covering as $U$ is a simple consequence of the construction. ∎∎

Corollary 8**.**

Let $P$ be a non-deadlocked process. Then $\langle\alpha_{1},\ldots,\alpha_{n}\rangle$ is an execution of $P$ if it is a linear extension of ${\mathscr{P}\!\mathscr{O}}(P)$. Consequently, the number of executions of $P$ is equal to the number of linear extensions of ${\mathscr{P}\!\mathscr{O}}(P)$.

We now reach our “negative” result that is the starting point of the rest of the paper: there is no efficient algorithm to count the number of executions, even for such simplistic barrier processes.

Corollary 9**.**

Counting the number of executions of a (non-deadlocked) barrier synchronization process is $\sharp{P}$-complete333A function $f$ is in $\sharp$P if there is a polynomial-time non-deterministic Turing machine $M$ such that for any instance $x$, $f(x)$ is the number of executions of $M$ that accept $x$ as input. See https://en.wikipedia.org/wiki/%E2%99%AFP-complete.

This is a direct consequence of [8] since counting executions of processes boils down to counting linear extensions in (arbitrary) posets.

3. A generic decomposition scheme and its (symbolic) counting algorithm

We describe in this section a generic (and symbolic) solution to the counting problem, based on a systematic decomposition of finite Posets (thus, by Theorem 6, of process expressions) through their covering DAG (i.e. control graphs).

3.1. Decomposition scheme

In Fig. 3 we introduce the four decomposition rules that define the BITS-decomposition. The first three rules are somehow straightforward. The (B)-rule (resp. (T)-rule) allows to consume a node with no outgoing (resp. incoming) edge and one incoming (resp. outgoing) edge. In a way, these two rules consume the “pending” parts of the DAG. The (I)-rule allows to consume a node with exactly one incoming and outgoing edge. The final (S)-rule takes two incomparable nodes $x,y$ and decomposes the DAG in two variants: the one for $x\prec y$ and the one for the converse $y\prec x$.

We now discuss the main interest of the decomposition: the incremental construction of an integral formula that solves the counting problem. The calculation is governed by the equations specified below the rules in Fig. 3, in which the current formula $\Psi$ is updated according to the definition of $\Psi^{\prime}$ in the equations.

Theorem 10**.**

The numerical evaluation of the integral formula built by the BITS-decomposition yields the number of linear extensions of the corresponding Poset. Moreover, the applications of the BITS-rules are confluent, in the sense that all the sequences of (valid) rules reduce the DAG to an empty graph444At the end of the decomposition, the DAG is in fact reduced to a single node, which is removed by an integration between [math] and $1$..

The precise justification of the integral computation and the proof for the theorem above are postponed to Section 3.2 below. We first consider an example.

Example 11**.**

Illustrating the BITS-decomposition scheme.

[TABLE]

The DAG to decompose (on the left) is of size $8$ with nodes $x_{1},\ldots,x_{8}$. The decomposition is non-deterministic, multiple rules apply, e.g. we could “consume” the node $x_{7}$ with the (I) rule. Also, the (S)plit rule is always enabled. In the example, we decide to first remove the node $x_{1}$ by an application of the (T) rule. We then show an application of the (S)plit rule for the incomparable nodes $x_{3}$ and $x_{4}$. The decomposition should then be performed on two distinct DAGs: one for $x_{3}\prec x_{4}$ and the other one for $x_{4}\prec x_{3}$. We illustrate the second choice, and we further eliminate the nodes $x_{7}$ then $x_{5}$ using the (I) rule, etc. Ultimately all the DAGs are decomposed and we obtain the following integral computation:

[TABLE]

The result means that there are exactly 14 distinct linear extensions in the example Poset.

3.2. Embedding in the hypercube: the order polytope

The justification of our decomposition scheme is based on the continuous embedding of posets into the hypercube, as investigated in [19].

Definition 12** (order polytope).**

Let $P=(E,\prec)$ be a poset of size $n$. Let $C$ be the unit hypercube defined by $C=\left\{(x_{1},\dots,x_{n})\in\mathbb{R}^{n}~{}|~{}\forall i,~{}0\leq x_{i}\leq 1\right\}$. For each constraint $x_{i}\prec x_{j}\in P$ we define the convex subset $S_{i,j}=\left\{(x_{1},\dots,x_{n})\in\mathbb{R}^{n}~{}|~{}x_{i}\leq x_{j}\right\}$, i.e. one of the half spaces obtained by cutting $\mathbb{R}^{n}$ with the hyperplane $\left\{(x_{1},\dots,x_{n})\in\mathbb{R}^{n}~{}|~{}x_{i}-x_{j}=0\right\}$. Thus, the order polytope $C_{P}$ of $P$ is:

[TABLE]

Each linear extension, seen as total orders, can similarly be embedded in the unit hypercube. Then, the order polytopes of the linear extensions of a poset $P$ form a partition of the Poset embedding $C_{p}$ as illustrated in Figure 4.

The number of linear extensions of a poset $P$, written $|{\mathscr{L}\!\mathscr{E}}(P)|$, is then characterized as a volume in the embedding.

Theorem 13**.**

*([19, Corollary 4.2])

Let $P$ be a Poset of size $n$ then its number of linear extensions $|{\mathscr{L}\!\mathscr{E}}(P)|=n!\cdot Vol(C_{P})$ where $Vol(C_{P})$ is the volume, defined by the Lebesgue measure, of the order polytope $C_{P}$.*

The integral formula introduced in the BITS-decomposition corresponds to the computation of $Vol(C_{p})$, hence we may now give the key-ideas of Theorem 10.

Theorem 10, sketch.

We begin with the (S)-rule. Applied on two incomparable elements $x$ and $y$, the rule partitions the polytope in two regions: one for $x\prec y$ and the other for $y\prec x$. Obviously, the respective volume of the two disjoint regions must be added.

We focus now on the (I)-rule. In the context of Lebesgue integration, the classic Fubini’s theorem allows to compute the volume $V$ of a polytope $P$ as an iteration on integrals along each dimension, and this in all possible orders, which gives the confluence property. Thus,

[TABLE]

$\mathbbm{1}_{P}$ being the indicator function of $P$ such that $\displaystyle{\mathbbm{1}_{P}((x,y,z,\dots))=\prod_{\alpha\text{ actions}}\mathbbm{1}_{P_{\alpha}}(\alpha),}$ with $P_{\alpha}$ the projection of $P$ on the dimension associated to $\alpha$. By convexity of $P$, the function $\mathbbm{1}_{P_{y}}$ is the indicator function of a segment $[x,z]$. So the following identity holds: $\int_{P}\mathbbm{1}_{P_{y}}(y)\mathrm{d}y=\int_{x}^{z}\mathrm{d}y$. Finally, the two other rules (T) and (B) are just special cases (taking $x=0$, alternatively $z=1$). ∎∎

Corollary 14**.**

(Stanley [19]) The order polytope of a linear extension is a simplex and the simplices of the linear extensions are isometric, thus of the same volume.

4. Uniform random generation of process executions

In this section we describe a generic algorithm for the uniform random generation of executions of barrier synchronization processes. The algorithm is based on the BITS-decomposition and its embedding in the unit hypercube. It has two essential properties. First, it is directly working on the control graphs (equivalently on the corresponding poset), and thus does not require the explicit construction of the state-space of processes. Second, it generates possible executions of processes at random according to the uniform distribution. This is a guarantee that the sampling is not biased and reflects the actual behavior of the processes.

The starting point of Algorithm 1 (cf. previous page) is a Poset over a set of points $\{x_{1},\ldots,x_{n}\}$ (or equivalently its covering DAG). The decomposition scheme of Section 3 produces an integral formula $\mathcal{I}$ of the form $\int^{1}_{0}F(y_{n},\ldots,y_{1})~{}\mathrm{d}y_{n}\cdots\mathrm{d}y_{1}$. with $F$ a symbolic integral formula over the points $x_{1},\ldots,x_{n}$. The $y$ variables represent a permutation of the poset points giving the order followed along the decomposition. Thus, the variable $y_{i}$ corresponds to the $i$-th removed point during the decomposition. We remind the reader that the evaluation of the formula $\mathcal{I}$ gives the number of linear extensions of the partial order. Now, starting with the complete formula, the variables $y_{1},~{}y_{2},\ldots$ will be eliminated, in turn, in an “outside-in” way. Algorithm 1 takes place at the $i$-th step of the process. At this step, the considered formula is of the following form:

[TABLE]

Note that in the subformula $f(y_{i})$ the variable $y_{i}$ may only occur (possibly multiple times) as an integral bound.

In the algorithm, the variable $C$ gets the result of the numerical computation of the integral $\mathcal{I}$ at the given step. Next we draw (with Uniform) a real number $U$ uniformly at random between the integration bounds $a$ and $b$. Based on these two intermediate values, we perform a numerical solving of variable $t$ in the integral formula corresponding to the slice of the polytope along the hyperplan $y_{i}=U$. The result, a real number between $a$ and $b$, is stored in variable $Y_{i}$. The justification of this step is further discussed in the proof sketch of Theorem 15 below.

If there remains integrals in $\mathcal{I}$, the algorithm is applied recursively by substituting the variable $y_{i}$ in the integral bounds of $\mathcal{I}$ by the numerical value $Y_{i}$. If no integral remains, all the computed values $Y_{i}$’s are returned. As illustrated in Example 16 below, this allows to select a specific linear extension in the initial partial ordering. The justification of the algorithm is given by the following theorem.

Theorem 15**.**

Algorithm 1 uniformly samples a point of the order polytope with a $\mathcal{O}(n)$ complexity in the number of integrations.

sketch.

The problem is reduced to the uniform random sampling of a point $p$ in the order polytope. This is a classical problem about marginal densities that can be solved by slicing the polytope and evaluating incrementally the $n$ continuous random variables associated to the coordinates of $p$. More precisely, during the calculation of the volume of the polytope $P$, the last integration (of a monovariate polynomial $p(y)$) done from 0 to 1 corresponds to integrate the slices of $P$ according the last variable $y$. So, the polynomial $p(y)/\int_{0}^{1}p(y)dy$ is nothing but the density function of the random variable $Y$ corresponding to the value of $y$. Thus, we can generate $Y$ according to this density and fix it. When this is done, we can inductively continue with the previous integrations to draw all the random variables associated to the coordinates of $p$. The linear complexity of Algorithm 1 follows from the fact that each partial integration deletes exactly one variable (which corresponds to one node). Of course at each step a possibly costly computation of the counting formula is required. ∎∎

We now illustrate the sampling process based on Example 11 (page 11).

Example 16**.**

First we assume that the whole integral formula has already been computed. To simplify the presentation we only consider (S)plit-free DAGs i.e. decomposable without the (S) rule. Note that it would be easy to deal with the (S)plit rule: it is sufficient to uniformly choose one of the DAG processed by the (S)-rule w.r.t. their number of linear extensions.

Thus we will run the example on the DAG of Example 11 where the DAG corresponding to “$x_{4}\prec x_{3}$” as been randomly chosen (with probability $\frac{8}{14}$) i.e. the following formula holds:

[TABLE]

In the equation above, the sub-formula between parentheses would be denoted by $f(x_{2})$ in the explanation of the algorithm. Now, let us apply the Algorithm 1 to that formula in order to sample a point of the order polytope. In the first step the normalizing constant $C$ is equal to $\frac{8!}{8}$, we draw $U$ uniformly in $[0,1]$ and so we compute a solution of $\frac{8!}{8}\int_{0}^{t}\dots\mathrm{d}x_{2}=U$. That solution corresponds to the second coordinate of a the point we are sampling. And so on, we obtain values for each of the coordinates:

[TABLE]

These points belong to a simplex of the order polytope. To find the corresponding linear extension we compute the rank of that vector i.e. the order induced by the values of the coordinates correspond to a linear extension of the original DAG:

[TABLE]

This is ultimately the linear extension returned by the algorithm.

5. Classes of processes that are BIT-decomposable

(or not)

Thanks to the BITS decomposition scheme, we can generate a counting formula for any (deadlock-free) process expressed in the barrier synchronization calculus, and derive from it a dedicated uniform random sampler. However the (S)plit rule generates two summands, thus if we cannot find common calculations between the summands the resulting formula can grow exponentially in the size of the concerned process. If we avoid splits in the decomposition, then the counting formula remains of linear size. This is, we think, a good indicator that the subclass of so-called “BIT-decomposable” processes is worth investigating for its own sake. In this Section, we first give some illustrations of the expressivity of this subclass, and we then study the question of what it is to be not BIT-decomposable. By lack of space, the discussion in this Section remains rather informal with very rough proof sketches, and more formal developments are left for a future work. Also, the first two subsections are extended results based on previously published papers (respectively [6] and [7]).

5.1. From tree Posets to fork-join parallelism

If the control-graph of a process is decomposed with only the B(ottom) rule (or equivalently the T(op) rule), then it is rather easy to show that its shape is that of a tree. These are processes that cannot do much beyond forking sub-processes. For example, based on our language of barrier synchronization it is very easy to encode e.g. the (rooted) binary trees:

[TABLE]

The good news is that the combinatorics on trees is well-studied. In the paper [4] we provide a thorough study of such processes, and in particular we describe very efficient counting and uniform random generation algorithms. Of course, this is not a very interesting sub-class in terms of concurrency.

Thankfully, many results on trees generalize rather straightforwardly to fork-join parallelism, a sub-class we characterize inductively in Table 1. Informally, this proof system imposes that processes use their synchronization barriers according to a stack discipline. When synchronizing, only the last created barrier is available, which exactly corresponds to the traditional notion of a join in concurrency. Combinatorially, there is a correspondence between these processes and the class of series-parallel Posets. In the decomposition both the (B) and the (I) rule are needed, but following a tree-structured strategy. Most (if not all) the interesting questions about such partial orders can be answered in (low) polynomial time.

Theorem 17** (cf. [6]).**

For a fork join process of size $n$ the counting problem is of time complexity $O(n)$ and we developed a bit-optimal uniform random sampler with time complexity $O(n\sqrt{n})$ on average.

5.2. Asynchronism with promises

We now discuss another interesting sub-class of processes that can also be characterized inductively on the syntax of our process calculus, but this time using the three BIT-decomposition rules (in a controlled manner). The strict stack discipline of fork-join processes imposes a form of synchronous behavior: all the forked processes must terminate before a join may be performed. To support a limited form of asynchronism, a basic principle is to introduce promise processes.

In Table 2 we define a simple inductive process structure composed as follows. A main control thread can perform atomic actions (at any time), and also fork a sub-process of the form $\nu(B)\left(P\parallel Q\right)$ but with a strong restriction:

• •

a single barrier $B$ is created for the sub-processes to interact.

• •

the left sub-process $P$ must be the continuation of the main control thread,

• •

the right sub-process $Q$ must be a promise, which can only perform a sequence of atomic actions and ultimately synchronize with the control thread.

We are currently investigating this class as a whole, but we already obtained interesting results for the arch-processes in [7]. An arch-process follows the constraint of Table 2 but adds further restrictions. The main control thread can still spawn an arbitrary number of promises, however there must be two separate phases for the synchronization. After the first promise synchronizes, the main control thread cannot spawn any new promise. In [7] a supplementary constraint is added (for the sake of algorithmic efficiency): each promise must perform exactly one atomic action, and the control thread can only perform actions when all the promises are running. In this paper, we remove this rather artificial constraint considering a larger, and more useful process sub-class.

In Fig. 5 (left) is represented the general structure of a generalized arch-process. The $a_{i}$’s actions are the promise forks, and the synchronization points are the $c_{j}$’s. The constraint is thus that all the $a_{i}$’s occur before the $c_{j}$’s.

Theorem 18**.**

The number of executions of an arch-process can be calculated in $O(n^{2})$ arithmetic operations, using a dynamic programming algorithm based on memoization.

idea.

A complete proof is provided in [7] for “simple” arch-processes, and the generalization is detailed in the companion document. We only describe the inclusion-exclusion principle on which our counting algorithm is based. Fig. 5 (right) describes this principles (we omit the representation of the other promises to obtain a clear picture of our approach). Our objective is to count the number of execution contributed by a single promise with atomic action $b_{1,1}$. If we denote by $\ell_{\mathcal{P}}$ this contribution, we reformulate it as a combination \ell_{\mathcal{P}}=\ell_{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathcal{A}}}-\ell_{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{B}}}+\ell_{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}{\mathcal{C}}} as depicted on the rightmost part of Fig. 5. First, we take the “virtual” promise $\mathcal{A}$ going from the starting point $a_{1}$ of $\ell_{\mathcal{P}}$ until the end point $c_{k}$ of the main thread. Of course there are two many possibilities if we only keep {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathcal{A}}. An over-approximation of what it is to remove is the promise {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathcal{B}} going from the start of the last promise (at point $a_{k}$) until the end. But this time we removed too many possibilities, which corresponds to promise {\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\mathcal{C}}. The latter is thus reinserted in the count. Each of these three “virtual” promises have a simpler counting procedure. To guarantee the quadratic worst-time complexity (in the number of arithmetic operations), we have to memoize the intermediate results. We refer to the companion document for further details. ∎∎

From this counting procedure we developed a uniform random sampler following the principles of the recursive method, as described in [10].

Theorem 19**.**

Let $\mathcal{P}$ be a promise-process of size $n$ with $k\geq n$ promises. A random sampler of $O(n^{4})$ time-complexity (in the number of arithmetic operations) builds uniform executions.

The algorithm and the complete proof are detailed in the companion document. One notable aspect is that in order to get rid of the forbidden case of executions associated to the “virtual” promise {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathcal{B}} we cannot only do rejection (because the induced complexity would be exponential). In the generalization of arch-processes, we proceed by case analysis: for each possibility for the insertion of $b_{1,1}$ in the main control thread we compute the relative probability for the associated process $\mathcal{P}$. This explains the increase of complexity (from $O(n^{2})$ to $O(n^{4})$) if compared to [7].

5.3. BIT-free processes

The class of BIT-decomposable processes is rather large, and we in fact only uncovered two interesting sub-classes that can be easily captured inductively on the process syntax. The relatively non-trivial process $Sys$ of Fig. 2 is also interestingly BIT-decomposable. We now adopt the complementary view of trying to understand the combinatorial structure of a so called “BIT-free” process, which is not decomposable using only the (B), (I) and (T) rules.