The Backslash Incident

I guess it’s never a good time to find out your code has bugs. But there are exceptionally bad times to do so. A middle of a live demo is one such example. Immediately after said demo, when you’ve invited the attendees to take your code for a spin, is not too good either.

Case in point: I had the honor of presenting BPjs at a seminar at Harvard School of Engineering and Applied Sciences (SEAS). BPjs is a tool suite for running and verifying programs written in JavaScript, using the Behavioral Programming programming paradigm. In short (very very very short): It’s a paradigm that focuses on how the system should behave, rather than on how its implemented (e.g. objects, functions, or procedures). Because behavioral programs (“b-programs” for short) can be verified against a set of formal specification, BPjs allows writing verified systems in JavaScript. Which is, admittedly, weird. But in a good way.

As part of the above mentioned demo, I’ve created VisualRunningExamples, an application that allows playing with a behavioral program for a maze walker. Users can load and modify the walker’s behavioral model and formal specification, and then run or verify it, using a friendly GUI. It also serves as an example of how to build a program around a BPjs model.

VisualRunningExamples – Maze solution obtained by formal verification of the maze and walker model.

One fun part of VisualRunningExample’s UI is the selection of the maze the walker would roam in. My favorite maze has a cow (created using cowsay, of course). During the presentation I let the walker walk around the cow a bit, and I thought I saw it demonstrating a bad behavior – it seemed like it was going through a wall. I’m not an expert in maze walking, but I assume maze walkers should not do that.

Immediately after the presentation, I looked into this in more depth. It seemed like the walker was moving diagonally. Which it should never do, since no part of the program requests such a move. It ostensibly went from point X to point Y:

_______
<BP(moo) >     @@@@@@@@@   t
-------
        \Y  ^__^    @@@@@@@@
@ @@@@@ X\  (oo)_______
s           (__)~~~~~~~)\/\
@ @@@@@        ||----w~|
               ||     ||

Was this really happening? Using VisualRunningExamples, I’ve added the following b-threads, and verified the program against it. The idea behind this code is that whenever the maze walker gets into a cell, a set of b-threads that look for diagonal entries is spawned. These b-threads blow the program up if they detect a diagonal mode. Pretty neat pattern, I think (reminiscent of LSC’s symbolic charts used to forbid events):

bp.registerBThread("no-diagonal", function(){
    while (true) {
      var crd=getCoords(bp.sync({waitFor:anyEntrance}).name);
    	noEntryNextMove(crd.col-1, crd.row-1);
    	noEntryNextMove(crd.col-1, crd.row+1);
    	noEntryNextMove(crd.col+1, crd.row-1);
    	noEntryNextMove(crd.col+1, crd.row-+1);
    }
});
 
function noEntryNextMove(col, row){
    bp.registerBThread("nenv(" + col + "," + row + ")", function(){
        var evt = bp.sync({waitFor:anyEntrance});
        var newCoords = getCoords(evt.name);
        bp.ASSERT( newCoords.col !== col || newCoords.row !== row, "Diagonal Movement detected");
    });
}

Verification did not find anything wrong, yet that parallel movement is happening, live, in front of my eyes. So, verification is broken too. Highly embarrassing, given that I just presented the tools at Harvard SEAS’ SPYS group. Time to do some runtime verification.

Runtime verification really boils down to adding these b-threads to the b-program (“model”), and running it. Easily done, and we know the runtime works. So, yay, next time mr. maze walker wants to do a diagonal jump, one of these b-threads will catch it red-handed. With an evil grin, I click the Run button.

Nothing. The walker does diagonal jumps like a boss. But only between points X and Y. Luckily, VisualRunningExamples’s UI is fun to play with, so I change the \ to *.

No more parallel jumps, which never really happened. Good news: BPjs’ verification works. As does its runtime.

What Went Wrong

What really happened was that when creating the source Javascript b-program, the Java layer was copying the maze into an array of strings, verbatim. This meant that \ was really an escaped space, which translates to a single space in JavaScript:

jjs$ var s = "\ "
jjs$ "|" + s + "|"
| |
jjs$

The Java UI, on the other hand, displayed the backslash in the maze monitor table. In short: the JavaScript b-program saw a space there, whereas Java saw a backslash. The ostensible diagonal jumps were just the maze walker going from X to Y through an empty cell, that was marked by the Java layer as a \ cell.

Lessons Learned

• Need to be careful when constructing code from user input (OK, that’s not a very new lesson, more of a reminder really. But still).
• If you have a suspicion something is wrong in a b-program, BPjs makes it easy to verify.
• Tooling and UI that make the b-program easy to play with are very important. All in all, I went from having a suspicion to verifying the code in about an hour of casual coding on the couches at an empty student center somewhere in the Harvard campus.
• Since BPjs uses the same structures for verification and for modeling/execution (namely, b-threads written in JavaScript), it is trivial to share code between the b-program and its formal specification. That’s important, e.g., when one wants to extract data from strings.

My experience with this whole BPjs as a verification platform, is that it enables “casual verification” – it is very easy to create and run verification code, all the tools are there already, and you’re probably in the mindset as well. Compared to re-creating the system by modeling it in, say, PROMELA, it’s much more casual. Not to mention translation errors between model and actual software.

VisualRunningExamples now has a shiny new cow that does not contain any backslashes. I kept the old cow too, but it’s now called “cow (bad)”. Escaping the maze text properly is followed by issue #1.