Colin Stebbins Gordon

Sc.B. Computer Science, Brown University

 colin@cs.brown.edu

 http://cs.brown.edu/~colin/

 http://ahamsandwich.wordpress.com/

 http://blogs.sun.com/csg/

 Resume

  PGP Key 1 | PGP Key 2

Interests

Music, Bass Guitar, Film, Literature, Programming Languages (especially type systems and other static analyses), Operating Systems, Distributed Computing

Course TA & Head TA Positions

Spring 2005: CS004, Fall 2005: CS017, Spring 2006: CS018, Fall 2006: Head TA CS017, Spring 2007: Head TA CS018
Head TA for CS167/9 (Operating Systems, w/ lab) for Fall 2007.
Head TA for CS190 (CSCI1900) Spring 2008.
Meta-TA Technical for the 2007-2008 school year

Experience

See my resume, linked above to the right. Primarily TA work, research (below) and industrial experience in the Data Retention Group (filesystem-related) at Network Appliance and the Solaris Kernel Group at Sun Microsystems.

Beginning in August 2008, I will be working in the Technical Strategy Incubation group at Microsoft, in Redmond, WA.

Current Projects

Mocha

Mocha (link) is an alternative course indexing system to help students shop for classes. It was originally created by five of my peers, because the system provided by Brown suffers from terrible usability issues. I joined the development and maintenance team last spring, and manage the server hosting the site in addition to continuing development work.

I occasionally also appear in print as a result.

MTA Tech

MTA Tech is a position I hold for the 07-08 school year. I am responsible for all technical aspects of the CS deparment's TA program, in addition to helping out the MTA Admin when needed. My direct responsibilities include scripts used by most classes, and some setuid/setgid programs such as those used for students to hand in their assignments (/usr/local/bin/handin) and those used by Head TAs to change permissions of files they do not own when needed in their course directories (chmod!/chgrp!). And of course, I fill the role of a general technical resource for all of the department's TAs. There are roughly 100 undergraduate and head TAs this fall.

Brown CS190 Head TA

The Head TA for CS190 (now listed as CSCI1900), Software Systems Design. An upper-level software engineering course, where students take a nontrivial software project in a large group from inception through requirements gathering, through design and complete implementation to learn about how to design software for people, rather than for assignments, on a somewhat larger scale.

Honors Thesis (see research)

A Type and Effect System for Limited Linearizability (see research)

Research & Publications

TR: ASM Relational Transducer Security Policies

Work on a controlled composition operator for abstract state machines, motivated by the desire to use ASMs for checking properties on security policies written in a modular way. Brown TR-06-12

Workshop Paper: Composition with Consistent Updates for Abstract State Machines

A paper based on the above technical report, focusing on the composition of smaller ASM programs to create atomic update groups to maintain consistency in ASMs. Presented at ASM '07. Co-authors Leo Meyerovich, Joel Weinberger, and Shriram Krishnamurthi. Paper. Proceedings.

Other Research: Software Transactional Memory

Software Transactional Memory (STM) Research group, using the SXM package for .NET to explore implementation details, and conflict resolution policies for software transactional memory, an alternative to normal locking, which works by adding machinery to a language to detect actual memory conflicts and abort (retry) all but one conflicting thread, rather than adding fine grained locking. Many current implementations far outperform coarse-grained locking, and several approach the performance of fine-grained locking.

A number of people worked on different parts of the system. My work focused on resolving conflicts between threads when both have attempted to work with the same piece of state, and at least one is a write to the shared location. Different policies (called contention managers) perform better or worse under various levels of contention for shared resources. I attempted to implement a contention manager for SXM which switched policies dynamically at runtime, automatically, to use the policy which performed best for that level of contention. Results after some time were inconclusive.

Other Research: Hardware Transactional Memory

Working on implementing a prototype for an alternative hardware TM implementation in a power-accurate simulator, to explore possible power savings from using HTM in embedded devices.

Honors Thesis: Type-safe Garbage Collection

Garbage collectors serve an important role in some programming languages, by abstracting away memory management. For collectors to work effectively, they must change memory without the knowledge of the running program. To do this safely, it must preserve unspoken invariants of the user program. There are basic safety issues such as not replacing pointers with null, or prematurely collecting memory still in use - these are likely to be easy to detect. A more subtle safety property to guarantee when writing a collector is that it must preserve the types of the program it is collecting - it must not replace a pointer to an instance of a Foo with a pointer to an instance of a Bar. This kind of bug in a collector would likely be very difficult to track down. High level languages, such as members of the ML family, offer a great deal of support for reasoning about the correctness of user programs. It would be useful to extend this reasoning capability to garbage collectors by making them explicit functions.

