Types for safe locking: Static race detection for Java
ACM Trans. Program. Lang. Syst.(2006)
摘要
This article presents a static race-detection analysis for multithreaded shared-memory programs, focusing on the Java programming language. The analysis is based on a type system that captures many common synchronization patterns. It supports classes with internal synchronization, classes that require client-side synchronization, and thread-local classes. In order to demonstrate the effectiveness of the type system, we have implemented it in a checker and applied it to over 40,000 lines of hand-annotated Java code. We found a number of race conditions in the standard Java libraries and other test programs. The checker required fewer than 20 additional type annotations per 1,000 lines of code. This article also describes two improvements that facilitate checking much larger programs: an algorithm for annotation inference and a user interface that clarifies warnings generated by the checker. These extensions have enabled us to use the checker for identifying race conditions in large-scale software systems with up to 500,000 lines of code.
更多查看译文
关键词
internal synchronization,large-scale software system,standard java library,additional type annotation,hand-annotated java code,concurrent programs,static race detection,type inference,java programming language,race conditions,common synchronization pattern,type system,race condition,client-side synchronization,user interface,shared memory,software systems,lines of code
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络