pith. sign in

arxiv: 1907.04243 · v1 · pith:MOZDDJYWnew · submitted 2019-07-03 · 💻 cs.PL · cs.LO

The Combinatorics of Barrier Synchronization

Olivier Bodini , Matthieu Dien , Antoine Genitrini , Fr\'ed\'eric Peschanski This is my paper

Pith reviewed 2026-05-25 09:44 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords barrier synchronizationcombinatorial countingprocess executionsintegral formulascontrol graphsuniform random samplingdecomposition method
0
0 comments X

The pith

A systematic decomposition of processes yields symbolic integral formulas for counting executions under barrier synchronization.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a combinatorial method to count the executions of simple processes that interact through synchronization barriers. It does so by breaking processes into components whose interactions translate into a symbolic integral formula. This approach operates directly on the control graph rather than enumerating the full state space, which opens the door to uniform random generation of executions and to specialized efficient algorithms for certain process classes. A reader would care because the technique sidesteps the combinatorial explosion that usually makes concurrency analysis intractable.

Core claim

We elaborate a systematic decomposition of processes that produces a symbolic integral formula to solve the problem of counting the number of executions of simple processes interacting with synchronization barriers. 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.

What carries the argument

The systematic decomposition of processes into components that translate into a symbolic integral formula, performed on the control graph.

If this is right

  • A generic algorithm exists that samples executions uniformly at random using the same decomposition.
  • Specialized subclasses admit faster counting and sampling procedures that remain graph-based.
  • All derived algorithms avoid explicit state-space construction by staying on the control graph.
  • The integral representation directly encodes the quantitative effect of barrier synchronization.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same decomposition technique might apply to counting executions under other synchronization primitives if the barrier case generalizes.
  • One could test the formulas on larger but still manually enumerable processes to check scaling behavior.
  • The integral approach may connect to existing combinatorial methods for counting paths in graphs with additional constraints.
  • Uniform sampling enabled by the method could support statistical model checking without building the full state space.

Load-bearing premise

A decomposition of processes exists that captures every barrier interaction correctly and produces valid integral formulas without needing the full state space.

What would settle it

Compute the integral formula for a small concrete process with known barriers, enumerate its executions by hand or exhaustive search, and check whether the two numbers match.

Figures

Figures reproduced from arXiv: 1907.04243 by Antoine Genitrini, Fr\'ed\'eric Peschanski, Matthieu Dien, Olivier Bodini.

