Colin Stebbins Gordon

Contact: [first initial, middle initial, last name] @cs.washington.edu

CV: [pdf]
Google Scholar Author Page
ACM Author Page
DBLP

Useful or interesting links:

Software:

JavaUI
RGref

About Me

I'm a fourth year PhD student interested providing strong static guarantees about program behavior, particularly for concurrent and systems-level code. So I study programming languages. I'm part of the programming languages and software engineering (PLSE) group at UW.

For my thesis, I'm developing an approach to verifying serial and concurrent programs using fine-grained descriptions of interference and capabilities for heap mutation, attached to every reference in a program. My thesis committee consists of Michael Ernst, Dan Grossman, and Matt Parkinson.

In the past I was an undergrad at Brown University, where I worked with Shriram Krishnamurthi and Maurice Herlihy. I've interned with NetApp's filesystem group, the Solaris kernel group at ~~Sun~~ pre-Oracle, and have been both a full-time employee (before grad school) and intern (during grad school) with an operating system incubation group at Microsoft.

News

5/20/13: I will be giving an invited talk at Languages for the Multicore Era (LaME) 2013.
3/4/13: "JavaUI: Effects for Controlling UI Object Access" will appear at ECOOP'13.
2/4/13: "Rely-Guarantee References for Refinement Types over Aliased Mutable Data" will appear at PLDI'13.

Publications

Partial publication lists are also available on Google Scholar, the ACM portal, and DBLP.

Conference Papers

JavaUI: Effects for Controlling UI Object Access.
In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP'13), Montpellier, France. July 2013. To Appear.
Colin S. Gordon, Werner M. Dietl, Michael D. Ernst, and Dan Grossman.
[+abstract] [+bibtex] [pdf | tech report] [code]
Abstract: 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 = {July},
  note = "To Appear."
}
```
Rely-Guarantee References for Refinement Types over Aliased Mutable Data.
In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13), Seattle, WA, USA. June 2013. To Appear.
Colin S. Gordon, Michael D. Ernst, and Dan Grossman.
[+abstract] [+bibtex] [pdf | tech report] [code]
Abstract: 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 modiﬁcation, rely-guarantee references allow types to depend on mutable data while still permitting ﬂexible 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 reﬁnement (subset) types that may depend on mutable data. As a special case, we derive the ﬁrst reference immutability type system with dependent types over immutable data. We show soundness for our approach, and describe experience using relyguarantee 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 = {June},
  note = "To Appear."
}
```
Uniqueness and Reference Immutability for Safe Parallelism.
In Proceedings of the 27th ACM SIGPLAN Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA'12), Tucson, AZ, USA. October 2012.
Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Acceptance rate 26% (59/228).
[+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report | tech report @ msr ] [slides]
[Press: slashdot | reddit | hacker news (most coverage misunderstood the work)]
Abstract: 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 = {October},
  year = 2012,
}
```

Workshop Papers

Static Lock Capabilities for Deadlock Freedom.
In Proceedings of the 8th Workshop on Types in Language Design and Implementation (TLDI'12), Philadelphia, PA, USA. January 2012.
Colin S. Gordon, Michael D. Ernst, and Dan Grossman.
[+abstract] [+bibtex] [acm | acm authorizer | pdf | tech report] [slides] [conference homepage]
Abstract: 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 = {Colin S. Gordon and Michael D. Ernst and Dan Grossman},
  title = {{Static Lock Capabilities for Deadlock Freedom}},
  year = 2012,
  booktitle = {{Workshop on Types in Language Design and Implementation}},
  address = {{Philadelphia, PA, USA}},
  month = "January"
}
```
Formal Semantics for Testing.
In Off the Beaten Track Workshop (OBT'12), Philadelphia, PA, USA. January 2012. Position paper.
Colin S. Gordon.
[+abstract] [+bibtex] [pdf] [slides] [conference homepage | schedule]
Abstract: 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 = {Colin S. Gordon},
  title = {{Formal Semantics for Testing}},
  year = 2012,
  booktitle = {{Off the Beaten Track Workshop}},
  address = {{Philadelphia, PA, USA}},
  month = "January"
}
```
Composition with Consistent Updates for Abstract State Machines.
In Proceedings of the 14th International Workshop on Abstract State Machines (ASM'07), Grimstad, Norway. June 2007.
Colin Gordon, Leo Meyerovich, Joel Weinberger, and Shriram Krishnamurthi. [+abstract] [+bibtex] [pdf] [proceedings]
Abstract: 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="Colin Gordon and Leo Meyerovich and Joel Weinberger and Shriram Krishnamurthi",
  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="June",
  isbn = "978-82-7117-627-3"
}
```

Theses and Technical Reports

JavaUI: Effects for Controlling UI Object Access (Extended Version).
Technical Report UW-CSE-13-04-01, Computer Science and Engineering, University of Washington, Seattle, WA, USA. April 2013.
Colin S. Gordon, Werner M. Dietl, Michael D. Ernst, and Dan Grossman.
[+abstract] [+bibtex] [ dept pdf | dept TRs] [code]
Abstract: 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.
```
@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 = {April},
  year = {2013},
  number = {UW-CSE-13-04-01},
  institution = {{University of Washington}}
}
```
Rely-Guarantee References for Refinement Types Over Aliased Mutable Data (Extended Version).
Technical Report UW-CSE-13-03-02, Computer Science and Engineering, University of Washington, Seattle, WA, USA. March 2013.
Colin S. Gordon, Michael D. Ernst, Dan Grossman.
[+abstract] [+bibtex] [pdf ] [dept pdf | dept TRs]

