BlogFace.org

I guess I never mentioned this because of how hectic things were the last two weeks, but I did participate in the OOPSLA 2009 Student Research Competition. The first day, I presented my poster in an all-conference poster session. Owing to the excellent position of my poster (Yay for alphabetically-early last names!) I talked to a ton of people, thus giving me the necessary confidence for when the actual judges came to talk to me. 

That night, I had a message in my hotel room that I had passed on to the final round, meaning I needed to give a short presentation explaining my work. Of course I didn't have one, so I wrote one there in the conference. The results, were pretty good. I think I gave a good talk. My slides were fine. I definitely could have answered the questions better. 

Nonetheless, I won third place, which amazingly means I will receive a plaque and a small monetary prize. Tudo Dumitraş, another CMU student from a different research group, won first prize. 

Therefore, from this point forward, I shall refer to my thesis work as award-winning research.

Hey folks. I have lately been thinking about moving this blog over to a different service, most likely Blogger. I wanted to see if anyone had any comments or suggestions. I know this will mean a few changes. Among other things, those of you who follow me as a friend on livejournal will no longer get my updates. Blogface.org, which now resolves to this blog would naturally be updated to resolve to my new blog. This could mean a change to those of you who subscribe to my livejournal RSS feed. I have thought about that. In order to future-proof yourself, you could change that subscription to instead point to feed.blogface.org, which as of today will always point to the current RSS feed.

The main reason I am contemplating a switch is flexibility. Livejournal just isn't that flexible. Its methods for creating blog entries can also be somewhat painful. I can't post cool gadgets like a Last.fm most-recently played songs widget. There are only a limited number of templates. I cannot install Google Analytics. Other things. 

So what do you think. Is this a bad idea? Would you be adversely affected?

Success! I finally got SMLNJ and the MLton optimizing compiler to work with Windows. I am very happy about this, as I had been trying for quite a while and ran into various annoying compilation and DLL problems. (Really mlton was the difficult one.) Here's how I did it.:

• Download Sun's VirtualBox VM software.
• Install Ubuntu.
• Use apt-get to install smlnj and mlton.

Seriously. I really think this is the way to do it and I am perfectly happy to launch Linux every time I want to program, it's just so much easier in Linux land. I like cygwin generally, but I have found that if you want to install some software and there's not already a distribution for it, it can make your life miserable. Ubuntu, on the other hand, has like 9 million packages, and even includes obscure stuff like sml. Problem solved!

Now, what about objects? Certainly Java, as an object-oriented language, provides many features for creating an using objects. Many of those those features, unfortunately, seem to obfuscate the essence of objects. In some ways the most important features of objects are that they implement an interface, and that we can treat them as merely their interface. Here is an interface, and means of constructing objects that implement it. Notes to follow.

In Java, Abstract Data Types and Objects are rather intertwined, often to the detriment of programmers. In this post and the next, I'll try to separate the two concepts as best as I understand. Note that most of these ideas, and the Set example specifically, come to me from William Cook's recent essay. The ideas are also well-covered in TAPL, without the Java code.

Here, I will use a subset of Java's features to express an ADT, such as one would have in a language like ML or Ada. It's a (not very efficient) set. Notes follow.

• The class Set is the abstract data type. It has been declared final, which tells the programmer that the representation is fixed and known completely inside of the class.
• The members field is private to hide the representation. 
• The constructor is private so that new Sets must be created through one of the existing introduction means, namely empty().
• All methods are static. No dynamic dispatch is being used here. We do not want to send messages to objects that can handle that message in an arbitrary way, rather we want to perform some operation on a hidden representation by functions inside of the abstraction that are allowed to view the hidden representation.
• Benefits: Functions inside the Set class can operate on sets with complete knowledge of a set's representation. This can occasionally be beneficial, particularly in cases where performance is important. Knowing that all sets are implemented as sorted arrays of ints can sometimes allow me to write better performing methods. (Binary methods in particular, but other methods as well.) For instance, in the union method above which is incomplete, can perform its task using merge sort if that is more efficient. Still, the representation is hidden from the rest of the program, so we can change things internally without affecting code as long as we don't change the public methods.
• Caveats: No one else can define a Set that is compatible with this Set! If a certain method expects an IntSet of the sort we've just defined, then the IntSet can only be created through this class, and not through any other means. The representation for all IntSets is fixed (but hidden).