Figure 1
Figure 1. Figure 1: A process of size 2n and its control graph with 2n nodes and n 2 edges. Obviously PO(P) is a par￾tially ordered set (poset) with covering ≺, capturing the causal ordering of the actions of P. The covering of a partial or￾der is by construction an in￾transitive directed acyclic graph (DAG), hence the description of PO(P) itself is simply the tran￾sitive closure of the covering, yielding O(n 2 ) edges over n… view at source ↗
Figure 2
Figure 2. Figure 2: An example process with barrier synchroniza￾tions (left) and its control graph (right). The process is of size 16 and it has exactly 1975974 possible executions [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The BITS-decomposition and the construction of the counting formula. 3.1. Decomposition scheme. In [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: From left to right: the unit hypercube, the em￾bedding of the total order 1 ≺ 2 ≺ 3 and the embedding of the poset P = ({1, 2, 3}, {1 ≺ 2}) divided in its three linear extensions. Theorem 13. ([19, Corollary 4.2]) Let P be a Poset of size n then its number of linear extensions |LE (P)| = n! · V ol(CP ) where V ol(CP ) is the volume, defined by the Lebesgue measure, of the order polytope CP . The integral f… view at source ↗
Figure 5
Figure 5. Figure 5: The structure of an arch-process (left) and the inclusion-exclusion counting principle (right). In [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Typical BIT-free substructures, and their BIT “equivalent” (when possible). The BIT-free condition implies the occurrence of structures similar to the ones depicted on [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper studies synchronization combinatorially by counting executions of simple processes interacting with barriers. It introduces a systematic decomposition of processes yielding symbolic integral formulas for the count, develops a generic algorithm for uniform random generation of executions, and gives efficient counting/sampling algorithms for interesting subclasses. All algorithms operate directly on the control graph without explicit state-space construction.

Significance. If the decomposition is exhaustive and the integrals correctly encode barrier constraints without over- or under-counting, the work provides a parameter-free combinatorial method for a class of concurrent systems that avoids state-space explosion. The control-graph-only property and the shift to symbolic integrals are potentially valuable for random testing and analysis in concurrency.

major comments (2)
  1. [Abstract] Abstract and introduction: the central claim that the decomposition produces valid integral formulas rests on the unproven assumption that it is exhaustive for all barrier interactions in the defined class of simple processes; no validation data, error bounds, or proof sketch is referenced in the provided abstract, making it impossible to assess whether the counting claims hold.
  2. [Introduction / decomposition procedure] The weakest assumption (that the decomposition captures all interactions without explicit state-space) is load-bearing for the claim that the method works on the control graph alone; if any barrier configuration is missed, the integrals would be incorrect, yet no concrete test case or counter-example check is indicated.
minor comments (2)
  1. Define 'simple processes' and the precise class of barrier interactions at the outset to allow readers to assess the scope.
  2. Clarify how the symbolic integrals are evaluated numerically or symbolically for the random sampling algorithm.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their comments. We address the two major comments point by point below.

read point-by-point responses

  1. Referee: [Abstract] Abstract and introduction: the central claim that the decomposition produces valid integral formulas rests on the unproven assumption that it is exhaustive for all barrier interactions in the defined class of simple processes; no validation data, error bounds, or proof sketch is referenced in the provided abstract, making it impossible to assess whether the counting claims hold.

    Authors: The abstract is a high-level summary and therefore omits technical details such as the proof. The full manuscript defines the class of simple processes, presents the systematic decomposition procedure, and contains a formal proof that the decomposition is exhaustive (i.e., it accounts for every possible barrier interaction that can arise in this class). We will revise the abstract to include a brief reference to this proof. revision: yes

  2. Referee: [Introduction / decomposition procedure] The weakest assumption (that the decomposition captures all interactions without explicit state-space) is load-bearing for the claim that the method works on the control graph alone; if any barrier configuration is missed, the integrals would be incorrect, yet no concrete test case or counter-example check is indicated.

    Authors: The manuscript proves completeness of the decomposition with respect to the control-graph semantics of the processes; the proof shows that every reachable barrier configuration is accounted for by the integral formula without requiring an explicit product construction. The paper also supplies several worked examples that apply the procedure to concrete control graphs. We can add an explicit counter-example verification subsection if the referee considers the existing examples insufficient. revision: partial

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper derives counting formulas via an explicit systematic decomposition of processes into a symbolic integral representation, with all algorithms operating directly on the control graph. No equations or steps reduce by construction to fitted parameters, self-definitions, or load-bearing self-citations; the procedure is presented as a direct combinatorial construction without renaming known results or smuggling ansatzes. The central claim remains independent of its outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract, the central claim rests on the existence of a systematic process decomposition and the validity of resulting symbolic integrals; no free parameters, invented entities, or explicit axioms are mentioned.

pith-pipeline@v0.9.0 · 5634 in / 974 out tokens · 27219 ms · 2026-05-25T09:44:50.843069+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages · 1 internal anchor

  1. [1]

    Uniform generation in trac e monoids

    Samy Abbes and Jean Mairesse. Uniform generation in trac e monoids. In MFCS 2015, volume 9234 of LNCS, pages 63–75. Springer, 2015

    work page 2015

  2. [2]

    Rectangular Young tableaux with local decreases and the density method for uniform rand om generation (short version)

    Cyril Banderier, Philippe Marchal, and Michael Wallner . Rectangular Young tableaux with local decreases and the density method for uniform rand om generation (short version). In GASCom 2018 , Athens, Greece, June 2018

    work page 2018

  3. [3]

    Unifo rm sampling for networks of automata

    Nicolas Basset, Jean Mairesse, and Michèle Soria. Unifo rm sampling for networks of automata. In Concur 2017 , volume 85 of LIPIcs, pages 36:1–36:16. Schloss Dagstuhl, 2017

    work page 2017

  4. [4]

    Bodini, A

    O. Bodini, A. Genitrini, and F. Peschanski. The combinat orics of non-determinism. In FSTTCS’13, volume 24 of LIPIcs, pages 425–436. Schloss Dagstuhl, 2013

    work page 2013

  5. [5]

    Bodini, A

    O. Bodini, A. Genitrini, and F. Peschanski. A Quantitati ve Study of Pure Parallel Processes. Electronic Journal of Combinatorics , 23(1):P1.11, 39 pages, 2016

    work page 2016

  6. [6]

    Entropic uniform sampling of linear extensions in series-parallel p osets

    Olivier Bodini, Matthieu Dien, Antoine Genitrini, and F rédéric Peschanski. Entropic uniform sampling of linear extensions in series-parallel p osets. In CSR 2017 , volume 10304 of LNCS, pages 71–84. Springer, 2017

    work page 2017

  7. [7]

    Beyond series- parallel concurrent systems: The case of arch processes

    Olivier Bodini, Matthieu Dien, Antoine Genitrini, and A lfredo Viola. Beyond series- parallel concurrent systems: The case of arch processes. In Analysis of Algorithms, AofA 2018 , volume 110 of LIPIcs, pages 14:1–14:14, 2018

    work page 2018

  8. [8]

    Brightwell and P

    G. Brightwell and P. Winkler. Counting linear extension s is #P-complete. In STOC, pages 175–181, 1991

    work page 1991

  9. [9]

    Counting linear extensions of restricted posets

    Samuel Dittmer and Igor Pak. Counting linear extensions of restricted posets. arXiv e-prints, page arXiv:1802.06312, February 2018

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  10. [10]

    Flajolet, P

    P. Flajolet, P. Zimmermann, and B. Van Cutsem. A calculu s for the random genera- tion of labelled combinatorial structures. Theor. Comput. Sci. , 132(2):1–35, 1994

    work page 1994

  11. [11]

    A. V. Gerbessiotis and L. G. Valiant. Direct bulk-synch ronous parallel algorithms. J. Parallel Distrib. Comput. , 22(2):251–267, 1994

    work page 1994

  12. [12]

    Grosu and S

    R. Grosu and S. A. Smolka. Monte carlo model checking. In TACAS’05, volume 3440 of LNCS, pages 271–286. Springer, 2005

    work page 2005

  13. [13]

    Hensgen, R

    D. Hensgen, R. A. Finkel, and U. Manber. Two algorithms f or barrier synchronization. International Journal of Parallel Programming , 17(1):1–17, 1988

    work page 1988

  14. [14]

    M. Huber. Fast perfect sampling from linear extensions . Discrete Mathematics , 306(4):420–428, 2006

    work page 2006

  15. [15]

    Liskov and L

    B. Liskov and L. Shrira. Promises: Linguistic support f or efficient asynchronous pro- cedure calls in distributed systems. In PLDI’88, pages 260–267. ACM, 1988

    work page 1988

  16. [16]

    Uniform monte-carlo model checking

    Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Ric hard Lassaigne, and Syl- vain Peyronnet. Uniform monte-carlo model checking. In F ASE 2011, volume 6603 of LNCS. Springer, 2011

    work page 2011

  17. [17]

    Algorithms and Order

    Ivan Rival, editor. Algorithms and Order . NATO Science Series. Springer, 1988

    work page 1988

  18. [18]

    Effective random testing of concurrent pro grams

    Koushik Sen. Effective random testing of concurrent pro grams. In Automated Software Engineering ASE’07 , pages 323–332. ACM, 2007

    work page 2007

  19. [19]

    R. P. Stanley. Two poset polytopes. Discrete & Computational Geometry , 1:9–23, 1986. THE COMBINATORICS OF BARRIER SYNCHRONIZATION 21 Labora toire d’Informa tique de P aris-Nord, CNRS UMR 7030 - I nstitut Galilée - Université P aris-Nord, 99, a venue Jean-Baptiste Clément, 93430 Villetaneuse, France. E-mail address : Olivier.Bodini@lipn.univ-paris13.fr Un...

    work page 1986