Colin Stebbins Gordon

About Me

I'm a third year PhD student interested primarily in improving software reliability by providing guarantees of interesting and useful properties of programs. I'm particularly interested in applying these techniques to parallel programs, operating system kernels, language runtimes, and security-critical code. So I study programming languages. I'm part of the programming languages (WASP) and software engineering (UW SE) groups at UW.

I'm currently working with Michael Ernst and Dan Grossman on a capability type system to prevent deadlock. The system uses static capabilities that are available for duration of a lock acquisition, and permit the further acquisition of specific additional locks. We are also using a variation on unique references that permit strong updates to part of a type (for example, which capability allows a particular lock to be acquired) while allowing aliasing at a less complete type (for example, that the referent is a lock, which may still be acquired by a thread holding no other locks).

In the past I was an undergrad at Brown University. While I was there I worked with Shriram Krishnamurthi and the Brown PLT group on several programming language and program analysis projects. I also worked with Maurice Herlihy on software and hardware transactional memory. In between all those things I TAed a number of courses and did internships in NetApp's filesystem group and the Solaris kernel group at Sun. After finishing undergrad I spent a bit over a year working on an operating system incubation project at Microsoft before starting at UW CSE.

Publications

Refereed

Colin S. Gordon, Michael D. Ernst, and Dan Grossman. 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.
[+abstract] [+bibtex] [acm | pdf] [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"
}
```
Colin S. Gordon. Formal Semantics for Testing. In Off the Beaten Track Workshop (OBT'12), Philadelphia, PA, USA. January 2012. Position paper.
[+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"
}
```
Colin Gordon, Leo Meyerovich, Joel Weinberger, and Shriram Krishnamurthi. 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.
[+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

Colin S. Gordon, Michael D. Ernst, Dan Grossman. 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.
[+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}},
}
```
Colin Stebbins Gordon. Type-Safe Stack Traversal for Garbage Collector Implementation. Brown University Senior Honors Thesis. May 2008. Undergraduate Thesis.
[+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"
}
```
Meyerovich, L.A., Weinberger, J.H.W., Gordon, C.S., Krishnamurthi, S.: ASM Relational Transducer Security Policies. Technical Report CS-06-12, Computer Science Department, Brown University, Providence, RI, USA. November, 2006.
[+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

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

Unpublished Projects

Sadly not everything can 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 (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 patent applications, one public so far: USPTO Application Record,WO/2008/133977 a.k.a. PCT/US2008/005333 (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