Presentation
Parallelizing Complementary Approximate Reachability
DescriptionModel checking, especially symbolic algorithms such as IC3/PDR, is a powerful verification technique but is increasingly constrained by single-threaded performance. Existing parallel model checking approaches either rely on redundant portfolio executions or suffer from scalability bottlenecks caused by centralized scheduling.
We propose a new parallel paradigm for model checking based on fine-grained task decomposition and a decentralized Work-pulling architecture. A distributed concurrent task repository replaces the central coordinator, enabling worker threads to autonomously acquire tasks and naturally achieve dynamic load balancing. We present the framework design, analyze its parallel mechanisms, and evaluate its performance on representative benchmarks. Our approach achieves notable speedup and demonstrates solid scalability over serial execution.
We propose a new parallel paradigm for model checking based on fine-grained task decomposition and a decentralized Work-pulling architecture. A distributed concurrent task repository replaces the central coordinator, enabling worker threads to autonomously acquire tasks and naturally achieve dynamic load balancing. We present the framework design, analyze its parallel mechanisms, and evaluate its performance on representative benchmarks. Our approach achieves notable speedup and demonstrates solid scalability over serial execution.
Event Type
Research Manuscript
TimeWednesday, July 2911:54am - 12:06pm PDT
LocationMtg Room 202AB