Type-safe multithreading in cyclone

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Type-safe multithreading in cyclone

Full text

Pdf (228 KB)

Source

Types In Languages Design And Implementation archive
Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation table of contents

New Orleans, Louisiana, USA

SESSION: Types and multithreading table of contents

Pages: 13 - 25

Year of Publication: 2003

ISBN:1-58113-649-8

Also published in ...

Author

Dan Grossman

Cornell University, Ithaca, NY

Sponsors

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

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 47, Citation Count: 33

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions 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/604174.604177 What is a DOI?

ABSTRACT

We extend Cyclone, a type-safe polymorphic language at the C level of abstraction, with threads and locks. Data races can violate type safety in Cyclone. An extended type system statically guarantees their absence by enforcing that thread-shared data is protected via locking and that thread-local data does not escape the thread that creates it. The extensions interact smoothly with parametric polymorphism and region-based memory management. We present a formal abstract machine that models the need to prevent races, a polymorphic type system for the machine that supports thread-local data, and a corresponding type-safety result.

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	Jonathan Aldrich , Craig Chambers , Emin Gün Sirer , Susan J. Eggers, Static Analyses for Eliminating Unnecessary Synchronization from Java Programs, Proceedings of the 6th International Symposium on Static Analysis, p.19-38, September 22-24, 1999
	2	David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
	3	Bruno Blanchet, Escape analysis for object-oriented languages: application to Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.20-34, November 01-05, 1999, Denver, Colorado, United States
	4	Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
	5	Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
	6	David R. Butenhof, Programming with POSIX threads, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
	7	Guang-Ien Cheng , Mingdong Feng , Charles E. Leiserson , Keith H. Randall , Andrew F. Stark, Detecting data races in Cilk programs that use locks, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.298-309, June 28-July 02, 1998, Puerto Vallarta, Mexico [doi>10.1145/277651.277696]
	8	Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
	9	Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	10	Cyclone User's Manual, 2002. http://www.cs.cornell.edu/projects/cyclone/.
	11	Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
	12	Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	13	Cormac Flanagan , Martín Abadi, Object Types against Races, Proceedings of the 10th International Conference on Concurrency Theory, p.288-303, August 24-27, 1999
	14	Cormac Flanagan , Martín Abadi, Types for Safe Locking, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.91-108, March 22-28, 1999
	15	Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
	16	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Thread-Modular Verification for Shared-Memory Programs, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.262-277, April 08-12, 2002
	17	Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	18	Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
	19	Dan Grossman, Existential Types for Imperative Languages, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.21-35, April 08-12, 2002
	20	Daniel Joseph Grossman , Greg Morrisett, Safe programming at the c level of abstraction, 2003
	21	Dan Grossman , Greg Morrisett , Trevor Jim , Michael Hicks , Yanling Wang , James Cheney, Region-based memory management in cyclone, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	22	Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
	23	J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
	24	George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
	25	Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
	26	N. Sterling. A static date race analysis tool. In USENIX Winter Technical Conference, pages 97--106, 1993.
	27	Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
	28	David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]
	29	Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

