Generating Concurrency Checks Automatically
Jonathan Hoyland, Matthew Hague

TL;DR
This paper presents ATAB, an automated tool that generates efficient pairwise reachability checks for concurrent programs modeled as action trees, improving scalability and automation in concurrency analysis.
Contribution
Introduces ATAB, a tool that automates the generation of compact alternating tree automata for pairwise reachability in lock-based concurrent programs.
Findings
ATAB produces more compact automata than previous methods.
The automata are more efficiently checkable and scalable.
Automation simplifies encoding complex concurrency checks.
Abstract
This article introduces ATAB, a tool that automatically generates pairwise reachability checks for action trees. Action trees can be used to study the behaviour of real-world concurrent programs. ATAB encodes pairwise reachability checks into alternating tree automata that determine whether an action tree has a schedule where any pair of given points in the program are simultaneously reachable. Because the pairwise reachability problem is undecidable in general ATAB operates under a restricted form of lock-based concurrency. ATAB produces alternating tree automata that are more compact and more efficiently checkable than those that have been previously used. The process is entirely automated, which simplifies the process of encoding checks for more complex action trees. The alternating tree automata produced are easier to scale to large numbers of locks than previous constructions.
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.
