BWoS - Formally Verified Block-based Work Stealing for Parallel Processing

Explore a 15-minute conference talk from OSDI '23 that introduces Block-based Work Stealing (BWoS), a novel approach to parallel processing scheduling. Delve into the design that splits per-core queues into multiple blocks, reducing interference between thieves and owners while enabling aggressive optimizations. Learn about the probabilistic stealing policy that ensures thieves target longer queues with higher probability. Discover how BWoS improves performance in various applications, including Java GC, Go runtime for JSON processing, and Rust Tokio runtime for HTTP servers. Examine the formal verification process and optimization techniques applied to BWoS on weak memory models using a model-checking-based framework.