Research Nomads

LFX Videos now available

2010-06-15T20:50:00.001-07:00

Videos from the recent LFX workshop are available here:
http://www.vimeo.com/groups/lfx

Slides are also available online on the workshop's homepage:
http://research.ihost.com/lfx2010/

Phalanx is to appear in ISMM 2010!

2010-03-20T18:00:00.000-07:00

Our paper on Phalanx — a practical framework for dynamically checking expressive heap properties — was accepted to ISSM 2010. Phalanx uses novel parallel algorithms to efficiently check a wide range of heap properties including ownership, sharing and reachability.

Abstraction-Guided Synthesis to appear in POPL'10

2009-09-27T06:37:00.000-07:00

Our paper titled "Abstraction-Guided Synthesis" will appear in POPL'10. The paper presents an approach for synthesizing synchronization in concurrent programs using abstract interpretation. Below is a word-cloud summary. The paper itself will be available online sometime early November.

Bell Labs

2009-09-16T08:53:00.000-07:00

"Pierce created a rare environment in any industry or research lab, one in which the scientists felt empowered to do their best and in which creativity was highly valued. At the time, the Bell Telephone Company/AT&T had a complete monopoly on telephone service in the U.S. and a large cash reserve. Their laboratory was something of a playground for the very best and brightest inventors, engineers and scientists in America. In the Bell Labs 'sandbox', Pierce allowed his people to be creative without worrying about the bottom line or the applicability of their ideas to commerce. Pierce understood that the only way true innovation can occur is when people don't have to censor themselves and can let their ideas run free. Although only a small proportion of those ideas may be practical, and a smaller proportion still would become products, those that did would be innovative, unique, and potentially very profitable. Out of this environment came a number of innovations including lasers, digital computers, and the Unix operating system".

(from the book This is your brain on music / Daniel J. Levitin)

PSY 2009 videos now available online

2009-08-18T17:25:00.000-07:00

On June, we held the 1st International Workshop on Practical Synthesis for Concurrent Systems (PSY 2009). In this workshop, we experimented with recording all the talks with a Vado HD (recommended by our gadget-guru Noam Rinetzky). The results are definitely far from a professional-level recording, but the cost of the entire setup was only a few hundred bucks.

The resulting videos are available here.

I think that the main lesson from these videos is to get a better tripod, preferably one with a bubble level.

The exact setup used for producing these videos:

Creative Vado HD 720p Camcorder with 8 GB and 2x Digital Zoom
Creative Labs Battery Charger for Vado and Vado HD Camcorders
Creative Labs Rechargeable Lithium Ion Battery for Vado HD Camcorder
Digipower TP-S010 flexible and sturdy ultra compact Mini Tripod
Handbrake video transcoder (thanks to Yoad for the reference)
Quicktime Pro for editing the videos (yes, you will have to edit the videos)
Vimeo Plus for hosting the videos

Total cost: ~$300 including 1yr of plus membership on Vimeo

QVM Word Clouds

2009-04-20T06:02:00.000-07:00

Here's some more word cloud joy, now for the QVM OOPLSA'08 paper.

and for the QVM Chameleon PLDI'09 paper

Algorithms for Concurrent Data Structures

2009-04-20T05:53:00.000-07:00

Word clouds seem to be all the rage lately. Playing with some clouds for a recent talk, I found them to actually provide an interesting summary of research papers. For example, here's a word cloud for our PLDI'08 paper on derivation of highly-concurrent linearizable data structure algorithms.

Apart from the emphasis of terms like "true", this is a pretty decent summary of what's going on in the paper --- concurrent algorithms, linearizability, and a lot of dance around atomic blocks, restarts, and the pointers curr and pred.

Irad Yavneh: Megilat Hamuamad 2005

2008-12-20T08:37:00.001-08:00

A recent visit to Israel exposed me to this brilliant piece (in Hebrew). There are a few subsequent performances by Irad that are equally good. You can find them all at http://www.youtube.com/user/shaulm

SAFE Tech Fair Posters

2008-08-21T19:29:00.001-07:00

QVM Tech Fair Poster

2008-08-21T08:04:00.001-07:00

(click to see full size image)

Vista Pains

2008-08-19T14:52:00.000-07:00

