Article

Type-safe multithreading in cyclone

Author:

Dan GrossmanAuthors Info & Claims

TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation

Pages 13 - 25

https://doi.org/10.1145/604174.604177

Published: 18 January 2003 Publication History

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

[1]

J. Aldrich, C. Chambers, E. G. Sirer, and S. Eggers. Eliminating unnecessary synchronization from Java programs. In 6th International Static Analysis Symposium, volume 1694 of Lecture Notes in Computer Science, pages 19--38, Venice, Italy, Sept. 1999. Springer-Verlag.]]

Digital Library

[2]

D. Bacon, R. Strom, and A. Tarafdar. Guava: A dialect of Java without data races. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 382--400, Minneapolis, MN, Oct. 2000.]]

Digital Library

[3]

B. Blanchet. Escape analysis for object oriented languages. Application to Java. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 20--34, Denver, CO, Nov. 1999.]]

Digital Library

[4]

C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 211--230, Seattle, WA, Nov. 2002.]]

Digital Library

[5]

C. Boyapati and M. Rinard. A parameterized type system for race-free Java programs. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 56--69, Tampa Bay, FL, Oct. 2001.]]

Digital Library

[6]

D. Butenhof. Programming with POSIX® Threads. Addison-Wesley, 1997.]]

Digital Library

[7]

G.-I. Cheng, M. Feng, C. Leiserson, K. Randall, and A. Stark. Detecting data races in Cilk programs that use locks. In 10th ACM Symposium on Parallel Algorithms and Architectures, pages 298--309, Puerto Vallarta, Mexico, June 1998.]]

Digital Library

[8]

J.-D. Choi, M. Gupta, M. Serrano, V. Sreedhar, and S. Midkiff. Escape analysis for Java. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 1--19, Denver, CO, Nov. 1999.]]

Digital Library

[9]

J.-D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In ACM Conference on Programming Language Design and Implementation, pages 258--269, Berlin, Germany, June 2002.]]

Digital Library

[10]

Cyclone User's Manual, 2002. http://www.cs.cornell.edu/projects/cyclone/.]]

[11]

R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In ACM Conference on Programming Language Design and Implementation, pages 59--69, Snowbird, UT, June 2001.]]

Digital Library

[12]

M. Fähndrich and R. DeLine. Adoption and focus: Practical linear types for imperative programming. In ACM Conference on Programming Language Design and Implementation, pages 13--24, Berlin, Germany, June 2002.]]

Digital Library

[13]

C. Flanagan and M. Abadi. Object types against races. In CONCUR'99---Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 288--303, Eindhoven, The Netherlands, Aug. 1999. Springer-Verlag.]]

[14]

C. Flanagan and M. Abadi. Types for safe locking. In 8th European Symposium on Programming, volume 1576 of Lecture Notes in Computer Science, pages 91--108, Amsterdam, The Netherlands, Mar. 1999. Springer-Verlag.]]

Digital Library

[15]

C. Flanagan and S. Freund. Type-based race detection for Java. In ACM Conference on Programming Language Design and Implementation, pages 219--232, Vancouver, Canada, June 2000.]]

Digital Library

[16]

C. Flanagan, S. Freund, and S. Qadeer. Thread-modular verification for shared-memory programs. In 11th European Symposium on Programming, volume 2305 of Lecture Notes in Computer Science, pages 262--277, Grenoble, France, Apr. 2002. Springer-Verlag.]]

Digital Library

[17]

C. Flanagan, K. R. Leino, M. Lillibridge, G. Nelson, J. Saxe, and R. Stata. Extended static checking for Java. In ACM Conference on Programming Language Design and Implementation, pages 234--245, Berlin, Germany, June 2002.]]

Digital Library

[18]

J. Foster, M. Fähndrich, and A. Aiken. A theory of type qualifiers. In ACM Conference on Programming Language Design and Implementation, pages 192--203, Atlanta, GA, May 1999.]]

Digital Library

[19]

D. Grossman. Existential types for imperative languages. In 11th European Symposium on Programming, volume 2305 of Lecture Notes in Computer Science, pages 21--35, Grenoble, France, Apr. 2002. Springer-Verlag.]]

Digital Library

[20]

D. Grossman. Safe Programming at the C Level of Abstraction. PhD thesis, Cornell University, 2003. Forthcoming.]]

Digital Library

[21]

D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Region-based memory management in Cyclone. In ACM Conference on Programming Language Design and Implementation, pages 282--293, Berlin, Germany, June 2002.]]

Digital Library

[22]

T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In USENIX Annual Technical Conference, pages 275--288, Monterey, CA, June 2002.]]

Digital Library

[23]

J. Lucassen and D. Gifford. Polymorphic effect systems. In 15th ACM Symposium on Principles of Programming Languages, pages 47--57, San Diego, CA, Jan. 1988.]]

Digital Library

[24]

G. Necula, S. McPeak, and W. Weimer. CCured: Type-safe retrofitting of legacy code. In 29th ACM Symposium on Principles of Programming Languages, pages 128--139, Portland, OR, Jan. 2002.]]