Yesterday in SSSG (that class I have to take every semester until I graduate) I gave a talk entitled, "Case Studies in Concurrent Object Protocols." It was really an experience report describing the use of my approach on some open source programs. I used my tool Sync-or-Swim to verify some open source programs, and I encountered a couple of neat patterns which I describe. If you're intrested, check out the slides. I'm afraid you need something that can read PPTX, but if you're interested and you can't read that, let me know and I'll put it up in a different format. 

Today I learned something new! At first it was startling, but in hindsight it makes perfect sense: The Simply Typed Lambda Calculus is not Turing complete. Any well-typed program will eventually terminate, and the intuition here is that your program can only have a finite number of arrow types, and evaluation will always reduce the number of arrow-typed things that you have around. The Untyped Lambda Calculus, however, allows programs that never terminiate. I guess the Y-combinator is a pretty good example here. I once learned that the Untyped Lambda Calculus can be embedded inside the Typed Lambda Calculus by having essentially one type, the everything type. So I guess this makes sense, since there are no arrow types that can decrease monotonically...

Now I have more questions: 
Does this mean the untyped lambda calculus is Turing complete?
How does the encoding of the untyped lambda calculus into the lambda calculus work? I mean, don't functions always have to have function type? Or is the everything type some kind of function type?

 I like Scala, and I am excited about it. But for some reason, every time I try to use it I encounter some minor annoying issue that sort of turns me off and prevents me from making more use of it. Not something significant mind you (type system, performance) but rather something simply annoying.

This time: I just read about improvements to the Eclipse IDE which would make it easy to create mixed Java/Scala projects, which would be great for Plural. So I downloaded it, installed it, and what do you know, I can't even create an object without a syntax error! This is definitely a bug, since I created an object using the wizards, but when I do it I get a syntax error, "Syntax Error: Delete these tokens" on my object declaration. This bug has been reported, but not fixed, and makes the plugin entirely unusable for me. Boo!

This is going to be a rather technical post. Sorry, but I couldn't find information about this anywhere online, or at least I was misunderstanding what information was available online. What I am going to try to explain is something that I just figured out. Let's say you are creating an Eclipse plugin, and part of the functionality provided by your plugin is some classes that will be usable by other programmers who are using your plugin. How can you make it so that the update site for your plugin includes the source code for your plugin, so that users can hover over class names, see the Java docs, etc.?

( Click here for the gory, gory details. )

Today I made a screen capture demo of Sync-or-Swim, the static analysis program that I created with Kevin Bierhoff as part of my thesis research. You should definitely watch it now, even if you don't know anything about computers. If you want to actually be able to read the text, you should watch in HD, fullscreen.

Sync-or-Swim Video

The creation of the video was a little annoying. I needed it to be HD so that the text was actually readable. Here's how I did it:

1. Downloaded CamStudio, a great and free screen capture program.
2. Downloaded their lossless video codec.
3. Important: If you watch Vimeo to recognize your video as HD, it cannot have a 4:3 aspect ratio! To fix this I changed my screen resolution to 1280x768. I told Windows not to stretch the screen so that I saw black bars at the top and bottom.
4. Record and upload to Vimeo. Sweet!

Also, if you've been wondering why my rate of posting has dropped a bit, it's probably because I am putting more of the pointless stuff up on Twitter. If you want to follow me, do, but you'll have to request my friendship (nolacoaster). I still can't decide if I should be open or if I want the protection to post #juicytweets.

I just encountered something in Java that I thought was worth mentioning. It's not exactly a gotcha, but it's good to be aware of.

If you have a nested instance class, synchronizing on this in the inner class is not the same as synchronizing on this in the outer class. This may seem obvious, but it is worth noting because the inner class can refer to methods of either the inner or the outer class in a seemingly ambiguous manner (without explicit qualification). Here's an example program, and its output:


If you know how nested instance classes are implemented, this is not at all surprising. A separate class is created that takes as a constructor argument a reference to an instance of the outer class. So there are two separate instances upon which we are synchronizing.

Man, it seems like everyone is defending or proposing these days!

Yesterday I went to Kevin Bierhoff's thesis defense. Since my work is based on his and also he is my friend, I thought it'd be a good idea to check it out. The defense was great. There was a huge turnout. He passed. The talk went well, if a little light on the technical details, but it was great for a general CS audience. Later that night we went to Bites & Brews to celebrate. Congratulations Kevin!

I also went to see Bite of Brecht, a play on campus that focused on the poetry of Bertolt Brecht. Among other things, it included the song Mack the Knife, which he wrote for the Threepenny Opera. I was expecting some avant-garde garbage based on the lukewarm review in the City Paper, but I actually found it to be quite entertaining. The music was good. The acting was good. There were some funny parts. It did seem to drag a bit at the end, but that was my only complaint. Check it out.

After spending a lot of time doing pointless things, I finally got SDL to work with Scala. Actually, there was nothing tricky about the fact that I was using Scala, that was just part of my original goal. You could equally well say I couldn't get SDL to work with Java. It was pretty obvious that I needed to download SDL.dll and the bindings for Java (both a jar file and some more DLLs), but even then things still weren't working. I was getting the dreaded java.land.UnsatisfiedLinkError. 

Turned out I needed to do three things...
- Add -Djava.library.path= as a VM argument, giving it there folders where both the SDL DLLs and the sdljava DLLs were located.
- Add System.loadLibrary("XXX") for each of the required DLLs into the code itself. This is difficult because it's kind of hard to figure out which DLLs are required! I used this tool to figure it out. 
- Lastly, the biggest problem was that I needed a DLL that I didn't have, SDL_image.dll. The tutorial I was using needed it, but I guess it didn't say or I didn't see where I needed to download it separately. You can get it here.

Just wanted to remind you all of your constitutional obligation to submit to SIGBOVIK 2009, CMU's preeminent fake conference in computer science. This year we've got an EasyChair submission site, just like a real conference. I am currently working on a (secret) project that will be the basis of my submission. It's sucking up all my free Spring Break time, but is pretty fun. I'm not actually sure that this will be at all funny, but it certainly will be strange and something that could not otherwise be submitted at a real conference.

On Saturday night I went to a heroes/villians costume party as The Shoveler, from the movie Mystery Men. Not too many people recognized my character. I guess that movie wasn't as popular as I remembered. If you have thefacebook, here's a picture.

Today marks the beginning of Spring Break 2009, which means it's extremely quiet around the halls of Wean, um, Hall. That's okay. I'm in a relatively good mood.

Yesterday I found out that a paper that I co-authored was accepted at ECOOP 2009. It's called "Practical API Protocol Checking with Access Permissions," and it describes a case study in using the protocol checker Plural to find bugs in real programs. Actually this is mostly Kevin's work. He is the primary author, and this paper comes in large part from his thesis which he is diligently working on. But he doesn't have a blog, now does he? So that means I get to bask in the Internet glory. Um, and you can check out the submitted version of the paper here. (Also congrats to Ciera whose paper was also accepted!)

But the acceptance of this paper definitely has consequences for me, since I was planning to resubmit my failed TRANSACT submission to an ECOOP workshop. Now I'll really have to get on that since I might actually be able to go. (It's in Genova, Italy. How very swank.) I've never yet been to ECOOP, which has a slightly more theoretical and I guess European feel to it than, say, OOPSLA where I have been a couple of times.

