一句话:提出一种用于 C#/Visual Studio 的快速静态检查器,在编码时检测数据竞争与死锁。
并发程序中的数据竞争与死锁往往在开发后期才暴露,而编码时检查又要求工具兼具速度与精度。本文提出并实现了一个面向 C# 的实用静态检查器,集成于 Visual Studio,能在源代码中交互式标记数据竞争和死锁。其核心采用随机有界具体并发解释这一简单技术,并覆盖任务并行、数据并行、异步编程、UI 调度、多种同步原语、monitor、原子与 volatile 访问以及 finalizer 等并发语言概念。作者将该工具应用于流行的开源 C# 项目,发现了若干真实并发问题,同时仅产生少量误报,表明该方案在开发时并发检查场景中具有实用性。
We have developed a practical static checker that is designed to interactively mark data races and deadlocks in program source code at development time. As this use case requires a checker to be both fast and precise, we engaged a simple technique of randomized bounded concrete concurrent interpretation that is experimentally effective for this purpose. Implemented as a tool for C# in Visual Studio, the checker covers the broad spectrum of concurrent language concepts, including task and data parallelism, asynchronous programming, UI dispatching, the various synchronization primitives, monitor, atomic and volatile accesses, and finalizers. Its application to popular open-source C# projects revealed several real issues with only a few false positives.