I really wanted to like Vista. When I got my Thinkpad X61 Tablet, it came with Vista installed by default. Ignoring the negative Vista press and applying wild optimism, I was sure that this is the beginning of a wonderful friendship. Unfortunately, this was not meant to be. Not only that Vista crashes left and right, it is always somebody else's fault: "Problem is caused by Intel Graphics Driver", "Problem is caused by Cygwin", and my all time favorite "This problem is being researched".

The utility may be called "Solve problems on your computer", but in the several months I had Vista, it did not help me find a solution to a single problem. All it really does is allocate blame, elsewhere.

To see how bad things are, here's a report from the performance and reliability monitor.

As you can see by the red markers, almost no day goes by without some sort of a failure. In some days, there are multiple failures. I already started booting to my Ubuntu on most days, but even for my sparse use of windows, I will probably roll back to XP soon.

Carl Sagan on the Importance of Scientific Research, May '93

2008-06-27T17:42:00.001-07:00

Mark Wegman gave an interesting talk on the upcoming grand challenges in CS. In his talk, he used a snippet from this Carl Sagan clip. I thought that the message in this clip is worth echoing by posting it here.

The Right Stuff

2008-05-11T18:39:00.000-07:00

On a Saturday afternoon, Greta, Martin and me enjoyed this ale (mostly its name, actually). The meat that accompanied it was cooked in a range from running-rare to nuclear-well-done... the chef was mostly hitting the end points of this range.

Workshop on the Verification of Concurrent Algorithms

2008-05-06T17:30:00.000-07:00

Four of the nomads attended the Cambridge workshop on the verification of concurrent algorithms. I gave an overview talk on Shape Analysis for concurrent programs (slides). Martin gave a short talk about our work on synthesis of concurrent set algorithms (slides).

On the last day, we had a few hours before our flight, so we went punting. Below are a couple of pictures taken by Noam (you can see Noam's reflection in my sunglasses).

Now this is quality paper reviewing

2008-04-30T07:47:00.001-07:00

Without a doubt, the most helpful and well thought out paper review I have ever received. This is the review in its entirety, except for the two-sentence summary of the paper which is excluded.

"The proposed technique appears to be novel. The authors have implemented the technique and evaluated on several significant software systems. The results are very promising."

QVM Talk

2008-04-14T12:31:00.000-07:00

Just gave a QVM talk in Dagstuhl seminar on Scalable Program Analysis.
The slides are available here: http://kathrin.dagstuhl.de/08161/Materials2/

QVM: From 16.5K to 10K in 1 hour

2008-04-01T20:41:00.001-07:00

This is a story that should serve as a warning to all people submitting to conferences. The tragic part is mostly the fact that we have learned that lesson
so many times, and still manage to ignore it... here goes...

When we wrote our QVM submission for OOPSLA, we assumed that the rules of the game are: ACM SIGPLAN template, 20 page limit. These are pretty reasonable rules. To be honest, we were quite pleased with our ability to describe things nicely and in sufficient detail using this format.

A few hours before the deadline (no more than 2), we decided to verify that our
nice submission indeed conforms to the OOPSLA submission directions. Much to our surprise, a strict 10,000 words limit accompanied the 20 page limit. A quick word-count of our submission yielded the fantastic number of 16,500 words... a mere 65% over the limit.

What followed can be only described as a major slash-and-burn frenzy in which whole sections of the paper went out. After a lot of work we reached the more reasonable limit of 12,000 words. Needless to say, the aforementioned "nice and in detail" was no longer a valid description of the paper. However, we believe that we maintained some of the essence of the paper in a reasonable form. (A final word count, without tables and figures, produced a number that was sufficiently close to 10,000 words.)

Some of the things that were described in the slashed 4000 words are:
- formal descriptions of certain components, notably the typestate histories
- some implementation details of typestate history and debug information
- implementation details of parallel checking of heap assertions
- additional experimental evaluation of the heap assertions
- also lost were various discussions of future extensions and optimizations
- references to our online supplement material (see below).

Here are some of the experiment logs recording (some of) our experience with QVM over various benchmarks:

Azureus (here are some bug reports bug1,bug2,bug3,bug4,bug5)
EclipseTrader
GOIM
Feed'NRead

coming soon

2008-04-01T07:42:00.000-07:00