Checking race freedom via linear programming

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Checking race freedom via linear programming

Full text

Pdf (192 KB)

Source

Conference on Programming Language Design and Implementation archive
Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation table of contents

Tucson, AZ, USA

SESSION: Session I table of contents

Pages 1-10

Year of Publication: 2008

ISBN:978-1-59593-860-2

Also published in ...

Author

Tachio Terauchi

Tohoku University, Sendai, Japan

Sponsors

ACM: Association for Computing Machinery
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 55, Downloads (12 Months): 146, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTex EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1375581.1375583 What is a DOI?

ABSTRACT

We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to (rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	GNU Linear Programming Kit. http://www.gnu.org/software/glpk/glpk.html.
	2	R. Agarwal and S. D. Stoller. Type inference for parameterized race-free Java. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Proceedings, pages 149--160.
	3	R. Bornat, C. Calcagno, P. W. O'Hearn, and M. J. Parkinson. Permission accounting in separation logic. In Proceedings of the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 259--270, Long Beach, California, Jan. 2005.
	4	C. Boyapati, A. Salcianu, W. Beebee, Jr., and M. Rinard. Ownership types for safe region-based memory management in real-time Java. In Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation, San Diego, California, June 2003.
	5	J. Boyland. Checking interference with fractional permissions. In Static Analysis, Tenth International Symposium, pages 55--72, San Diego, CA, June 2003.
	6	M. Das. Unification-based pointer analysis with directional assignments. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 35--46, Vancouver B.C., Canada, June 2000.
	7	M. Das, B. Liblit, M. Fähndrich, and J. Rehof. Estimating the impact of scalable pointer analysis on optimization. In Static Analysis, Eighth International Symposium, pages 260--278, Paris, France, July 2001.
	8	M. F\"ahndrich, J. Rehof, and M. Das. Scalable context-sensitive flow analysis using instantiation constraints. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 253--263, Vancouver B.C., Canada, June 2000.
	9	C. Flanagan and M. Abadi. Types for safe locking. In D. Swierstra, editor, 8th European Symposium on Programming, volume 1576 of Lecture Notes in Computer Science, pages 91--108, Amsterdam, The Netherlands, Mar. 1999. Springer-Verlag.
	10	C. Flanagan and S. N. Freund. Type-based race detection for Java. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 219--232, Vancouver B.C., Canada, June 2000.
	11	C. Flanagan and S. N. Freund. Type inference against races. In Static Analysis, Eleventh International Symposium, pages 116--132, Verona, Italy, August 2004.
	12	J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, Berlin, Germany, June 2002.
	13	D. Grossman. Type-safe multithreading in Cyclone. In Proceedings of the 2003 ACM Workshop on Types in Language Design and Implementation, pages 13--25, New Orleans, Louisiana, Jan. 2003.
	14	J. Kodumal and A. Aiken. The set constraint/cfl reachability connection in practice. In Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 207--218, Washington DC, USA, June 2004.
	15	S. Mimram. ocaml-glpk. http://ocaml-glpk.sourceforge.net/.
	16	H. Mittelmann. Benchmarks for optimization software. http://plato.asu.edu/bench.html.
	17	M. Naik and A. Aiken. Conditional must not aliasing for static race detection. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 327--338, Nice, France, Jan. 2007.
	18	M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 308--319, Ottawa, Ontario, Canada, June 2006.
	19	G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of c programs. In Compiler Construction, 11th International Conference, pages 213--228, Grenoble, France, Apr. 2002.
	20	P. Pratikakis, J. S. Foster, and M. W. Hicks. LOCKSMITH: context-sensitive correlation analysis for race detection. In Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 320--331, Ottawa, Ontario, Canada, June 2006.
	21	T. Terauchi and A. Aiken. A capability calculus for concurrency and determinism. In Concurrency Theory, 17th International Conference, volume 4137, pages 218--232, Bonn, Germany, Aug. 2006.
	22	J. W. Voung, R. Jhala, and S. Lerner. RELAY: static race detection on millions of lines of code. In Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 205--214, Dubrovnik, Croatia, Sept. 2007.
	23	J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 131--144, Washington DC, USA, June 2004.