Abstract: 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 modiﬁcation, rely-guarantee references allow types to depend on mutable data while still permitting ﬂexible 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 reﬁnement (subset) types that may depend on mutable data. As a special case, we derive the ﬁrst reference immutability type system with dependent types over immutable data. We show soundness for our approach, and describe experience using relyguarantee references in a dependently-typed monadic DSL in Coq.
```
@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 = {March},
  year = {2013},
  number = {UW-CSE-13-03-02},
  institution = {{University of Washington}}
}
```
Uniqueness and Reference Immutability for Safe Parallelism (Extended Version).
Technical Report MSR-TR-2012-79, Microsoft Research, Redmond, WA, USA. August 2012.
Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy.
[+abstract] [ pdf | pdf @ msr ]
Abstract: 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.
Static Lock Capabilities for Deadlock Freedom.
Technical Report UW-CSE-11-10-01, Computer Science and Engineering, University of Washington, Seattle, WA, USA. October 2011.
Colin S. Gordon, Michael D. Ernst, Dan Grossman.
[+abstract] [+bibtex] [pdf ] [dept pdf | dept TRs]

Abstract: 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.
```
@techreport{uw-cse-11-10-01,
  author = {Colin S. Gordon and Michael D. Ernst and Dan Grossman},
  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}},
}
```
Type-Safe Stack Traversal for Garbage Collector Implementation.
Brown University Senior Honors Thesis. May 2008. Undergraduate Thesis.
Colin Stebbins Gordon.
[+abstract] [+bibtex] [pdf] [slides] [other honors theses]
Abstract: 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="Colin Stebbins Gordon",
  title={{Type-Safe Stack Inspection for Garbage Collector Implementation}},
  howpublished={Brown University Senior Honors Thesis},
  year=2008,
  month="May",
  note="Undergraduate Thesis"
}
```
ASM Relational Transducer Security Policies.
Technical Report CS-06-12, Computer Science Department, Brown University, Providence, RI, USA. November, 2006.
Meyerovich, L.A., Weinberger, J.H.W., Gordon, C.S., Krishnamurthi, S.
[+abstract] [+bibtex] [pdf ] [department page]
This report is essentially an extended version of Composition with Consistent Updates for Abstract State Machines
Abstract: 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="Leo A. Meyerovich and Joel H. W. Weinberger and 
    Colin S. Gordon and Shriram Krishnamurthi",
  title="{ASM} Relational Transducer Security Policies",
  institution="Computer Science Department, Brown University",
  year=2006,
  number="CS-06-12",
  address="Providence, RI, USA"
}
```

Patents

Merging Containers in a Multi-Container System.
US Patent 7828201. Filed April, 2007, issued November 2010. Assigned to Network Appliance.
Colin Stebbins Gordon, Pratap Vikram Singh, and Donald Alvin Trimmer.
[ Patent at USPTO ]
Data Containerization for Reducing Unused Space in a File System.
US Patent 7739312. Filed April, 2007, issued June 2010. Assigned to Network Appliance.
Colin Stebbins Gordon, Pratap Vikram Singh, and Donald Alvin Trimmer.
[ Patent at USPTO ]

Unpublished Projects

Sadly not everything can (or should) make it to the presses.

Reducing the overhead of runtime instrumentation by running checks asynchronously (2010)
Automatic inference of documentation for useful code properties (2010)
Work towards a type system to check linearizability of lock-free data structure implementations (2008)
Using hardware transactional memory to reduce power consumption in embedded systems (2007-2008)
Dynamic rebalancing of software transactional memory contention management policies based on recent workload (2007)

Industry Experience

Microsoft: Technical Strategy Incubation - Intern, Program analysis work. See OOPSLA'12 publication. (Summer 2011)
Microsoft: Technical Strategy Incubation - Full Time, Kernel developer on an unannounced systems project. Worked on kernel debugger implementation, interrupt handling, post-mortem debugging, platform abstractions, all work interacting with other subsystems. (August 2008 - September 2009)
Sun Microsystems: Solaris Kernel Group - Intern, merged two processor grouping scheduler abstractions. (Summer 2007)
NetApp: Filesystems Group - Intern, designed, documented, and implemented special-purpose filesystem. Resulted in two patents, listed above. (Summer 2006)

Honors

Teaching

University of Washington CSE333: Systems Programming Grad TA, Spring 2011
University of Washington CSEP551: Operating Systems (Graduate-level course) Grad TA, Fall 2009
(a short hiatus from TA work while I was at Microsoft)
Brown University CS190: Software System Design Head TA, Spring 2008 (the particular run I TAed)
Brown University CS167/9: Operating Systems & Operating Systems Lab Head TA, Fall 2007 (students implement a small but full-featured OS kernel)
Brown University CS017/018: Integrated Introduction to Computer Science Head TA, Fall 2006 - Spring 2007
Brown University CS017/018: Integrated Introduction to Computer Science TA, Fall 2005 - Spring 2006
Brown University CS004: Introduction to Scientific Computing TA, Spring 2005 (back when the course was taught in C)

Interesting Readings

Benjamin Pierce's Great Works in Programming Languages collection
Karl Crary's Classic Papers in Programming Languages and Logic course
Patrick Cousot's Abstract Interpretation course (readings section)
Matthew Might's Reading for Graduate Students includes a list of general resources for graduate students, particularly those working in PL, compilers, or static analysis.
Matthias Felleisen's History of Programming Languages course readings
Viktor Vafeiadis and Derek Dreyer's course on Concurrent Program Logics