CITED BY 33

	Cormac Flanagan , Shaz Qadeer, Types for atomicity, ACM SIGPLAN Notices, v.38 n.3, March 2003
	Martin Abadi , Cormac Flanagan , Stephen N. Freund, Types for safe locking: Static race detection for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.207-255, March 2006
	Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Chandrasekhar Boyapati , Alexandru Salcianu , William Beebee, Jr. , Martin Rinard, Ownership types for safe region-based memory management in real-time Java, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
	Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, ACM SIGPLAN Notices, v.39 n.1, p.256-267, January 2004
	Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting purity for atomicity, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Michael F. Ringenburg , Dan Grossman, Types for describing coordinated data structures, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.25-36, January 10-10, 2005, Long Beach, California, USA
	Cormac Flanagan , Stephen N. Freund , Marina Lifshin, Type inference for atomicity, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.47-58, January 10-10, 2005, Long Beach, California, USA
	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer, Exploiting Purity for Atomicity, IEEE Transactions on Software Engineering, v.31 n.4, p.275-291, April 2005
	Xinyu Feng , Zhong Shao, Modular verification of concurrent assembly code with dynamic thread creation and termination, ACM SIGPLAN Notices, v.40 n.9, September 2005
	James Rose , Nikhil Swamy , Michael Hicks, Dynamic inference of polymorphic lock types, Science of Computer Programming, v.58 n.3, p.366-383, December 2005
	Dan Grossman, Quantified types in an imperative language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.3, p.429-475, May 2006
	Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, ACM SIGPLAN Notices, v.41 n.6, June 2006
	Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, ACM SIGPLAN Notices, v.42 n.1, January 2007
	Cormac Flanagan , Stephen N. Freund, Type inference against races, Science of Computer Programming, v.64 n.1, p.140-165, January, 2007
	Alexey Gotsman , Josh Berdine , Byron Cook , Mooly Sagiv, Thread-modular shape analysis, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Tachio Terauchi, Checking race freedom via linear programming, ACM SIGPLAN Notices, v.43 n.6, June 2008
	Pratibha Permandla , Michael Roberson , Chandrasekhar Boyapati, A type system for preventing data races and deadlocks in the java virtual machine language: 1, ACM SIGPLAN Notices, v.42 n.7, July 2007
	Cormac Flanagan , Stephen N. Freund , Marina Lifshin , Shaz Qadeer, Types for atomicity: Static checking and inference for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-53, July 2008
	Marius Nita , Dan Grossman , Craig Chambers, A theory of platform-dependent low-level software, ACM SIGPLAN Notices, v.43 n.1, January 2008
	Cormac Flanagan , Stephen N. Freund, Atomizer: A dynamic atomicity checker for multithreaded programs, Science of Computer Programming, v.71 n.2, p.89-109, April, 2008
	Jan Wen Voung , Ranjit Jhala , Sorin Lerner, RELAY: static race detection on millions of lines of code, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
	Dan Grossman, The transactional memory / garbage collection analogy, ACM SIGPLAN Notices, v.42 n.10, October 2007
	Joe Devietti , Colin Blundell , Milo M. K. Martin , Steve Zdancewic, Hardbound: architectural support for spatial safety of the C programming language, ACM SIGARCH Computer Architecture News, v.36 n.1, March 2008
	Tian Zhao , Jason Baker , James Hunt , James Noble , Jan Vitek, Implicit ownership types for memory management, Science of Computer Programming, v.71 n.3, p.213-241, May, 2008
	Nels E. Beckman , Kevin Bierhoff , Jonathan Aldrich, Verifying correct usage of atomic blocks and typestate, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Paruj Ratanaworabhan , Martin Burtscher , Darko Kirovski , Benjamin Zorn , Rahul Nagpal , Karthik Pattabiraman, Detecting and tolerating asymmetric races, Proceedings of the 14th ACM SIGPLAN symposium on Principles and practice of parallel programming, February 14-18, 2009, Raleigh, NC, USA
	Daniel Frampton , Stephen M. Blackburn , Perry Cheng , Robin J. Garner , David Grove , J. Eliot B. Moss , Sergey I. Salishev, Demystifying magic: high-level low-level programming, Proceedings of the 2009 ACM SIGPLAN/SIGOPS international conference on Virtual execution environments, March 11-13, 2009, Washington, DC, USA
	Cormac Flanagan , Stephen N. Freund, FastTrack: efficient and precise dynamic race detection, ACM SIGPLAN Notices, v.44 n.6, June 2009
	Zachary R. Anderson , David Gay , Mayur Naik, Lightweight annotations for controlling sharing in concurrent data structures, ACM SIGPLAN Notices, v.44 n.6, June 2009
	Tiago Cogumbreiro , Francisco Martins , Vasco T. Vasconcelos, Compiling the π-calculus into a Multithreaded Typed Assembly Language, Electronic Notes in Theoretical Computer Science (ENTCS), 241, p.57-84, July, 2009