Syntactic Regions for Concurrent Programs
Samuel Mimram (Ecole polytechnique), Aly-Bora Ulusoy (Ecole, polytechnique)

TL;DR
This paper introduces a method to analyze concurrent programs using syntactic regions derived directly from program syntax, enabling geometrical modeling of execution states for better verification.
Contribution
It demonstrates that regions for modeling concurrent programs can be constructed directly from syntax, forming a boolean algebra with explicit algorithms, simplifying geometrical analysis.
Findings
Regions form a boolean algebra under reasonable conditions
Explicit algorithms for region operations are provided
Normal form representations facilitate program state analysis
Abstract
In order to gain a better understanding of the state space of programs, with the aim of making their verification more tractable, models based on directed topological spaces have been introduced, allowing to take in account equivalence between execution traces, as well as translate features of the execution (such as the presence of deadlocks) into geometrical situations. In this context, many algorithms were introduced, based on a description of the geometrical models as regions consisting of unions of rectangles. We explain here that these constructions can actually be performed directly on the syntax of programs, thus resulting in representations which are more natural and easier to implement. In order to do so, we start from the observation that positions in a program can be described as partial explorations of the program. The operational semantics induces a partial order on…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