Digital Library

[25]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems, 15(4):391--411, Nov. 1997.]]

Digital Library

[26]

N. Sterling. A static date race analysis tool. In USENIX Winter Technical Conference, pages 97--106, 1993.]]

[27]

C. von Praun and T. Gross. Object race detection. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 70--82, Tampa Bay, FL, Oct. 2001.]]

Digital Library

[28]

D. Walker, K. Crary, and G. Morrisett. Typed memory management in a calculus of capabilities. ACM Transactions on Programming Languages and Systems, 24(4):701--771, July 2000.]]

Digital Library

[29]

A. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.]]

Digital Library

Cited By

Pearce D(2021)A Lightweight Formalism for Reference Lifetimes and Borrowing in RustACM Transactions on Programming Languages and Systems10.1145/344342043:1(1-73)Online publication date: 17-Apr-2021
https://dl.acm.org/doi/10.1145/3443420
Zhou DTamir Y(2019)PUShProceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchitecture10.1145/3352460.3358317(886-898)Online publication date: 12-Oct-2019
https://dl.acm.org/doi/10.1145/3352460.3358317
Wilcox JFlanagan CFreund S(2018)VerifiedFTACM SIGPLAN Notices10.1145/3200691.317851453:1(354-367)Online publication date: 10-Feb-2018
https://dl.acm.org/doi/10.1145/3200691.3178514
Show More Cited By

Index Terms

Type-safe multithreading in cyclone
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Concurrent programming structures
        Polymorphism
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Type-safe multithreading in cyclone

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 ...
Ownership types for safe programming: preventing data races and deadlocks
OOPSLA '02: Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications

This paper presents a new static type system for multithreaded programs; well-typed programs in our system are guaranteed to be free of data races and deadlocks. Our type system allows programmers to partition the locks into a fixed number of ...
Ownership types for safe programming: preventing data races and deadlocks

This paper presents a new static type system for multithreaded programs; well-typed programs in our system are guaranteed to be free of data races and deadlocks. Our type system allows programmers to partition the locks into a fixed number of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation

January 2003

144 pages

ISBN:1581136498

DOI:10.1145/604174

General Chair:
Zhong Shao
Yale University
,
Program Chair:
Peter Lee
Carnegie Mellon University

ACM SIGPLAN Notices Volume 38, Issue 3
March 2003
134 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/640136
Issue’s Table of Contents

Copyright © 2003 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 January 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

TLDI03

Sponsor:

TLDI03: International Workshop on Types in Language Design and Implementation 2003

January 18, 2003

Louisiana, New Orleans, USA

Acceptance Rates

TLDI '03 Paper Acceptance Rate 11 of 26 submissions, 42%;

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

111
Total Citations
View Citations
356
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pearce D(2021)A Lightweight Formalism for Reference Lifetimes and Borrowing in RustACM Transactions on Programming Languages and Systems10.1145/344342043:1(1-73)Online publication date: 17-Apr-2021
https://dl.acm.org/doi/10.1145/3443420
Zhou DTamir Y(2019)PUShProceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchitecture10.1145/3352460.3358317(886-898)Online publication date: 12-Oct-2019
https://dl.acm.org/doi/10.1145/3352460.3358317
Wilcox JFlanagan CFreund S(2018)VerifiedFTACM SIGPLAN Notices10.1145/3200691.317851453:1(354-367)Online publication date: 10-Feb-2018
https://dl.acm.org/doi/10.1145/3200691.3178514
Wilcox JFlanagan CFreund SKrall AGross T(2018)VerifiedFTProceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3178487.3178514(354-367)Online publication date: 10-Feb-2018
https://dl.acm.org/doi/10.1145/3178487.3178514
Xu MQian CLu KBackes MKim T(2018)Precise and Scalable Detection of Double-Fetch Bugs in OS Kernels2018 IEEE Symposium on Security and Privacy (SP)10.1109/SP.2018.00017(661-678)Online publication date: May-2018
https://doi.org/10.1109/SP.2018.00017
Luo PZou DJin HDu YZheng LShen J(2018)DigHRThe Journal of Supercomputing10.1007/s11227-018-2307-874:6(2684-2704)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s11227-018-2307-8
Lochbihler A(2018)Mechanising a Type-Safe Model of Multithreaded Java with a Verified CompilerJournal of Automated Reasoning10.1007/s10817-018-9452-x61:1-4(243-332)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-018-9452-x
Bagherzadeh MRajan HDe Koster JBergenti F(2017)Order types: static reasoning about message races in asynchronous message passing concurrencyProceedings of the 7th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control10.1145/3141834.3141837(21-30)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3141834.3141837
Rhodes DFlanagan CFreund S(2017)BigFoot: static check placement for dynamic race detectionACM SIGPLAN Notices10.1145/3140587.306235052:6(141-156)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062350
Rhodes DFlanagan CFreund SCohen AVechev M(2017)BigFoot: static check placement for dynamic race detectionProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062350(141-156)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062350
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents