So it turns out I have a lot to say about how my 2012 went. Part 2 to follow!
In January, I began a research
assistant position with my advisor, Ryan, marking the first time in grad school that I've had no major responsibilities other than research (that is, no classes and no teaching). In December, Ryan and I had submitted an NSF grant proposal about lattice-based deterministic parallel computation, so now we began fleshing out the ideas we'd described in the proposal, putting together a semantics for a small language with lattice-based data structures that we called LVars.
Alex and I started training for the 2012 Toronto Marathon, and I opened a
Fitocracy account on January 1 with ambitious plans to log 1,000 miles by year's end.
I spent some time helping organize InWIC, a conference for women in computing in Indiana; the main thing I did was work together with my friends Will and Ian at Studio Cypher to design a cooperative puzzle game for the InWIC attendees to play.
At the end of the month, I went on a delightful road trip to POPL in Philadelphia with a whole pile of folks from IU and CMU. Highlights included playing board games in the hotel lobby and being too scared to say hello to Simon Peyton Jones in the elevator (later I got over it and we had a lovely chat).
In February, Ryan and I continued working on our project. As our LVar-based language began to solidify, I started working on a determinism proof for it, taking the determinism proof for the Featherweight CnC language in this paper as a starting point and frequently soliciting Amr's advice. It had actually been the Featherweight CnC proof that had gotten me started thinking about the relationship between monotonicity and determinism in the first place, so it was interesting to go back to that proof and try to adapt it to our setting.
It began to sink in that I was headed toward doing a Ph.D. with Ryan on deterministic parallelism, which was pretty exciting. Deterministic parallelism was still rather unfamiliar territory for me, but now that I had a big proof to work on, I was in my element. Amr also agreed to join my nascent thesis committee.
As March began, I was getting close -- or so I thought! -- to finishing the proof, and we considered submitting something to ICFP, but with the proof still not done, we decided we'd better wait and shoot for POPL in July instead.
During IU's spring break in mid-March, Alex and I went to Boston for a few days, where I spent some time working with Amal on the still-unfinished multi-language parametricity project I was doing with her. While there, I told Amal about what I was working on with Ryan, and when I showed her one of the properties I'd had to prove to make our determinism proof go through, she pointed out that it looked sort of like a frame rule. At the time, I didn't really understand what that meant, but the idea stuck with me.
While I was in Boston, Amr found a bug in my proof that had to do with the names of memory locations and the circumstances under which they could be renamed. It wasn't a showstopper, but it would continue to plague us, in one guise or another, for several months.
When I got back to Bloomington, after a couple of meetings in which Ryan, Amr, and I all found ourselves evaluating expressions by hand on Amr's whiteboard, we realized that we really needed a runnable model of our language, so I started hacking a Redex model together. I had a lot of fun bringing the paper semantics to life. On March 30th, which was my 30th birthday, I celebrated by giving a whiteboard talk at PL-wonks about what Ryan, Amr, and I had been doing, followed by a Redex demo.
The next day, Alex and I ran the IU Mini Marathon, which doubled as part of my Toronto marathon training.
In April, I had the honor of visiting my undergrad school, Grinnell College, as part of the Alumni Scholars Program. It was a lot of fun: I chatted with my former professors, met some current students, and gave a talk about the work I did in 2011 implementing parts of the (former, prototype-based) Rust object system.
Once back at home, I spent much of the rest of April trying to finish a particularly hairy case of the diamond lemma (the lemma that did the heavy lifting of our determinism proof) that had been thwarting us for the previous two months. I finally got it at the end of the month -- the solution required a tweak to the aforementioned frame-rule-like property that seemed obvious in retrospect -- and the only remaining known problem with the proof was the
location-renaming bug that Amr had pointed out. By now, the proof had
grown to 40 pages long, and we'd started drafting our POPL submission.
In May, the semester ended, and Alex and I headed to Toronto
for the marathon (following a last-minute trip to Chicago to get my passport renewed). Toronto was great! We got to hang out with our friends Ryan and Janice, who live around the corner from Honest Ed's, and I caught up with my old friend Steven from the Act IV days. And I successfully completed my seventh marathon. Given the course's negative change in elevation, it should have been an easy PR, but I missed my PR by five minutes due to a series of unfortunate gastrointestinal events.
After Toronto, Alex and I headed to California (with cats in tow) for our second summers of
working on Google Translate and Rust, respectively. It
was great to return to Mozilla, where I pretty much already knew everyone on the Rust team. Most impressively, all of the summer 2011
Rust interns -- Tim Chevalier, Eric Holk, Paul Stansifer, Michael Sullivan, and me -- were back for summer 2012, either as
returning interns or, in Tim's case, as full-time employees.
For me, returning to Mozilla for a second summer was something of an indulgence. I had reached a point in my Ph.D. when I really should have been concentrating on research, rather than going off and doing yet another internship, and I suspect that some of the other interns were in a similar position. But the opportunity to work on a project as cool as Rust, with a team as good as the Rust team, was too tempting for any of us to pass up, it seems.
Near the end of May, Ryan
and I got the incredibly exciting news that the grant proposal we'd submitted in December had
been recommended for funding. Being recommended for funding usually means that a grant will be funded, but we kept quiet about it because it wasn't yet a sure thing. So began an extremely squirmy two months of compulsive email-checking and NSF-website-page-reloading.
In June, I managed to keep up my running, aided by the perfect Mountain View weather and the fact that our apartment was right next to the Stevens Creek Trail. For Alex's part, he ran almost every day, sometimes as part of his commute.
At work, I had to spend a fair amount of time re-familiarizing myself with
Rust; the compiler had matured a lot since I'd left the previous August, and the language had sprouted a mysterious new region system, a typeclass system of sorts, and a few other features that were new to me. After some amount of flailing with the type inference engine (which had been overhauled (...again)),
I finally landed integer-literal suffix inference in the compiler in mid-June, in time for the 0.3 release.
Once suffix inference was done, I needed a new project. The team had been mulling over the idea of adding traits to Rust for some time; as far as I know, Patrick was the first to bring up the idea of traits, in his object system proposal from November 2011. After reading a bit and asking some questions, I realized that what everyone had been calling traits were essentially Haskell-style typeclasses with default methods -- in the terminology of the original traits paper, "provided" methods were implementations, while "required" methods corresponded to signatures -- and that Rust's existing
ifaces were just underpowered typeclasses that could be extended to traits (whereas traits and interfaces had been distinct notions in the original proposal). The idea of combining traits and interfaces was well received, and I spent a fair amount of time putting a proposal together, with help from Patrick and Dave, who had already done some thinking about separate compilation and so on. Adding default methods to an interface, it turns out, has surprisingly deep semantic ramifications -- the whole thing's...polarity?...flips, or something. I don't have a good explanation at hand, but something about it made me go "whoa" and sort of stagger back from the whiteboard.
Meanwhile, I was continuing to work on Ryan's and my POPL submission in my off hours. We still had the location-renaming bug in the proof to contend with, but Ryan suggested that I put the proof aside for a while and focus on writing instead, since the POPL deadline was quickly approaching...
Continued in part 2!