More Web Proxy on the site http://driver.im/

Article

Flow-sensitive type qualifiers

Authors:

Jeffrey S. Foster,

Tachio Terauchi,

Alex AikenAuthors Info & Claims

PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation

Pages 1 - 12

https://doi.org/10.1145/512529.512531

Published: 17 May 2002 Publication History

Abstract

We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled flow-sensitively---the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. We demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the Linux kernel.

References

[1]

A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tool Addison Wesley, 1988]]

Digital Library

[2]

A. Aiken, M. Fahndrich, and R. Levien. Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages. Proceedings of the 1995 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 174--185, La Jolla, California, June 1995]]

Digital Library

[3]

R. Altucher and W. Landi. An Extended Form of Must Alias Analysis for Dynamic Allocation.Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 74--84, San Francisco, California, Jan. 1995]]

Digital Library

[4]

D. R. Chase, M. Wegman, and F. K. Zadeck. Analysis of Pointers and Structures. Proceedings of the 1990 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 296--310, White Plains, New York, June 1990]]

Digital Library

[5]

K. Crary, D. Walker, and G. Morrisett. Typed Memory Management in a Calculus of Capabilities. Proceedings of the Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 262--275, San Antonio, Texas, Jan. 1999]]

Digital Library

[6]

M. Das, S. Lerner, and M. Seigle. SP: Path-Sensitive Program Verification in Polynomial Time. Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, Berlin, Germany, June 2002. To appear]]

Digital Library

[7]

R. DeLine and M. Fahndrich. Enforcing High-Level Protocols in Low-Level Software. Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 59--69, Snowbird, Utah, June 2001]]

Digital Library

[8]

M. Emami, R. Ghiya, and L. J. Hendren. Context-Sensitive Interprocedural Points-to Analysis in the Presence of Function Pointers. Proceedings of the 1994 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 242--256, Orlando, Florida, June 1994]]

Digital Library

[9]

D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions. Fourth symposium on Operating System Design and Implementation, San Diego, California, Oct. 2000]]

Digital Library

[10]

D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code. Proceedings of the 18th ACM Symposium on Operating Systems Principles, Banff, Canada, Oct. 2001]]

Digital Library

[11]

D. Evans. Static Detection of Dynamic Memory Errors. Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 44--53, Philadelphia, Pennsylvania, May 1996]]

Digital Library

[12]

M. Fahndrich and R. DeLine. Adoption and Focus: Practical Linear Types for Imperative Programming. Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, Berlin, Germany, June 2002. To appear]]

Digital Library

[13]

C. Flanagan and S. N. Freund. Type-Based Race Detection for Java. Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 219--232, Vancouver B.C., Canada, June 2000]]

Digital Library

[14]

C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended Static Checking for Java. Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, Berlin, Germany, June 2002. To appear]]

Digital Library

[15]

J. S. Foster and A. Aiken. Checking Programmer-Specified Non-Aliasing. Technical Report UCB//CSD-01-1160, University of California, Berkeley, Oct. 2001]]

Digital Library

[16]

J. S. Foster, M. Fahndrich, and A. Aiken. A Theory of Type Qualifiers. Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 192--203, Atlanta, Georgia, May 1999]]

Digital Library

[17]

D. Grossman, G. Morrisett, Y. Wang, T. Jim, M. Hicks, and J. Cheney. Cyclone user's manual. Technical Report 2001-1855, Department of Computer Science, Cornell University, Nov. 2001. Current version at http://www.cs.cornell.edu/projects/cyclone]]

Digital Library

[18]

A. Igarashi and N. Kobayashi. Resource Usage Analysis. Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 331--342, Portland, Oregon, Jan. 2002]]

Digital Library

[19]

S. Jagannathan, P. Thiemann, S. Weeks, and A. Wright. Single and loving it: Must-alias analysis for higher-order languages. Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 329--341, San Diego, California, Jan. 1998]]

Digital Library

[20]

J. M. Lucassen and D. K. Gifford. Polymorphic Effect Systems. Proceedings of the 15th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47--57, San Diego, California, Jan. 1988]]

Digital Library

[21]

G. Necula, S. McPeak, and W. Weimer. CCured: Type-Safe Retrofitting of Legacy Code. In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 128--139, Portland, Oregon, Jan. 2002]]

Digital Library

[22]

R. O'Callahan. A Simple, Comprehensive Type System for Java Bytecode Subroutines. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 70--78, San Antonio, Texas, Jan. 1999]]

Digital Library

[23]

J. Rehof and T. AE. Mogensen.Tractable Constraints in Finite Semilattices. In R. Cousot and D. A. Schmidt, editors, Static Analysis, Third International Symposium, volume 1145 of Lecture Notes in Computer Science, pages 285--300, Aachen, Germany, Sept. 1996. Springer-Verlag]]

Digital Library

[24]

U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Detecting Format String Vulnerabilities with Type Qualifiers. Proceedings of the 10th Usenix Security Symposium, Washington, D.C., Aug. 2001]]

Digital Library

[25]

