Types for safe locking: Static race detection for Java Export

@article{citeulike:5800900, abstract = {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.}, author = {Abadi, Martin and Flanagan, Cormac and Freund, Stephen N.}, citeulike-article-id = {5800900}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.9055}, journal = {ACM Transactions on Programming Languages and Systems}, keywords = {compilers, concurrency, java, ownership-types, programming-language-design, type-theory}, posted-at = {2009-09-18 03:04:37}, priority = {5}, title = {Types for safe locking: Static race detection for Java}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.9055}, volume = {28}, year = {2006} }

TY - JOUR ID - citeulike:5800900 L3 - citeulike-article-id:5800900 N2 - 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. JF - ACM Transactions on Programming Languages and Systems TI - Types for safe locking: Static race detection for Java VL - 28 KW - compilers KW - concurrency KW - java KW - ownership-types KW - programming-language-design KW - type-theory AU - Abadi, Martin AU - Flanagan, Cormac AU - Freund, Stephen PY - 2006/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.9055 ER -