{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T17:05:14Z","timestamp":1742403914768},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2006,3]]},"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.<\/jats:p>","DOI":"10.1145\/1119479.1119480","type":"journal-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T16:09:20Z","timestamp":1147104560000},"page":"207-255","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":164,"title":["Types for safe locking"],"prefix":"10.1145","volume":"28","author":[{"given":"Martin","family":"Abadi","sequence":"first","affiliation":[{"name":"Microsoft Research and University of California at Santa Cruz, Santa Cruz, CA"}]},{"given":"Cormac","family":"Flanagan","sequence":"additional","affiliation":[{"name":"University of California at Santa Cruz, Santa Cruz, CA"}]},{"given":"Stephen N.","family":"Freund","sequence":"additional","affiliation":[{"name":"Williams College, Williamstown, MA"}]}],"member":"320","published-online":{"date-parts":[[2006,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/263698.263720"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268974"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Static Analysis Symposium, A. Cortesi and G. Fil\u00e9, Eds. Lecture Notes in Computer Science","volume":"1694","author":"Aldrich J.","unstructured":"Aldrich , J. , Chambers , C. , Sirer , E. G. , and Eggers , S . 1999. Static analyses for eliminating unnecessary synchronization from Java programs . In Proceedings of the Static Analysis Symposium, A. Cortesi and G. Fil\u00e9, Eds. Lecture Notes in Computer Science , vol. 1694 . Springer-Verlag, 19--38.]] Aldrich, J., Chambers, C., Sirer, E. G., and Eggers, S. 1999. Static analyses for eliminating unnecessary synchronization from Java programs. In Proceedings of the Static Analysis Symposium, A. Cortesi and G. Fil\u00e9, Eds. Lecture Notes in Computer Science, vol. 1694. Springer-Verlag, 19--38.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002700"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/353171.353197"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320387"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320388"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 211--230","author":"Boyapati C.","unstructured":"Boyapati , C. , Lee , R. , and Rinard , M . 2002. A type system for preventing data races and deadlocks in Java programs . In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 211--230 .]] Boyapati, C., Lee, R., and Rinard, M. 2002. A type system for preventing data races and deadlocks in Java programs. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. 211--230.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504287"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286957"},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Computer Science on Foundations of Logic and Functional Programming","volume-title":"Typechecking dependent types and subtypes","author":"Cardelli L.","unstructured":"Cardelli , L. 1988. Typechecking dependent types and subtypes . In Lecture Notes in Computer Science on Foundations of Logic and Functional Programming . Springer-Verlag , New York , Inc., 45--57.]] Cardelli, L. 1988. Typechecking dependent types and subtypes. In Lecture Notes in Computer Science on Foundations of Logic and Functional Programming. Springer-Verlag, New York, Inc., 45--57.]]"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286958"},{"key":"e_1_2_1_15_1","volume-title":"Tech. Rep. 96-084, Department of Computer Science","author":"Chamillard A. T.","year":"1996","unstructured":"Chamillard , A. T. , Clarke , L. A. , and Avrunin , G. S . 1996 . An empirical comparison of static concurrency analysis techniques. Tech. Rep. 96-084, Department of Computer Science , University of Massachusetts at Amherst.]] Chamillard, A. T., Clarke, L. A., and Avrunin, G. S. 1996. An empirical comparison of static concurrency analysis techniques. Tech. Rep. 96-084, Department of Computer Science, University of Massachusetts at Amherst.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320386"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512560"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489078"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_1_21_1","volume-title":"Research Report 159, Compaq Systems Research Center.]]","author":"Detlefs D. L.","year":"1998","unstructured":"Detlefs , D. L. , Leino , K. R. M. , Nelson , G. , and Saxe, J. B. 1998 . Extended static checking. Research Report 159, Compaq Systems Research Center.]] Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Research Report 159, Compaq Systems Research Center.]]"},{"key":"e_1_2_1_22_1","volume-title":"European Conference On Object Oriented Programming. 389--418","author":"Drossopoulou S.","unstructured":"Drossopoulou , S. and Eisenbach , S . 1997. Java is type safe---Probably . In European Conference On Object Oriented Programming. 389--418 .]] Drossopoulou, S. and Eisenbach, S. 1997. Java is type safe---Probably. In European Conference On Object Oriented Programming. 389--418.]]"},{"key":"e_1_2_1_23_1","volume-title":"Tech. Rep. 94-045, Department of Computer Science","author":"Dwyer M. B.","year":"1994","unstructured":"Dwyer , M. B. and Clarke , L. A . 1994 . Data flow analysis for verifying properties of concurrent programs. Tech. Rep. 94-045, Department of Computer Science , University of Massachusetts at Amherst.]] Dwyer, M. B. and Clarke, L. A. 1994. Data flow analysis for verifying properties of concurrent programs. Tech. Rep. 94-045, Department of Computer Science, University of Massachusetts at Amherst.]]"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the International Conference on Concurrency Theory, D. Sangiorgi and R. de Simone, Eds. Lecture Notes in Computer Science","volume":"1466","author":"Fajstrup L.","unstructured":"Fajstrup , L. , Goubault , E. , and Raussen , M . 1998. Detecting deadlocks in concurrent systems . In Proceedings of the International Conference on Concurrency Theory, D. Sangiorgi and R. de Simone, Eds. Lecture Notes in Computer Science , vol. 1466 . Springer-Verlag, 332--347.]] Fajstrup, L., Goubault, E., and Raussen, M. 1998. Detecting deadlocks in concurrent systems. In Proceedings of the International Conference on Concurrency Theory, D. Sangiorgi and R. de Simone, Eds. Lecture Notes in Computer Science, vol. 1466. Springer-Verlag, 332--347.]]"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the International Conference on Concurrency Theory, J. C. M. Baeten and S. Mauw, Eds. Lecture Notes in Computer Science","volume":"1664","author":"Flanagan C.","unstructured":"Flanagan , C. and Abadi , M . 1999a. Object types against races . In Proceedings of the International Conference on Concurrency Theory, J. C. M. Baeten and S. Mauw, Eds. Lecture Notes in Computer Science , vol. 1664 . Springer-Verlag, 288--303.]] Flanagan, C. and Abadi, M. 1999a. Object types against races. In Proceedings of the International Conference on Concurrency Theory, J. C. M. Baeten and S. Mauw, Eds. Lecture Notes in Computer Science, vol. 1664. Springer-Verlag, 288--303.]]"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the European Symposium on Programming, S. D. Swierstra, Ed. Lecture Notes in Computer Science","volume":"1576","author":"Flanagan C.","unstructured":"Flanagan , C. and Abadi , M . 1999b. Types for safe locking . In Proceedings of the European Symposium on Programming, S. D. Swierstra, Ed. Lecture Notes in Computer Science , vol. 1576 . Springer-Verlag, 91--108.]] Flanagan, C. and Abadi, M. 1999b. Types for safe locking. In Proceedings of the European Symposium on Programming, S. D. Swierstra, Ed. Lecture Notes in Computer Science, vol. 1576. Springer-Verlag, 91--108.]]"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349328"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379687"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the Static Analysis Symposium. 116--132","author":"Flanagan C.","unstructured":"Flanagan , C. and Freund , S. N . 2004. Type inference against races . In Proceedings of the Static Analysis Symposium. 116--132 .]] Flanagan, C. and Freund, S. N. 2004. Type inference against races. In Proceedings of the Static Analysis Symposium. 116--132.]]"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007543"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"e_1_2_1_32_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"2021","author":"Flanagan C.","unstructured":"Flanagan , C. and Leino , K. R. M. 2001. Houdini, an annotation assistant for ESC\/Java. In Formal Methods Europe, J. N. Oliveira and P. Zave , Eds. Lecture Notes in Computer Science , vol. 2021 . Springer-Verlag, 500--517.]] Flanagan, C. and Leino, K. R. M. 2001. Houdini, an annotation assistant for ESC\/Java. In Formal Methods Europe, J. N. Oliveira and P. Zave, Eds. Lecture Notes in Computer Science, vol. 2021. Springer-Verlag, 500--517.]]"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604176"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268961"},{"key":"e_1_2_1_37_1","unstructured":"Gosling J. Joy B. and Steele G. 1996. The Java Language Specification. Addison-Wesley.]] Gosling J. Joy B. and Steele G. 1996. The Java Language Specification. Addison-Wesley.]]"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the IEEE Conference on Computer Aided Verification. 72--83","author":"Graf S.","unstructured":"Graf , S. and Saidi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the IEEE Conference on Computer Aided Verification. 72--83 .]] Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the IEEE Conference on Computer Aided Verification. 72--83.]]"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604177"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_41_1","unstructured":"JavaSoft. 1998. Java Developers Kit version 1.1. available from http:\/\/java.sun.com.]] JavaSoft. 1998. Java Developers Kit version 1.1. available from http:\/\/java.sun.com.]]"},{"key":"e_1_2_1_42_1","unstructured":"JavaSoft. 2004. Java Developer's Kit version 1.5. available from http:\/\/java.sun.com.]] JavaSoft. 2004. Java Developer's Kit version 1.5. available from http:\/\/java.sun.com.]]"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99623"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the International World Wide Web Conference. Computer Networks and ISDN Systems","volume":"30","author":"Kistler T.","unstructured":"Kistler , T. and Marais , J . 1998. WebL---A programming language for the web . In Proceedings of the International World Wide Web Conference. Computer Networks and ISDN Systems , vol. 30 . Elsevier, 259--270.]] Kistler, T. and Marais, J. 1998. WebL---A programming language for the web. In Proceedings of the International World Wide Web Conference. Computer Networks and ISDN Systems, vol. 30. Elsevier, 259--270.]]"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/276393.278524"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the International Conference on Concurrency Theory, C. Palamidessi, Ed. Lecture Notes in Computer Science","volume":"1877","author":"Kobayashi N.","unstructured":"Kobayashi , N. , Saito , S. , and Sumii , E . 2000. An implicitly-typed deadlock-free process calculus . In Proceedings of the International Conference on Concurrency Theory, C. Palamidessi, Ed. Lecture Notes in Computer Science , vol. 1877 . Springer-Verlag, 489--503.]] Kobayashi, N., Saito, S., and Sumii, E. 2000. An implicitly-typed deadlock-free process calculus. In Proceedings of the International Conference on Concurrency Theory, C. Palamidessi, Ed. Lecture Notes in Computer Science, vol. 1877. Springer-Verlag, 489--503.]]"},{"key":"e_1_2_1_47_1","volume-title":"Tech. Rep. 1999-002","author":"Leino K. R. M.","year":"1999","unstructured":"Leino , K. R. M. , Saxe , J. B. , and Stata , R . 1999 . Checking Java programs via guarded commands. Tech. Rep. 1999-002 , Compaq Systems Research Center , Palo Alto, CA .]] Leino, K. R. M., Saxe, J. B., and Stata, R. 1999. Checking Java programs via guarded commands. Tech. Rep. 1999-002, Compaq Systems Research Center, Palo Alto, CA.]]"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263714"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234745"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268960"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263715"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/379539.379553"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_2_1_55_1","unstructured":"Schmidt D. C. and Harrison T. H. 1997. Double-checked locking---A optimization pattern for efficiently initializing and accessing thread-safe objects. In Pattern Languages of Program Design 3 R. Martin F. Buschmann and D. Riehle Eds. Addison-Wesley.]] Schmidt D. C. and Harrison T. H. 1997. Double-checked locking---A optimization pattern for efficiently initializing and accessing thread-safe objects. In Pattern Languages of Program Design 3 R. Martin F. Buschmann and D. Riehle Eds. Addison-Wesley.]]"},{"key":"e_1_2_1_56_1","volume-title":"SPEC JBB2000","author":"Standard Performance Evaluation Corporation","year":"2000","unstructured":"Standard Performance Evaluation Corporation . 2000 . SPEC JBB2000 . Available from http:\/\/www.spec.org\/osg\/jbb 2000\/.]] Standard Performance Evaluation Corporation. 2000. SPEC JBB2000. Available from http:\/\/www.spec.org\/osg\/jbb2000\/.]]"},{"key":"e_1_2_1_57_1","volume-title":"USENIX Winter Technical Conference. 97--106","author":"Sterling N.","year":"1993","unstructured":"Sterling , N. 1993 . Warlock: A static data race analysis tool . In USENIX Winter Technical Conference. 97--106 .]] Sterling, N. 1993. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference. 97--106.]]"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000393"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177855"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504288"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/320384.320400"},{"key":"e_1_2_1_64_1","unstructured":"World Wide Web Consortium. 2001. Jigsaw. Available from http:\/\/www.w3c.org.]] World Wide Web Consortium. 2001. Jigsaw. Available from http:\/\/www.w3c.org.]]"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360206"},{"key":"e_1_2_1_66_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"1703","author":"Yu Y.","unstructured":"Yu , Y. , Manolios , P. , and Lamport , L . 1999. Model checking TLA+ specifications. In Correct Hardware Design and Verification Methods, L. Pierre and T. Kropf , Eds. Lecture Notes in Computer Science , vol. 1703 . Springer-Verlag, 54--66.]] Yu, Y., Manolios, P., and Lamport, L. 1999. Model checking TLA+ specifications. In Correct Hardware Design and Verification Methods, L. Pierre and T. Kropf, Eds. Lecture Notes in Computer Science, vol. 1703. Springer-Verlag, 54--66.]]"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1119479.1119480","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T20:05:16Z","timestamp":1672257916000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1119479.1119480"}},"subtitle":["Static race detection for Java"],"short-title":[],"issued":{"date-parts":[[2006,3]]},"references-count":63,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["10.1145\/1119479.1119480"],"URL":"https:\/\/doi.org\/10.1145\/1119479.1119480","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,3]]},"assertion":[{"value":"2006-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}