F. Smith, D. Walker, and G. Morrisett. Alias Types. In G. Smolka, editor, 9th European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 366--381, Berlin, Germany, 2000. Springer-Verlag]]

Digital Library

[26]

R. Stata and M. Abadi. A Type System for Java Bytecode Subroutines. Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 149--160, San Diego, California, Jan. 1998]]

Digital Library

[27]

R. E. Strom and S. Yemini. Typestate: A Programming Language Concept for Enhancing Software Reliability.IEEE Transactions on Software Engineering, 12(1):157--171, Jan. 1986]]

Digital Library

[28]

M. Tofte and J.-P. Talpin. Implementation of the Typed Call-by-Value Calculus using a Stack of Regions. Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 188--201, Portland, Oregon, Jan. 1994]]

Digital Library

[29]

D. Walker and G. Morrisett. Alias Types for Recursive Data Structures. International Workshop on Types in Compilation, Montreal, Canada, Sept. 2000]]

Digital Library

[30]

D. Weise, 2001. Personal communication]]

[31]

R. P. Wilson and M. S. Lam. Efficient Context-Sensitive Pointer Analysis for C Programs. Proceedings of the 1995 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1--12, La Jolla, California, June 1995]]

Digital Library

[32]

A. K. Wright. Typing References by Effect Inference. In B. Krieg-Brucker, editor, 4th European Symposium on Programming, volume 582 of Lecture Notes in Computer Science, pages 473--491, Rennes, France, Feb. 1992. Springer-Verlag]]

Digital Library

[33]

Z. Xu, T. Reps, and B. P. Miller. Typestate Checking of Machine Code. In D. Sands, editor, 10th European Symposium on Programming, volume 2028 of Lecture Notes in Computer Science, pages 335--351, Genova, Italy, 2001. Springer-Verlag]]

Digital Library

Cited By

Yoo JErnst MJust RFilkov VRay BZhou M(2024)Verifying the Option Type with Rely-Guarantee ReasoningProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695036(367-380)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695036
Schenck RHinnerskov NHenriksen TMadsen MElsman M(2024)AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear ProgrammingProceedings of the ACM on Programming Languages10.1145/36897748:OOPSLA2(1787-1813)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689774
Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Show More Cited By

Recommendations

Flow-sensitive type qualifiers

We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled ...
Flow-insensitive type qualifiers

We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding new, user-specified type qualifiers to programming ...
Checking and inferring local non-aliasing
PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation

In prior work [15] we studied a language construct <tt>restrict</tt> that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation

June 2002

338 pages

ISBN:1581134630

DOI:10.1145/512529

General Chair:
Jens Knoop
Universität Dortmund, Germany
,
Program Chair:
Laurie J. Hendren
McGill University, Canada

ACM SIGPLAN Notices Volume 37, Issue 5
May 2002
326 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/543552
Issue’s Table of Contents

Copyright © 2002 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 May 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI02

Sponsor:

SIGPLAN

PLDI02: ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation

June 17 - 19, 2002

Berlin, Germany

Acceptance Rates

PLDI '02 Paper Acceptance Rate 28 of 169 submissions, 17%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

271
Total Citations
View Citations
861
Total Downloads

Downloads (Last 12 months)55
Downloads (Last 6 weeks)9

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yoo JErnst MJust RFilkov VRay BZhou M(2024)Verifying the Option Type with Rely-Guarantee ReasoningProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695036(367-380)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695036
Schenck RHinnerskov NHenriksen TMadsen MElsman M(2024)AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear ProgrammingProceedings of the ACM on Programming Languages10.1145/36897748:OOPSLA2(1787-1813)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689774
Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Dura AReichenbach CRodríguez GSadayappan PSukumaran-Rajam A(2024)Clog: A Declarative Language for C Static Code CheckersProceedings of the 33rd ACM SIGPLAN International Conference on Compiler Construction10.1145/3640537.3641579(186-197)Online publication date: 17-Feb-2024
https://dl.acm.org/doi/10.1145/3640537.3641579
Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Elsman M(2024)Explicit Effects and Effect Constraints in ReMLProceedings of the ACM on Programming Languages10.1145/36329218:POPL(2370-2394)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632921
Yuan YLu YZhu KHuang HYu LZhao J(2023)A Static Detection Method for SQL Injection Vulnerability Based on Program TransformationApplied Sciences10.3390/app13211176313:21(11763)Online publication date: 27-Oct-2023
https://doi.org/10.3390/app132111763
Emre MBoyland PParekh ASchroeder RDewey KHardekopf B(2023)Aliasing Limits on Translating C to Safe RustProceedings of the ACM on Programming Languages10.1145/35860467:OOPSLA1(551-579)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586046
Kellogg MDaskiewicz DDuc Nguyen LAhmed MErnst M(2023)Pluggable Type Inference for Free2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE56229.2023.00186(1542-1554)Online publication date: 11-Sep-2023
https://doi.org/10.1109/ASE56229.2023.00186
Machiry AKastner JMcCutchen MEline AHeadley KHicks M(2022)C to checked C by 3cProceedings of the ACM on Programming Languages10.1145/35273226:OOPSLA1(1-29)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527322
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