BlogFace.org

 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.

 Wow, the Code2000 font really has a lot of glyphs. It takes forever just to scroll from top to bottom in the Windows Charmap.

It is one of the few fonts that has circle times, circle plus and multimap which, as the cool kids know, is necessary for writing linear logic predicates. In LaTeX this had been working just fine, although I have no idea what font I was using, but when it came to PowerPoint I had to get a new font to write them...

 I've got two items of good news that I've kind of been sitting on for a bit, mostly because I didn't want to jinx them. But today they both fell into place!

Today I Scheduled My Proposal!
Today I scheduled my thesis proposal. It will be early next semester, January 27th at 9am. It will be at 9am. I am so sorry for the early time, but my external member is in India which is 10:30 hours ahead during the winter. It should be a rad time. Full details are forthcoming, since I don't have a location yet, but other than that, all of my committee members have committed to a time, and I have written my proposal document. Sweet!

Today I Signed a Lease!
I am moving to Bloomfield! My apartment is basically here. I am very excited to be moving to Bloomfield, where I can still get to school via bus or bike, but where I have a little more variety in terms of restaurants and bars. I looked around for a while and didn't find much, but the last apartment I looked at was very nice. It's also very reasonably priced and has parking. Hard to lose. Stay tuned for the obligatory "new apartment" pictures and the housewarming party. I can pretty much move in today, although I'm waiting until I get back from New Orleans.

I've been going back to read up on OO verification, and I found a very well-written paper entitled, Modular Invariants for Layered Object Structures. Peter Muller and Gary Leavens are co-authors, which comes as no surprise.

The thing is, this was a very easy to read paper that covers a lot of things about Ownership and OO Verification that I had sort of picked up along the way, but had never seen described in a comprehensive way. I guess that's partially due to the fact that it's a journal article, although frankly kind of a crazy journal. This paper uses Universe types, an extension of Ownership types, to prove class invariants. It's very similar to the Boogie methodology, or any of the papers on JML and verification, but this one actually takes the time to explain "classical" OO verification, which motivates the use of ownership.

I should have definitely read this a while ago considering this is basically what my own work is based on, but I guess I had been avoiding Ownership types for a while.

If you are at CMU and you want to check it out, our library has electronic access: here.

The Atomic Nugget design pattern is a way of encapsulating some action that a client wants to perform atomically with respect to a provider class. The idea is that the client will write a "first-class function," in the form of an anonymous inner class, and then give that action to the provider, who will then internally acquire and release the necessary synchronization. In order to make this work, we will need an interface for our first-class functions:

I've been telling people about the Atomic Nugget design pattern for a while, but I have not yet described it in detail anywhere. Atomic Nugget is a design pattern of my own creation that allows for better encapsulation with respect to synchronization in Java and similar languages. And yes, I mostly just like it because of the name, but I do happen to think it's legitamately useful. In this post, I'll just briefly talk about why Atomic Nugget is useful. In the next post, I'll give the code.

In Java, there are simple ways to protect the integrity of your objects with respect to multi-threading if you are the class implementer; you can make all of your public methods synchronized. This will ensure that access from multiple threads to an object instance are effectively serialized. (Of course, it's not always as simple as that, but to a first approximation, this strategy works.) However, what if you are implementing a class that depends on other thread-shared classes? For example, the following worker thread references a thread-shared work queue that is internally synchronized. 

class WorkerThread { 
  private Deque workQueue = // ...
  public void run() { while(true) { if( !this.workQueue.isEmpty() ) doWork( this.workQueue.pop() ) }  }
}

Please ignore the fact that this worker class has many problems. I'm trying to keep the examples short. There is one problem I would like you to focus on, however. The problem is the race condition. If another thread removes the last item from the work queue in between the time this thread calls isEmpty, and the time it calls pop, an exception will be thrown on the call to pop. This is a symptom of a more general problem. The designer of the queue has delineated certain critical sections when they wrote the methods of the queue class. However, as a client, I want to enlarge those critical sections, but in order to do so, I need access to the locks or synchronization primitives that are used internally to the queue. How do people solve this problem now?

1. I could try to make this work by synchronizing on workQueue. However, this is very brittle and violates encapsulation. It requires me to look inside the implementation of the work queue, and ensure that the methods I want to call are synchronized on the work queue object itself, and not some other private member object. Also, if the implementation of the work queue ever changes, to use a different synchronization strategy, my code will be broken.
2. The implementer can provide "lock" and "unlock" methods. This requires class implementers to think ahead to imagine how their classes might be used in the future. (My solution will require this too, as you will see.) But it also painfully requires clients to remember to call the unlock method, which in the simple case might not be to much additional work, but in reality requires clients to use a "finally" block, so that exceptions will not cause locks to be held on to indefinitely. And in general, it's just not nice to have to put your synchronization into the hands of your client.

Enter the Atomic Nugget.

Why, oh why does the 'backspace' key go 'back' to the previous page in all browsers? This is a bug, not something helpful. I just lost the entire entry that I was composing. This is worse than the 'insert' key.

Last night we finally submitted the paper that I have been spending all my time on for the past 3 weeks. We submitted to TRANSACT 2009, a workshop on transactional memory. Our paper was on an optimization of STM using the static aliasing annotations that we have been working on in our group.

Honestly, the process was pretty painful. We had to do benchmarks, which is not something I am used to, and we had a couple fall through at the very last moment, because we could not explain why we were seeing the results we were seeing. I now have a lot more repsect for people who work in systems.

Anyway, tonight I am rewarding myself by going to the Girl Talk concert. I've never seen him live, but his last two albums are in super heavy rotation at home and at work. (Seriously, check the stats.) Also, Grand Buffet is opening, and they are sweet.

 In honor of my not posting in two weeks (seriously, I have a paper deadline this Friday!) I would like to alert you to the following LOLs:

Generalized Super Mario Bros. is NP-Complete

This was a presentation from SIGBOVIK 2007, and I thought it was hilarious at the time, but never remembered to post it. (Also it wasn't online.) It's kind of nerdy, but hilarious.