一句话:提出 SURW,一种可对广泛程序或任意事件子集实现交织均匀采样的在线随机并发测试算法。
并发程序缺陷常只出现在极少数线程交织中,随机并发测试虽能概率采样大规模搜索空间,但现有算法探索均匀性不足,难以触发罕见交织导致的错误。本文针对黑盒随机并发测试的均匀探索特性,证明对广泛程序类仅需极少额外信息即可均匀采样交织空间;并提出仅对精心选取的事件子集施加该均匀性策略,以有效探索程序行为。作者实现在线随机算法 SURW(Selectively Uniform Random Walk)——首个对广泛程序类或其任意事件子集实现交织均匀性的此类算法。在主流并发基准上的评估表明,SURW 比同类随机算法发现更多缺陷且显著更快,并在真实程序上更均匀地探索交织与行为空间。
Buggy behaviors in concurrent programs are notoriously elusive, as they may manifest only in few of exponentially many possible thread interleavings. Randomized concurrency testing techniques probabilistically sample from (instead of enumerating) the vast search space and have been shown to be both an effective as well as a scalable class of algorithms for automated discovery of concurrency bugs. In this work we focus on the key desirable characteristic of black-box randomized concurrency testing algorithms --- uniformity of exploration. Unfortunately, prior randomized algorithms acutely fall short on uniformity and, as a result, struggle to expose bugs that only manifest in few, infrequent interleavings. Towards this, we show that, indeed, a sampling strategy for uniformly sampling over the interleaving space, is eminently achievable with minimal additional information for broad classes of programs. Moreover, when applied to a carefully selected subset of program events, this interleaving-uniformity strategy allows for an effective exploration of program behaviors. We present an online randomized concurrency testing algorithm named Selectively Uniform Random Walk (SURW) that builds on these insights. SURW is the first of its class to achieve interleaving-uniformity for a wide class of programs, or an arbitrary subset of events thereof. This property translates to effective behavioral exploration should a subset with desirable characteristics be selected. Extensive evaluation on leading concurrency benchmarks suggests SURW is able to expose more bugs and significantly faster than comparable randomized algorithms. In addition, we show that SURW is able to explore both the space of interleavings and behaviors more uniformly on real-world programs.