Colin S. Gordon

selected publications

1. 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) 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
2. 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
3. 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