Publications

2022

1. arXiv

   Preprocessing Source Code Comments for Linguistic Models

   Matskevich, Sergey,  and Gordon, Colin S.

   Aug 2022

   doi arXiv Bib

   @techreport{preprocessingtr,
     author = {Matskevich, Sergey and Gordon, Colin S.},
     title = {Preprocessing Source Code Comments for Linguistic Models},
     institution = {{Computing Research Repository (CoRR)}},
     number = {arXiv cs.SE 2208.11235v2},
     eprint = {2208.11235v2},
     doi = {10.48550/arXiv.2208.11235},
     month = aug,
     year = {2022}
   }

   Details
2. arXiv

   Natural Language Specifications in Proof Assistants

   Gordon, Colin S.,  and Matskevich, Sergey

   May 2022

   doi arXiv Bib

   @techreport{nlspectr,
     author = {Gordon, Colin S. and Matskevich, Sergey},
     title = {Natural Language Specifications in Proof Assistants},
     institution = {{Computing Research Repository (CoRR)}},
     number = {arXiv cs.PL 2205.07811},
     eprint = {2205.07811},
     doi = {10.48550/arXiv.2205.07811},
     month = may,
     year = {2022}
   }

   Details
3. ICSE NIER

   Towards Property-Based Tests in Natural Language

   Gordon, Colin S.

   In 44th IEEE/ACM International Conference on Software Engineering: New Ideas and Emerging Results, ICSE (NIER) May 2022

   Abs doi ieee arXiv Bib PDF Talk on YouTube

   We consider a new approach to generate tests from natural language. Rather than relying on machine learning or templated extraction from structured comments, we propose to apply classic ideas from linguistics to translate natural-language sentences into executable tests. This paper explores the application of combinatory categorial grammars (CCGs) to generating property-based tests. Our prototype is able to generate tests from English descriptions for each example in a textbook chapter on property-based testing.

   @inproceedings{icsenier22,
     author = {Gordon, Colin S.},
     title = {Towards Property-Based Tests in Natural Language},
     booktitle = {44th {IEEE/ACM} International Conference on Software Engineering:
                    New Ideas and Emerging Results, {ICSE} {(NIER)}},
     publisher = {{IEEE}},
     year = {2022},
     ieee = {https://ieeexplore.ieee.org/document/9793513},
     doi = {10.1145/3510455.3512781},
     youtube = {https://youtu.be/uQWuQoR5nbM},
     note = {Acceptance Rate 27\% (26/97). To Appear.}
   }

   Details

2021

1. TOPLAS

   Polymorphic Iterable Sequential Effect Systems

   Gordon, Colin S.

   ACM Transactions on Programming Languages and Systems (TOPLAS), 43(1) Apr 2021

   Abs doi acm arXiv Bib PDF

   Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant. Understanding such systems in terms of a semilattice of effects grounds understanding of the essential issues, and provides guidance when designing new effect systems. By contrast, sequential effect systems — where the order of effects is important — lack an established algebraic characterization. We derive an algebraic characterization from the shape of prior concrete sequential effect systems. We present an abstract polymorphic effect system with singleton effects parameterized by an effect quantale — an algebraic structure with well-defined properties that can model a range of existing sequential effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems. We show that for most effect quantales, there is a free, general notion of iterating a sequential effect, and that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work. Identifying and applying the right algebraic structure led us to subtle insights into the design of sequential effect systems, which provides guidance on non-obvious points of designing sequential effect systems. We also position effect quantales with respect to work on categorical semantics for sequential effect systems, clarifying the distinctions between these systems and our own. In addition, our derived iteration construct should generalize to these semantic structures, addressing limitations of that work.

   @article{toplas21,
     author = {Gordon, Colin S.},
     title = {{Polymorphic Iterable Sequential Effect Systems}},
     year = {2021},
     institution = {{Computing Research Repository (Corr)}},
     //number = {arXiv cs.PL/cs.LO 1808.02010},
     eprint = {1808.02010},
     volume = {43},
     month = apr,
     number = {1},
     articleno = {4},
     archiveprefix = {arXiv},
     primaryclass = {cs.PL},
     acm = {https://dl.acm.org/doi/abs/10.1145/3450272},
     journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
     doi = {10.1145/3450272},
   }

   Details

2020

1. ECOOP

   Designing with Static Capabilities and Effects

   Gordon, Colin S.

   In Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP’20) Jul 2020

   Abs doi Dagstuhl LIPIcs arXiv Bib PDF Talk on YouTube

   Capabilities (whether object or reference capabilities) are fundamentally tools to restrict effects. Thus static capabilities (object or reference) and effect systems take different technical machinery to the same core problem of statically restricting or reasoning about effects in programs. Any time two approaches can in principle address the same sets of problems, it becomes important to understand the trade-offs between the approaches, how these trade-offs might interact with the problem at hand. Experts who have worked in these areas tend to find the trade-offs somewhat obvious, having considered them in context before. However, this kind of design discussion is often written down only implicitly as comparison between two approaches for a specific program reasoning problem, rather than as a discussion of general trade-offs between general classes of techniques. As a result, it is not uncommon to set out to solve a problem with one technique, only to find the other better-suited. We discuss the trade-offs between static capabilities (specifically reference capabilities) and effect systems, articulating the challenges each approach tends to have in isolation, and how these are sometimes mitigated. We also put our discussion in context, by appealing to examples of how these trade-offs were considered in the course of developing prior systems in the area. Along the way, we highlight how seemingly-minor aspects of type systems – weakening/framing and the mere existence of type contexts – play a subtle role in the efficacy of these systems.

   @inproceedings{ecoop20a,
     author = {Gordon, Colin S.},
     title = {{Designing with Static Capabilities and Effects}},
     booktitle = {{Proceedings of the 34th European Conference on Object-Oriented Programming
       (ECOOP'20)}},
     doi = {10.4230/LIPIcs.ECOOP.2020.10},
     year = {2020},
     month = jul,
     lipics = {https://drops.dagstuhl.de/opus/volltexte/2020/13167/},
     note = {Acceptance rate 41\% (29/71)..},
     youtube = {https://youtu.be/Q8ycbdIziWA},
     address = {{Berlin, Germany}}
   }

   Details
2. ECOOP

   Lifting Sequential Effects to Control Operators

   Gordon, Colin S.

   In Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP’20) Jul 2020

   Abs doi Dagstuhl LIPIcs arXiv Bib PDF Talk on YouTube

   Sequential effect systems are a class of effect system that exploits information about program order, rather than discarding it as traditional commutative effect systems do. This extra expressive power allows effect systems to reason about behavior over time, capturing properties such as atomicity, unstructured lock ownership, or even general safety properties. While we now understand the essential denotational (categorical) models fairly well, application of these ideas to real software is hampered by the variety of source level control flow constructs and control operators in real languages. We address this new problem by appeal to a classic idea: macro-expression of commonly-used programming constructs in terms of control operators. We give an effect system for a subset of Racket’s tagged delimited control operators, as a lifting of an effect system for a language without direct control operators. This gives the first account of sequential effects in the presence of general control operators. Using this system, we also re-derive the sequential effect system rules for control flow constructs previously shown sound directly, and derive sequential effect rules for new constructs not previously studied in the context of source-level sequential effect systems. This offers a way to directly extend source-level support for sequential effect systems to real programming languages.

   @inproceedings{ecoop20b,
     author = {Gordon, Colin S.},
     title = {{Lifting Sequential Effects to Control Operators}},
     booktitle = {{Proceedings of the 34th European Conference on Object-Oriented Programming
       (ECOOP'20)}},
     doi = {10.4230/LIPIcs.ECOOP.2020.23},
     lipics = {https://drops.dagstuhl.de/opus/volltexte/2020/13180/},
     year = {2020},
     note = {Acceptance rate 41\% (29/71)..},
     month = jul,
     youtube = {https://youtu.be/1JZhmGh39Hw},
     address = {{Berlin, Germany}}
   }

   Details

2019

1. AGERE

   Modal Assertions for Actor Correctness

   Gordon, Colin S.

   In ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE 2019) Oct 2019

   Abs doi acm Bib PDF Code

   The actor model is a well-established way to approach to modularly designing and implementing concurrent and/or distributed systems, seeing increasing adoption in industry. But deductive verification tailored to actor programs remains underexplored; general concurrent logics could be used, but the logics are complex and full of features to reason about behaviors the actor model strives to avoid. We explore a relatively lightweight approach of extending a system for proving sequential program correctness with means to prove safety properties of distributed actor programs (currently, assuming no faults). We borrow ideas from hybrid logic, a modal logic for stating assertions are true at a particular point in a model (in this case, a particular actor’s local state). To make such assertions useful, we stabilize them using rely-guarantee-style reasoning over local actor states, and only permit sending stable versions of these assertions to other actors. By carefully restricting the formation of assertions that a proposition is true at a certain actor, we avoid the need for actors to handle each others’ rely-guarantee relations explicitly. We find that almost all of the required restrictions either fall out of established reference immutability techniques or can be implemented as a Dafny library, and outline the minor additional extensions that would be required for a sound implementation. We use this library to verify an actor variant of a classic rely-guarantee example (lower-bounding a montonic counter).

   @inproceedings{agere19,
     title = {{Modal Assertions for Actor Correctness}},
     author = {Gordon, Colin S.},
     booktitle = {{ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and
           Decentralized Control (AGERE 2019)}},
     address = {Athens, Greece},
     month = oct,
     year = {2019},
     doi = {10.1145/3358499.3361221},
     acm = {https://dl.acm.org/citation.cfm?id=3361221},
   }

   Details
2. ESOP

   A Type System for Read-Copy-Update Concurrency

   Kuru, Ismail,  and Gordon, Colin S.

   In European Symposium on Programming (ESOP 2019) Apr 2019

   Abs doi springer arXiv Bib PDF

   Memory management in lock-free data structures remains a major challenge in concurrent programming. Design techniques including read-copy-update (RCU) and hazard pointers provide workable solutions, and are widely used to great effect. These techniques rely on the concept of a grace period: nodes that should be freed are placed on a \emphdeferred free list, and all threads obey a protocol to ensure that the deallocating thread can detect when all possible readers have completed their use of the object. This provides an approach to safe deallocation, but only when these subtle protocols are implemented correctly. We present a static type system to ensure correct use of RCU memory management: that nodes removed from a data structure are always scheduled for subsequent deallocation, and that nodes are scheduled for deallocation at most once. As part of our soundness proof, we give an abstract semantics for RCU memory management primitives which captures the fundamental properties of RCU. Our type system allows us to give the first proofs of memory safety for RCU linked list and binary search tree implementations without requiring full verification.

   @inproceedings{esop19,
     title = {{A Type System for Read-Copy-Update Concurrency}},
     author = {Kuru, Ismail and Gordon, Colin S.},
     booktitle = {{European Symposium on Programming (ESOP 2019)}},
     month = apr,
     note = {Acceptance Rate 32.6\% (28/86).},
     address = {Prague, Czech Republic},
     year = {2019},
     doi = {10.1007/978-3-030-17184-1_4},
     springer = {https://link.springer.com/chapter/10.1007/978-3-030-17184-1_4}
   }

   Details

2018

1. arXiv

   A Type System for Read-Copy-Update Concurrency

   Kuru, Ismail,  and Gordon, Colin S.

   Dec 2018

   arXiv Bib PDF

   @techreport{rcupapertr,
     title = {{A Type System for Read-Copy-Update Concurrency}},
     author = {Kuru, Ismail and Gordon, Colin S.},
     institution = {{Computing Research Repository (Corr)}},
     number = {arXiv cs.PL 1811.11853},
     eprint = {1811.11853},
     month = dec,
     year = {2018}
   }

   Details
2. arXiv

   Sequential Effect Systems with Control Operators

   Gordon, Colin S.

   Dec 2018

   arXiv Bib PDF

   @techreport{controltr,
     title = {{Sequential Effect Systems with Control Operators}},
     author = {Gordon, Colin S.},
     institution = {{Computing Research Repository (CoRR)}},
     number = {arXiv cs.PL 1811.12285},
     eprint = {1811.12285},
     month = dec,
     year = {2018}
   }

   Details
3. NL4SE

   Generating Comments from Source Code

   Matskevich, Sergey,  and Gordon, Colin S.

   In ACM Workshop on Natural Language for Software Engineering (NL4SE) Nov 2018

   Abs doi acm arXiv Bib PDF

   Good comments help developers understand software faster and provide better maintenance. However, comments are often missing, generally inaccurate, or out of date. Many of these problems can be avoided by automatic comment generation. This paper presents a method to generate informative comments directly from the source code using general-purpose techniques from natural language processing. We generate comments using an existing natural language model that couples words with their individual logical meaning and grammar rules, allowing comment generation to proceed by search from declarative descriptions of program text. We evaluate our algorithm on several classic algorithms implemented in Python.

   @inproceedings{nl4se18,
     title = {{Generating Comments from Source Code}},
     author = {Matskevich, Sergey and Gordon, Colin S.},
     booktitle = {ACM Workshop on Natural Language for Software Engineering (NL4SE)},
     doi = {10.1145/3283812.3283822},
     year = {2018},
     month = nov,
     address = {{Lake Buena Vista, FL, USA}},
     acm = {https://dl.acm.org/citation.cfm?doid=3283812.3283822},
   }

   Details
4. OBT

   Synthesizing Program-Specific Static Analyses

   Gordon, Colin S.

   In Off the Beaten Track Workshop (OBT’18) Jan 2018

   Abs arXiv Bib PDF Slides

   Designing a static analysis is generally a substantial undertaking, requiring significant expertise in both program analysis and the domain of interest, and significant development resources. As a result, most program analyses target properties that are universally of interest (e.g., absence of null pointer dereference) or nearly so (e.g., deadlock freedom). However, many interesting program properties that would benefit from static checking are specific to individual programs, or sometimes programs utilizing a certain library. It is impractical to devote program analysis and verification experts to these problems. We propose instead to work on example-based synthesis of program analyses within well-understood domains like type qualifier systems and effect systems. The dynamic behaviors behind the classes of problems these systems prevent correspond to examples that developers who lack expertise in static analysis can readily provide (data flow paths, or stack traces).

   @inproceedings{obt18,
     author = {Gordon, Colin S.},
     title = {{Synthesizing Program-Specific Static Analyses}},
     booktitle = {{Off the Beaten Track Workshop (OBT'18)}},
     address = {{Los Angeles, CA, USA}},
     year = {2018},
     month = jan,
     url = {https://popl18.sigplan.org/event/obt-2018-synthesizing-program-specific-static-analyses},
     note = {Position paper.}
   }

   Details

2017

1. TOPLAS

   Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement Types

   Gordon, Colin S., Ernst, Michael D.,  Grossman, Dan and 1 more author

   ACM Transactions on Programming Languages and Systems (TOPLAS), 39(3) Jul 2017

   Abs doi acm Bib PDF Code More Code Talk on YouTube Slides

   We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive enough to accommodate several standard benchmarks with only minor workarounds. The invariants enforced by the types enable an ahead-of-time compiler to carry out optimizations typically beyond the reach of static compilers for dynamic languages. Unlike previous inference techniques for prototype inheritance, our algorithm uses a combination of lower and upper bound propagation to infer types and discover type errors in all code, including uninvoked functions. The inference is expressed in a simple constraint language, designed to leverage off-the-shelf fixed point solvers. We prove soundness for both the type system and inference algorithm. An experimental evaluation showed that the inference is powerful, handling the aforementioned benchmarks with no manual type annotation, and that the inferred types enable effective static compilation.

   @article{toplas17,
     author = {Gordon, Colin S. and Ernst, Michael D. and Grossman, Dan and Parkinson, Matthew J.},
     title = {{Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement
           Types}},
     year = {2017},
     journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
     volume = {39},
     number = {3},
     url = {http://doi.acm.org/10.1145/3064850},
     doi = {10.1145/3064850},
     month = jul,
     note = {2016 Impact Factor (JCR): 3.033.},
     acm = {http://doi.acm.org/10.1145/3064850},
     youtube = {https://youtu.be/dar-mVn5N8U},
   }

   Details
2. ECOOP

   A Generic Approach to Flow-Sensitive Polymorphic Effects

   Gordon, Colin S.

   In Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP’17) Jun 2017

   Abs doi Dagstuhl LIPIcs arXiv Bib PDF Talk on YouTube Slides

   Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant. Understanding such systems in terms of a lattice of effects grounds understanding of the essential issues, and provides guidance when designing new effect systems. By contrast, sequential effect systems - where the order of effects is important - lack a clear algebraic characterization. We derive an algebraic characterization from the shape of prior concrete sequential effect systems. We present an abstract polymorphic effect system with singleton effects parameterized by an effect quantale - an algebraic structure with well-defined properties that can model a range of existing order-sensitive effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems. We show that effect quantales provide a free, general notion of iterating a sequential effect, and that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work. Identifying and applying the right algebraic structure led us to subtle insights into the design of order-sensitive effect systems, which provides guidance on non-obvious points of designing order-sensitive effect systems. Effect quantales have clear relationships to the recent category theoretic work on order-sensitive effect systems, but are explained without recourse to category theory. In addition, some of our derived constructs (iteration) should generalize to these semantic structures, addressing limitations of that work.

   @inproceedings{ecoop17,
     author = {Gordon, Colin S.},
     title = {{A Generic Approach to Flow-Sensitive Polymorphic Effects}},
     booktitle = {{Proceedings of the 31st European Conference on Object-Oriented Programming
       (ECOOP'17)}},
     year = {2017},
     month = jun,
     address = {{Barcelona, Spain}},
     youtube = {https://youtu.be/nQOrOdsi0To},
     lipics = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7256},
     note = {Acceptance Rate 33.3\% (27/81).},
     doi = {10.4230/LIPIcs.ECOOP.2017.13},
     url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7256}
   }

   Details
3. A Generic Approach to Flow-Sensitive Polymorphic Effects (Extended Version)

   Gordon, Colin S.

   May 2017

   arXiv Bib PDF

     title = {{A Generic Approach to Flow-Sensitive Polymorphic Effects (Extended Version)}},
     author = {Gordon, Colin S.},
     year = {2017},
     month = may,
     institution = {{Computing Research Repository (CoRR)}},
     number = {arXiv cs.PL 1705.02264},
     eprint = {1705.02264},
   }

   Details

2016

1. OOPSLA

   Type Inference for Static Compilation of JavaScript

   Chandra, Satish,  Gordon, Colin S.,  Jeannin, Jean-Baptiste and 4 more authors

   In Proceedings of the 2016 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016) Nov 2016

   Abs doi arXiv Bib PDF

   We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive enough to accommodate several standard benchmarks with only minor workarounds. The invariants enforced by the types enable an ahead-of-time compiler to carry out optimizations typically beyond the reach of static compilers for dynamic languages. Unlike previous inference techniques for prototype inheritance, our algorithm uses a combination of lower and upper bound propagation to infer types and discover type errors in all code, including uninvoked functions. The inference is expressed in a simple constraint language, designed to leverage off-the-shelf fixed point solvers. We prove soundness for both the type system and inference algorithm. An experimental evaluation showed that the inference is powerful, handling the aforementioned benchmarks with no manual type annotation, and that the inferred types enable effective static compilation.

   @inproceedings{oopsla16,
     author = {Chandra, Satish and Gordon, Colin S. and Jeannin, Jean-Baptiste and Schlesinger, Cole and Sridharan, Manu and Tip, Frank and Choi, Young-Il},
     title = {{Type Inference for Static Compilation of JavaScript}},
     booktitle = {{Proceedings of the 2016 ACM Conference on Object-Oriented Programming, Systems,
           Languages, and Applications (OOPSLA 2016)}},
     month = nov,
     year = {2016},
     doi = {10.1145/2983990.2984017},
     eprint = {1608.07261},
     address = {{Amsterdam, The Netherlands}},
     url = {http://dl.acm.org/citation.cfm?doid=2983990.2984017},
     note = {Acceptance Rate 25.6\% (52/203).}
   }

   Details
2. Type Inference for Static Compilation of JavaScript (Extended Version)

   Chandra, Satish,  Gordon, Colin S.,  Jeannin, Jean-Baptiste and 4 more authors

   Aug 2016

   arXiv Bib PDF

     author = {Chandra, Satish and Gordon, Colin S. and Jeannin, Jean-Baptiste and Schlesinger, Cole and Sridharan, Manu and Tip, Frank and Choi, Young-Il},
     title = {{Type Inference for Static Compilation of JavaScript (Extended Version)}},
     institution = {{Computing Research Repository (CoRR)}},
     number = {arXiv cs.PL 1608.07261},
     month = aug,
     year = {2016},
     eprint = {1608.07261},
   }

   Details
3. ECOOP

   Trace Typing An Approach for Evaluating Retrofitted Type Systems

   Andreasen, Esben,  Gordon, Colin S.,  Chandra, Satish and 3 more authors

   In Proceedings of the 30th European Conference on Object-Oriented Programming (ECOOP’16) Jul 2016

   Abs doi Dagstuhl LIPIcs Bib PDF Talk on YouTube

   Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a delicate balance between disallowing certain coding patterns to keep the type system simple, or including them at the expense of additional complexity and effort. Thus far, the process for designing retrofitted type systems has been largely ad hoc, because evaluating multiple variations of a type system on large bodies of existing code is a significant undertaking. We present trace typing: a framework for automatically and quantitatively evaluating variations of a retrofitted type system on large code bases. The trace typing approach involves gathering traces of program executions, inferring types for instances of variables and expressions occurring in a trace, and merging types according to merge strategies that reflect specific (combinations of) choices in the source-level type system design space. We evaluated trace typing through several experiments. We compared several variations of type systems retrofitted onto JavaScript, measuring the number of program locations with type errors in each case on a suite of over fifty thousand lines of JavaScript code. We also used trace typing to validate and guide the design of a new retrofitted type system that enforces fixed object layout for JavaScript objects. Finally, we leveraged the types computed by trace typing to automatically identify tag tests - dynamic checks that refine a type - and examined the variety of tests identified.

   @inproceedings{ecoop16,
     author = {Andreasen, Esben and Gordon, Colin S. and Chandra, Satish and Sridharan, Manu and Tip, Frank and Sen, Koushik},
     title = {{Trace Typing An Approach for Evaluating Retrofitted Type Systems}},
     year = {2016},
     booktitle = {{Proceedings of the 30th European Conference on Object-Oriented Programming
       (ECOOP'16)}},
     month = jul,
     address = {{Rome, Italy}},
     doi = {10.4230/LIPIcs.ECOOP.2016.1},
     eprint = {1605.01362},
     lipics = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=6095},
     youtube = {https://www.youtube.com/watch?v=ijh023VRo8w&index=15&list=PL7gvT44-cjMPnfdKGDfcT9bW-QoIIzJG8},
     note = {Acceptance Rate 31.6\% (25/79).}
   }

   Details
4. Trace Typing An Approach for Evaluating Retrofitted Type Systems (Extended Version)

   Andreasen, Esben,  Gordon, Colin S.,  Chandra, Satish and 3 more authors

   May 2016

   arXiv Bib PDF

   @techreport{sra-csic-2016-001,
     author = {Andreasen, Esben and Gordon, Colin S. and Chandra, Satish and Sridharan, Manu and Tip, Frank and Sen, Koushik},
     title = {{Trace Typing An Approach for Evaluating Retrofitted Type Systems (Extended Version)}},
     year = {2016},
     month = may,
     number = {SRA-CSIC-2016-001},
     institution = {{Samsung Research America}},
     note = {Also available from Computing Research Repository (CoRR), arXiv cs.PL 1605.01362.},
     eprint = {1605.01362},
   }

   Details
5. Operating System Support for Contracts

   Duffy, John J., Parsons, Jared Porter,  Gordon, Colin Stebbins and 4 more authors

   Mar 2016

   Bib

   @patent{oscontracts16,
     author = {Duffy, John J. and Parsons, Jared Porter and Gordon, Colin Stebbins and Bromfield, Alexander Daniel and Taillefer, Martin and Bartolomeo, David Allen and Barnett, Michael},
     title = {Operating System Support for Contracts},
     note = {US Patent Number 9286039.  Filed March 14, 2013.  Assigned to Microsoft
           Corporation.},
     month = mar,
     year = {2016},
     howpublished = {Patent}
   }

   Details

2014

1. Verifying Concurrent Programs by Controlling Alias Interference

   Gordon, Colin S.

   Aug 2014

   Abs UW ResearchWorks Archive hdl Bib PDF

   This dissertation proposes a family of techniques for static verification of sequential and concurrent imperative programs by leveraging fine-grained characterizations of mutation. The key idea is that by attaching to each reference in a program (1) a restriction on mutations permitted using that reference, and (2) a characterization of possible interference through other aliases, a type system can reason about what properties are preserved by all mutations in a program. This thesis develops four variations on this idea: (1) We adapt reference immutability to support data-race-free concurrent programming. (2) We generalize reference immutability to rely-guarantee references, allowing two-state invariants to express usage restrictions between read-only and arbitrary mutation. (3) We extend rely-guarantee references to prove invariants and functional correctness of lock-free concurrent data structures. (4) We evaluate rely-guarantee references’ utility for existing Haskell programs. Together these variations show that reasoning about aliasing and reasoning about concurrent (imperative) programs are the same fundamental challenge, and that by taking the right foundational approach to reasoning about sequential programs, the gap to reasoning about concurrent programs is significantly reduced.

   @phdthesis{dissertation,
     author = {Gordon, Colin S.},
     title = {{Verifying Concurrent Programs by Controlling Alias Interference}},
     otherpub = {UW ResearchWorks Archive},
     otherpublink = {https://digital.lib.washington.edu/researchworks/handle/1773/26020},
     hdl = {1773/26020},
     year = {2014},
     month = aug,
     school = {{University of Washington}},
     address = {{Seattle, WA, USA}},
     url = {https://digital.lib.washington.edu/researchworks/handle/1773/26020},
   }

   Details

2013

1. ECOOP

   JavaUI: Effects for Controlling UI Object Access

   Gordon, Colin S., Dietl, Werner,  Ernst, Michael D. and 1 more author

   In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP’13) Jul 2013

   Abs doi Bib PDF Code

   Most graphical user interface (GUI) libraries forbid accessing UI elements from threads other than the UI event loop thread. Violat- ing this requirement leads to a program crash or an inconsistent UI. Unfortunately, such errors are all too common in GUI programs. We present the first type and effect system that prevents non-UI threads from accessing UI objects or invoking UI-thread-only methods. The type system still permits non-UI threads to hold and pass references to UI objects. We implemented this type system for Java and annotated 8 Java programs (over 140KLOC) for the type system, including several of the most popular Eclipse plugins. We confirmed bugs found by unsound prior work, found an additional bug and code smells, and demonstrated that the annotation burden is low. We also describe code patterns our effect system handles less gracefully or not at all, which we believe offers lessons for those applying other effect systems to existing code.

   @inproceedings{ecoop13,
     title = {{JavaUI: Effects for Controlling UI Object Access}},
     author = {Gordon, Colin S. and Dietl, Werner and Ernst, Michael D. and Grossman, Dan},
     year = {2013},
     booktitle = {{Proceedings of the 27th European Conference on Object-Oriented Programming
       (ECOOP'13)}},
     address = {{Montpellier, France}},
     month = jul,
     doi = {10.1007/978-3-642-39038-8_8},
     note = {Acceptance Rate 25\% (29/116).},
     url = {http://link.springer.com/chapter/10.1007/978-3-642-39038-8_8}
   }

   Details
2. PLDI

   Rely-Guarantee References for Refinement Types Over Aliased Mutable Data

   Gordon, Colin S., Ernst, Michael D.,  and Grossman, Dan

   In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’13) Jun 2013

   Abs doi Bib PDF Code

   Reasoning about side effects and aliasing is the heart of verifying imperative programs. Unrestricted side effects through one reference can invalidate assumptions about an alias. We present a new type system approach to reasoning about safe assumptions in the presence of aliasing and side effects, unifying ideas from reference immutability type systems and rely-guarantee program logics. Our approach, rely-guarantee references, treats multiple references to shared objects similarly to multiple threads in rely-guarantee program logics. We propose statically associating rely and guarantee conditions with individual references to shared objects. Multiple aliases to a given object may coexist only if the guarantee condition of each alias implies the rely condition for all other aliases. We demonstrate that existing reference immutability type systems are special cases of rely-guarantee references. In addition to allowing precise control over state modification, rely-guarantee references allow types to depend on mutable data while still permitting flexible aliasing. Dependent types whose denotation is stable over the actions of the rely and guarantee conditions for a reference and its data will not be invalidated by any action through any alias. We demonstrate this with refinement (subset) types that may depend on mutable data. As a special case, we derive the first reference immutability type system with dependent types over immutable data. We show soundness for our approach, and describe experience using rely-guarantee references in a dependently-typed monadic DSL in Coq.

   @inproceedings{pldi13,
     title = {{Rely-Guarantee References for Refinement Types Over Aliased Mutable Data}},
     author = {Gordon, Colin S. and Ernst, Michael D. and Grossman, Dan},
     year = {2013},
     booktitle = {{Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and
       Implementation (PLDI'13)}},
     address = {{Seattle, WA, USA}},
     month = jun,
     doi = {10.1145/2491956.2462160},
     note = {Acceptance Rate 17\% (46/267).},
     url = {http://dl.acm.org/citation.cfm?id=2462160}
   }

   Details
3. JavaUI: Effects for Controlling UI Object Access (Extended Version)

   Gordon, Colin S., Dietl, Werner,  Ernst, Michael D. and 1 more author

   Apr 2013

   Bib PDF

   @techreport{uw-cse-13-04-01,
     author = {Gordon, Colin S. and Dietl, Werner and Ernst, Michael D. and Grossman, Dan},
     title = {{JavaUI: Effects for Controlling UI Object Access (Extended Version)}},
     month = apr,
     year = {2013},
     number = {UW-CSE-13-04-01},
     institution = {{University of Washington}},
     url = {ftp://ftp.cs.washington.edu/tr/2013/03/UW-CSE-13-04-01.PDF}
   }

   Details
4. Rely-Guarantee References for Refinement Types Over Aliased Mutable Data (Extended Version)

   Gordon, Colin S., Ernst, Michael D.,  and Grossman, Dan

   Mar 2013

   Bib PDF

   @techreport{uw-cse-13-03-02,
     author = {Gordon, Colin S. and Ernst, Michael D. and Grossman, Dan},
     title = {{Rely-Guarantee References for Refinement Types Over Aliased Mutable Data (Extended Version)}},
     month = mar,
     year = {2013},
     number = {UW-CSE-13-03-02},
     institution = {{University of Washington}},
     url = {ftp://ftp.cs.washington.edu/tr/2013/03/UW-CSE-13-03-02.PDF}
   }

   Details
5. Merging Containers in a Multi-Container System

   Gordon, Colin Stebbins, Singh, Pratap Vikram,  and Trimmer, Donald Alvin

   Feb 2013

   Bib

   @patent{merging10,
     author = {Gordon, Colin Stebbins and Singh, Pratap Vikram and Trimmer, Donald Alvin},
     title = {Merging Containers in a Multi-Container System},
     note = {US Patent Number US8370401B2. Filed October, 2010.  Assigned to Network Appliance, Inc.},
     month = feb,
     year = {2013},
     howpublished = {Patent}
   }

   Details

2012

1. Uniqueness and Reference Immutability for Safe Parallelism (Extended Version)

   Gordon, Colin S., Parkinson, Matthew J.,  Parsons, Jared and 2 more authors

   Oct 2012

   Bib PDF

   @techreport{msr-tr-2012-79,
     title = {{Uniqueness and Reference Immutability for Safe Parallelism (Extended Version)}},
     author = {Gordon, Colin S. and Parkinson, Matthew J. and Parsons, Jared and Bromfield, Aleks and Duffy, Joe},
     institution = {{Microsoft Research}},
     month = oct,
     year = {2012},
     number = {MSR-TR-2012-79},
     url = {http://research.microsoft.com/apps/pubs/default.aspx?id=170528}
   }

   Details
2. OOPSLA

   Uniqueness and Reference Immutability for Safe Parallelism

   Gordon, Colin S., Parkinson, Matthew J.,  Parsons, Jared and 2 more authors

   In Proceedings of the 2012 ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA’12) Oct 2012

   Abs doi Bib PDF

   A key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread. In this paper, we present a type system to restrict the updates to memory to prevent these unintended side-effects. We provide a novel combination of immutable and unique (isolated) types that ensures safe parallelism (race freedom and deterministic execution). The type system includes support for polymorphism over type qualifiers, and can easily create cycles of immutable objects. Key to the system’s flexibility is the ability to recover immutable or externally unique references after violating uniqueness without any explicit alias tracking. Our type system models a prototype extension to C# that is in active use by a Microsoft team. We describe their experiences building large systems with this extension. We prove the soundness of the type system by an embedding into a program logic.

   @inproceedings{oopsla12,
     title = {{Uniqueness and Reference Immutability for Safe Parallelism}},
     author = {Gordon, Colin S. and Parkinson, Matthew J. and Parsons, Jared and Bromfield, Aleks and Duffy, Joe},
     booktitle = {{Proceedings of the 2012 ACM International Conference on Object Oriented Programming,
       Systems, Languages, and Applications (OOPSLA'12)}},
     address = {{Tucson, AZ, USA}},
     month = oct,
     year = {2012},
     doi = {10.1145/2384616.2384619},
     note = {Acceptance Rate 26\% (59/228).},
     url = {http://dl.acm.org/citation.cfm?id=2384619}
   }

   Details
3. TLDI

   Static Lock Capabilities for Deadlock Freedom

   Gordon, Colin S., Ernst, Michael D.,  and Grossman, Dan

   In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI’12) Jan 2012

   Abs doi Bib PDF

   We present a technique - lock capabilities - for statically verifying that multithreaded programs with locks will not deadlock. Most previous work is built around a strict total order on all locks held simultaneously by a thread, but such an invariant often does not hold with fine-grained locking, especially when data-structure mutations change the order locks are acquired. Lock capabilities support idioms that use fine-grained locking, such as mutable binary trees, circular lists, and arrays where each element has a different lock. Lock capabilities do not enforce a total order and do not prevent external references to data-structure nodes. Instead, the technique reasons about static capabilities, where a thread already holding locks can attempt to acquire another lock only if its capabilities allow it. Acquiring one lock may grant a capability to acquire further locks, and in data-structures where heap shape affects safe locking orders, we can use the heap structure to induce the capability-granting relation. Deadlock-freedom follows from ensuring that the capability-granting relation is acyclic. Where necessary, we restrict aliasing with a variant of unique references to allow strong updates to the capability-granting relation, while still allowing other aliases that are used only to acquire locks while holding no locks. We formalize our technique as a type-and-effect system, demonstrate it handles realistic challenging idioms, and use syntactic techniques (type preservation) to show it soundly prevents deadlock.

   @inproceedings{tldi12,
     author = {Gordon, Colin S. and Ernst, Michael D. and Grossman, Dan},
     title = {{Static Lock Capabilities for Deadlock Freedom}},
     year = {2012},
     booktitle = {{Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12)}},
     address = {{Philadelphia, PA, USA}},
     month = jan,
     doi = {10.1145/2103786.2103796},
     url = {http://dl.acm.org/citation.cfm?id=2103796}
   }

   Details
4. OBT

   Formal Semantics for Testing

   Gordon, Colin S.

   In Off the Beaten Track Workshop (OBT’12) Jan 2012

   Abs Bib PDF

   Software testing constitutes a substantial portion of the real world work of developing software. There has been much research aimed at partially-automating testing (random test generation, etc.). However, relatively little of it pays attention to precise semantics for languages or tests. Algorithms are described informally as pseudocode, and there is limited understanding of the relative power of many of the testing techniques in the literature. We outline a correspondence between tests and formal language semantics, and argue that techniques from programming language research are likely to advance our understanding of existing testing techniques and help to propose new techniques. We also argue that software tests can be a useful aid to formal verification.

   @inproceedings{obt12,
     author = {Gordon, Colin S.},
     title = {{Formal Semantics for Testing}},
     year = {2012},
     booktitle = {{Off the Beaten Track Workshop (OBT'12)}},
     address = {{Philadelphia, PA, USA}},
     month = jan,
     note = {Position paper.},
   }

   Details

2011

1. Static Lock Capabilities for Deadlock Freedom

   Gordon, Colin S., Ernst, Michael D.,  and Grossman, Dan

   Jan 2011

   Bib PDF

   @techreport{uw-cse-11-10-01,
     author = {Gordon, Colin S. and Ernst, Michael D. and Grossman, Dan},
     title = {{Static Lock Capabilities for Deadlock Freedom}},
     year = {2011},
     number = {UW-CSE-11-10-01},
     institution = {{Computer Science and Engineering, University of Washington}},
     address = {{Seattle, WA, USA}},
     url = {ftp://ftp.cs.washington.edu/tr/2011/10/UW-CSE-11-10-01.PDF}
   }

   Details

2008

1. Type-Safe Stack Traversal for Garbage Collector Implementation

   Gordon, Colin Stebbins

   May 2008

   Abs Bib PDF

   Garbage collectors are an important part of many modern language runtimes. Essentially all tools for developing and debugging programs using garbage collection assume the correctness of the collector, and therefore provide no means for detecting garbage collector errors. As a result it is especially important that garbage collector implementations be free of errors. This goal is even more challenging in the face of the typical implementation strategy for collectors: implementation in C, making error-prone inferences from complex bit patterns, where an error could result in dereferencing an invalid pointer or corrupting program data. One approach to reducing errors in collector implementation is to improve both the type-safety and memory-safety of garbage collector implementations. Prior work in this direction has focused on the use of modern type systems to statically detect errors in the collector code at compile time, but has practical shortcomings. The prior work replaces the standard machine stack with a heap allocated data structure to avoid unsafe walks of the native stack. Traversal of the runtime stack is normally not possible in higher-level languages because they trade the flexibility of arbitrary memory access - typically used to gather a root set from a runtime stack - for the safety of being unable to cause memory access errors. We present a method for addressing the safe stack traversal problem at the compiler level, by lifting actual machine stack frames up to the level of explicit data structures in Standard ML, such that complete stack traversal can be performed with minimal unsafe code. We implement a garbage collector in the ML Kit using the techniques described and provide details on key parts of the implementation.

   @misc{ugradthesis,
     author = {Gordon, Colin Stebbins},
     title = {{Type-Safe Stack Traversal for Garbage Collector Implementation}},
     howpublished = {Brown University Senior Honors Thesis},
     year = {2008},
     month = may,
     note = {Undergraduate Thesis},
   }

   Details

2007

1. ASM

   Composition with Consistent Updates for Abstract State Machines

   Gordon, Colin, Meyerovich, Leo,  Weinberger, Joel and 1 more author

   In Proceedings of the 14th International Workshop on Abstract State Machines (ASM’07) Jun 2007

   Abs Bib PDF

   Abstract State Machines (ASMs) offer a formalism for describing state transitions over relational structures. This makes them promising for modeling system features such as access control, especially in an environment where the policy’s outcome depends on the evolving state of the system. The current notions of modularity for asms, however, provide insufficiently strong guarantees of consistency in the face of parallel update requests. We present a real-world context that illustrates this problem, discuss desirable properties for composition in this context, describe an operator that exhibits these properties, formalize its meaning, and outline its implementation strategy.

   @inproceedings{asm07,
     author = {Gordon, Colin and Meyerovich, Leo and Weinberger, Joel and Krishnamurthi, Shriram},
     title = {{Composition with Consistent Updates for Abstract State Machines}},
     booktitle = {Proceedings of the 14th International Workshop on Abstract State
         Machines (ASM'07)},
     address = {Grimstad, Norway},
     year = {2007},
     month = jun,
     url = {http://cs.brown.edu/~sk/Publications/Papers/Published/gmws-comp-cons-upd-asm/}
   }

   Details

2006

1. ASM Relational Transducer Security Policies

   Meyerovich, Leo A., Weinberger, Joel H. W.,  Gordon, Colin S. and 1 more author

   Jun 2006

   Abs Bib PDF

   We present a model of the security policy for the Web-based Continue conference management tool. The policy model and properties are written as ASM Relational Transducers, which we extend with a module system in order to simplify the handling of conflicting updates. We assume prior familiarity with the security policy concerns surrounding Continue. First, we review the ASM Relational Transducer modeling and property language. Then we describe the basic structure of our policy implementation and demonstrate the ability to model useful properties in the original core ASM language. We exploring the use of the unmodified modeling language in a security policy context and describe typical ASM Relational Transducer complexity concerns and how these minimally impact our implementation. Next, we discuss difficulties encountered in representing our policy and properties in the standard ASM language, including our implementation in the appendices. Following the description of adapting ASMs for use in security modeling, we introduce policy modules and a composition operator to overcome the difficulty of programming in the original language known as the consistent update problem. Finally, we describe a reduction from our extended language to the original language, and prove it satisfies our required correctness property.

   @techreport{cs06-12,
     author = {Meyerovich, Leo A. and Weinberger, Joel H. W. and Gordon, Colin S. and Krishnamurthi, Shriram},
     title = {{ASM Relational Transducer Security Policies}},
     institution = {Computer Science Department, Brown University},
     year = {2006},
     number = {CS-06-12},
     address = {Providence, RI, USA},
   }

   Details