Thursday, April 29, 2010

Beginning of the Summer, Travel, etc.

Well folks, it's been and continues to be a very busy period in my life! The semester is ending. I traveled a whole lot this past year. I'm going to India, again! And the summer is beginning. So let me just bring you all up to date.

The short story is, I am going to Bangalore, India, and I am leaving tomorrow. I'm going to work on a project at Microsoft Research, India that's related to my thesis, but also related to work they do there, so it's a good match. Some of you may know that I was there back in 2007, and had an awesome time. Well I am pumped to be going back. I'll be working with the same person, Aditya Nori, and to a lesser extent with Sriram Rajamani, who is on my thesis committee. This is going to be a more concentrated research trip, since I'll only be there for May, and we have a project to start and finish, but I'll still have some time to be a tourist.

When I get back, I have a bunch of research to get to in my final push to be doctored on. I'll be glad to be back in Pittsburgh for an extended time. I love graduate school, and I love all the great travel opportunities it has provided me with, but I also love my friends in Pittsburgh, and it'll be nice to be here for the summer.

If this post seems a little frantic, it's because I am frantically getting ready! Am I packed? Of course not! But I'll figure something out...

Wednesday, April 21, 2010

Nearest Neighbor

Hey. Just learned about a cool data structure for computational geometry called, KD-Trees. Yes, it's sort of embarrassing that I've just now learned about them, but what can I say? I still think they are cool. Anyway, KD-Trees are like binary trees but for points in space. They make it really easy (well, fast) to do things like search for the nearest point in a set to some given point.

SO, I quickly hacked up a nearest neighbor application. It generates a bunch of random points, and then when you click highlights the nearest point in red. Yay.

Click here to download the JAR if you want to run it. It's on of those runnable Jars... remember those? Ah, Java... I tried to make it an Applet, but that process was even more ridiculous.

Tuesday, April 13, 2010

Proof of Soundness for a Typestate Checker with Locks

Right now I am working on (what I hope will be) the last major theoretical effort of my thesis. I need to do another proof. Way back when I wrote this paper for OOPSLA in 2008, I did a proof of soundness for my language, a language that used atomic blocks for mutual exclusion. Right now, I'm doing the same thing but for a language that uses synchronized blocks. In other words, a language that is more Java-like.

Proofs are pretty painful for me, and the last one I did was really complicated, so rather than merely update the old proof to add locks, I am actually rewriting and simplifying (I think?) a whole bunch of stuff.

One of the biggest questions for me is a question that is important whenever you are doing a proof for a language with references; how will I define a well-typed heap? A well-typed heap means a runtime heap that is consistent with the type-checking facts that were known statically. In my system, every thread is an expression, and each one has its own type-checking context. They all much be consistent with the heap. Furthermore, in anticipation of my proof of preservation (where I have to show that after a step, the heap will still be well-typed) I think that my definition of a well-typed heap will have to include the following condition:
At most one thread can know statically the exact state of an object.
In my last proof I had a similar condition, but it was really unweildy to work with. I wonder how I can simplify this desire?

We're Live @ Blogger

Hey folks,

As you may have noticed, my blog is now hosted at This is why a.) you see a fancy new layout and b.) if you normally get here by typing into your browser, it's no longer a silly URL redirect, but rather you actually see in your browser's address bar. Nice. There are a few reasons I switched over to Blogger, but mainly I just wanted to try something new. If you ever have the joy/pain of switching from one blog software to another, I highly recommend you check out the google-blog-converters project. You can run it on there app engine or on your own PC, and it even logs into your blog and grabs all the comments if you want it to.

Couple of things to keep in mind:
  • If you want to follow over RSS, go to
  • While comments were moved from the old blog, I guess you have pretty much lost your ability to edit your comment if you made one.
  • Lists should have three items.

Sunday, April 11, 2010

The Dissatisfactory Doily

The most recent incarnation of SIGBOVIK, the annual celebration of all that is computer science humor, occurred on April 1st. I didn't have much time to recap it earlier, but it went very well. With the exception of being just a tiny bit long, this may have been the best SIGBOVIK ever. If you're interested in a (free) electronic copy of the proceedings or a ($7) paper copy of the proceedings, go back and click those links!

But I mostly wanted to talk about my own paper, The Dissatisfactory Doily. The premise of the paper is this: You own a sports team. You are jealous of the Pittsburgh Steelers and their ability to sell $10 Terrible Towels. You's like to make your own, but you don't have a clever, alliterative name. Well look no further than the Dissatisfactory Doily, a random name generator for Terrible Towel knock-offs. It takes a list of adjectives (synonyms for terrible) and a list of nouns (cloth-related) and spits out your new product name. For a long list of examples, please see the paper, but some of my favorites are, The Wanton Wall-to-Wall Carpeting, The Abominable Afghan, and The Horrendous Hanky.

In further news, this was likely my last year as SIGBOVIK MC. It's been a lot of fun, but my jokes are getting stale. Time to pass the torch!