Context-Bounded Verification of Thread Pools
summary
The work proves safety for thread-pooled Boolean programs with per-task context bound k and pool size n (both given in binary) is EXPSPACE-complete, while without pooling the k-only problem jumps to 3EXPSPACE-complete. It builds succinct pushdown automata encodings, computes succinct downward closures, converts them to doubly succinct NFA, and reduces verification to a transducer-controlled VASS coverability problem. The constructions are polynomial-time in the succinct representation and compress exponentially large NFAs so the EXPSPACE upper bound holds.
AI-written summary · about
chapters (18)
- 0:00Intro
- 0:43Multithreaded Shared-Memory Programs
- 1:44Thread Operations
- 2:26Switching Threads
- 2:52Running a New Task
- 3:04Summary of Model Features
- 3:30What is Decidable?
- 4:03Context-Switch Numbers
- 5:17Context-Bounded Analysis
- 7:03Thread Pool
- 8:59Outline
- 9:35Atig Bouajjani Qadeer 2EXPSPACE Result
- 11:59Succinct PDA
- 13:01Succinct Task PDA
- 14:34Bounded Stack PDA for Downclosure
- 17:31Transducer Controlled VASS
- 18:47TCVASS to VASS Coverability
- 20:05Conclusion
related talks
26mContext-Bounded Verification of Liveness for Multithreaded Shared-Memory Programs
19mCommutativity Simplifies Proofs of Parameterized Programs
25mParametrised Verification of Intel-x86 Programs
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
20mFixed Parameter Tractable Linearizability Monitoring
01h 02mThread pools: variety of algorithms and features
18mPetrification: Software Model Checking for Programs with Dynamic Thread Managem...
21mA Navigation Logic for Recursive Programs with Dynamic Thread Creation