In other news, I finally saw "Frost / Nixon," or as I like to call it, "Frosted Nixons." Good movie. As you've no doubt already heard, Frank Langella does an amazing job of portraying Nixon. 

Today was the last day of "Introduction to Separation Logic," a mini-course that I am taking from the creator of Separation Logic himself, John C. Reynolds. It was a good course. Even though I found it difficult, I actually got a quite a good deal out of the course because I decided to take it for credit and therefore I actually did the homework. This will come as no surprise to many of you, but if you actually do the assignments in a course that is centered around proofs you get so much more out of it than if you kind of just take the theorems as already having been proved by someone else.

The weird thing about separation logic (for me) is how different it is from other logics that I have learned which were based upon "hypothetical reasoning." Hypothetical reasoning, I am lead to believe, it pretty much the latest, greatest way of presenting a logic. You get this context of assumptions and then you can do your reasoning from there, using facts from your context whenever necessary. 

Proofs in Separation Logic had a much different feel. In it, you have a whole bunch of rules that are implications. There also aren't really introduction and ellimination rules, just more rules. Every single proof that I did was like this:
I want to prove 
P => D

Therefore, I start with the rule
P => P

Then I find things that P implies that are slighly closer to D...
P => P'

and I have to use the rule, "P=>Q and Q => R means P => R" at every step along the way... Not sure if that makes sense, but it was new for me.

If you're interested, and outside of CMU, you can get the lecture notes for the entire course from John's web site. This is a great way to learn separation logic which has recently become kind of a big deal.

I am currently working on a document. It's kind of a manual. Maybe more like a manefesto. But really, it's a collection of the ideas and strategies that I use when writing Java code. As it turns out, many of those ideas and strategies come from my attempts (and the attempts of other's that I have learned) to use Java in a style that is more like functional languages, particularly the ML languages with which I have some experience.

This document is really targetted at people with some Java experience, and some functional experience, but people who would not consider themselves experts. In particular, it's not targetted at academics, or at least not at PL people. But hopefully it may contain some ideas that you find cool.

Part of the reason that I am posting this now rather than after I have completed a first draft is due to my relatively slow progress. I am hoping that if I post what I've got, you guys may give me some feedback and some cooler ideas, and that this enthusiasm will be enough to help me complete this in a reasonable amount of time. That being said, after this post I will not put up any more blog posts until I at least have an entire draft. If you want to wait until then to read, please be my guest.

So without futher ado, the current draft of, "How to Hack Java Like a Functional Programmer" will be posted at the following URL, and will be updated just as often as I work on it until it is complete:
http://www.nelsbeckman.com/java_like_an_fp.pdf

As alluded to in my last post, I am trying to get a simple little GUI program running in Ocmal. Modulo the ever-annoying X11 issues and some problem using records defined in another module, it's going pretty well. I'm going to post the program and source really soon (not that it's terribly interesting), but here's a screenshot to whet your appetite. This interactive program allows you to place points, and then the convex hull of those points will be computed:

 Hey guys. I'm wondering if anyone out there can help me with a Linux/Cygwin/X11 problem.

I am trying to use the Graphics library in Ocaml. I am using a Windows machine, so I've got cygwin running (not the Ocaml for Windows thing). When I try to build a new ocaml top-level with the graphics library included, like so:

ocamlmktop -o mytop graphics.cma

I get the following result:

Well, it was pretty stressful and my talk went a little longer than I would have hoped, but made it to proposal land! 

Today at 9am I proposed my thesis and about two hours later learned that I passed. We had some good times. We laughed. We cried. We told stories. It was very real.

If you'd like to see my proposal document, please check it out here:
http://www.cs.cmu.edu/~nbeckman/research/proposal.pdf

You can also check out my proposal talk. However, I must warn you, it's very large. I created a PDF from my Powerpoint slides, and somehow they got very large:
http://www.cs.cmu.edu/~nbeckman/research/nbeckman_proposal_talk.zip

Awesome dudes.