Previous work by others established a basic type-safe approach to collecting the heap, but facilitated this by performing heavyweight transformations on programs in order to get the roots, destroying the normal machine stack, and turning the program into what is essentially a dispatch loop on a structure - a literal implementation of an abstract machine. This hurts performance, as well as making many existing debugging tools, which depend on the stack to help programmers determine what code paths they have followed, useless. Rather than removing the machine stack from consideration, what we would really like is a type-safe way to walk the native machine stack. Other work established such an approach, but it was somewhat impractical. My honors thesis is designing (and implementing) a type-safe approach to walking the stack, and integrating it with prior work on safely collecting the heap, to write a completely type-safe garbage collector. Towards this end, I'm currently hacking up a copy of the MLkit compiler. It's a great compiler for experimentation, as it has extensive support for printing various intermediate forms.

A Type and Effect System for Limited Linearizability

Joint project with Eric McCorkle. Implementation of lock-free data structures is typically a challenging task. Not only must one prove an algorithm is safe, but once a general algorithm is shown to be linearizable (and therefore safe to use), implementation is error-prone. We have a set of constraints which we believe are sufficient (though not necessary) to guarantee linearizability for a function, which are permissive enough to show a number of established linearizable algorithms are in fact linearizable. We are now building a type and effect system to enforce these constraints, which can then be used to verify implementations of those and other simple linearizable data structures.

Reading I Found Particularly Interesting or Useful

I occasionally tag some interesting papers with the papers tag on my blog.

Courses Taken

Spring 2008

CSCI2950-X* (formerly CS296-1*) Topics in Programming Languages and Systems: Optimistic Replication, CS197-17 Independent Study on Hardware Transactional Memory, CS197-20 Independent Study (towards honors thesis) on type-safe garbage collection, MCM0900-O: Code, Software, and Serious Games

Fall 2007

CS149 Intro. to Combinatorial Optimization, CS197-17 Independent Study on Hardware Transactional Memory, CS197-20 Independent Study (towards honors thesis) on provably correct and type-safe garbage collection

Spring 2007

CS190 Software System Design, CS194-17 Independent Study on Software Transactional Memory with Maurice Herlihy, CS157 Algorithms, EN164 Design of Computing Systems, GS006 Group Independent Study Project on Dystopian Literature

Fall 2006

CS051 Models of Computation, CS176 Distributed Computing, CS167 Operating Systems, CS169 Operating Systems Lab

Spring 2006

CS036 Systems Programming, CS166 Computer Security, CS296-1* Specification and Verification of Dynamic Access Control, RU031 Russian Literature in Translation II: Tolstoy to Solzhenhitsyn

Fall 2005

CS031 Computer Architecture, CS173 Programming Languages, MA158 Cryptography, PL003 Knowledge and Skepticism

Spring 2005

CS018 Integrated Intro. to CS (Part II), MA020 Multivariable Calculus (for Physics and Engineering), CS022 Discrete Mathematics, CS034 Intro. to Systems Programming, PH008 Intro. To Relativity and Quantum Mechanics

Fall 2004

CS017 Integrated Intro. to CS (Part I), MA019 Advanced Calculus, IT101 Dante in English Translation, PH007 Analytical Mechanics

* Graduate Level

This site is constantly (albeit slowly) under construction.

About Me

I'm me. I am a computer science concentrator at Brown University, in Providence, RI. My interests lie primarily in the areas of operating systems-related topics, programming languages, and parallel and distributed algorithms, though I am certainly interested in other subareas of the field as well. I'm currently involved with the Brown PLT research group, and in August will begin working in the Technical Strategy Incubation team at Microsoft, exploring new directions in the systems arena.

I'm interested in improving the construction software to make the process easier and the results more robust. Specifically, they should be more natural to specify, and the programming languages and tools used should detect as many errors as possible before a potentially erroneous system is deployed. To this end I'm interested in new abstractions for managing difficult portions of software engineering (e.g. transactional memory), rich type systems to guarantee correctness of system behavior, as well as model checking to verify other correct behavior of systems.

Courses every CS concentrator at Brown should absolutely take:

  • CS167/9
  • CS173
And if you have time:
  • CS176
  • EN164

Get OpenSolaris