We present a tool BEST (Binary instrumentation-based Error-directed Symbolic Testing) for predicting concurrency violations.1 We automatically infer potential concurrency violations such as atomicity violations from an observed run of a multi-threaded program, and use precise modeling and constraint-based symbolic (non-enumerative) search to find feasible violating schedules in a generalization of the observed run. We specifically focus on tool scalability by devising POR-based simplification steps to reduce the formula and the search space by several orders-of-magnitude. We have successfully applied the tool to several publicly available C/C++/Java programs and found several previously known/unknown concurrency related bugs. The tool also has extensive visual support for debugging.
展开▼
机译：我们介绍了一种最佳刀具（基于二进制仪器的错误定向符号测试），用于预测并发违规。 1 我们自动推断出潜在的并发违规，例如从观察到的多线程程序运行的原子违规，并使用基于精确的建模和基于约束的符号（非枚举）搜索，以在观察到的运行的概括中找到可行的违反计划。我们通过设计基于POR的简化步骤来专注于刀具可扩展性，以便将公式和搜索空间的数量级减少。我们已成功将该工具应用于几个公开可用的C / C ++ / Java程序，并找到了几个先前已知/未知的并发相关的错误。该工具还具有广泛的视觉支持来调试。
展开▼
