remylabs

Let’s say you just got a brand spanking new 8-core computer.  Let’s also say you can’t run Mathematica because Wolfram’s registration process sucks so much (seriously, it’s the worst I’ve ever seen, and I always end up calling them on the PHONE to register).  Now you’re thinking what to do with all those cycles that could be crunching numbers and doing some good, but they’re just sitting there re-indexing Spotlight or something.  You think about downloading BOINC, which is a generic grid computing client that a bunch of different projects are using.  The thing is, you’re a bit obsessive about unnecessary cruft on your computer and BOINC wants to create hidden users and stuff:

Starting with version 5.5.4 of the BOINC Manager for the Macintosh, the BOINC installer creates 2 new “hidden” users boinc_master and boinc_project, and two new “hidden” groups, also named boinc_master and boinc_project (unless they were created by a previous installation of BOINC.)

Yuck.  You’re just not that committed to the project, but you do have the cycles to contribute.  Isn’t there some way to more casually participate in projects?  When I leave for lunch or overnight, why can’t I pull up a page that contains a Flash or Java applet that does some crunching, displays the nice graphics, uploads results and doesn’t install stuff on my machine?  Sure, it’s not as efficient as a native binary, and it doesn’t ramp up when my computer’s workload is low or when the screen saver comes on, but it’s much less intrusive.  It’s also more intentional.

UPDATE: There’s Legion, a Silverlight-based grid computing framework, but I’m not finding any projects that use it.

I stumbled across this profoundly cool tool this week. From the Alloy homepage:

Alloy [is] a simple structural modeling language based on first-order logic. The [Alloy Analyzer] can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

Or, put another way, you can use Alloy to model a software system, complete with facts and assertions about the model, and have the Alloy Analyzer check correctness of the model. It can discover exception cases allowed by your model that violate your assertions. Now you can do agile software design without diving into code right away (even the most elegant code obscures your model’s abstractions with implementation details, and makes it harder to revise your design), and you can do real modeling without generating stacks of UML diagrams. The model is expressed in the Alloy language, and diagrams are generated dynamically by the Analyzer. Here’s an example for Daniel Jackson’s book on Alloy. This system models a set of traffic lights at a junction:

module chapter4/lights —– The model from page 127

abstract sig Color {}

one sig Red, Yellow, Green extends Color {}

fun colorSequence: Color -> Color {
    Color < : iden + Red->Green + Green->Yellow + Yellow->Red
}

sig Light {}
sig LightState {color: Light -> one Color}
sig Junction {lights: set Light}

fun redLights [s: LightState]: set Light { s.color.Red }

pred mostlyRed [s: LightState, j: Junction] {
    lone j.lights – redLights[s]
}

pred trans [s, s': LightState, j: Junction] {
    lone x: j.lights | s.color[x] != s’.color[x]
    all x: j.lights |
        let step = s.color[x] -> s’.color[x] {
            step in colorSequence
            step in Red->(Color-Red) => j.lights in redLights[s]
        }
}

assert Safe {
all s, s’: LightState, j: Junction |
    mostlyRed [s, j] and trans [s, s', j] => mostlyRed [s', j]
}

check Safe for 4 but 1 Junction

The last line tells the Alloy Analyzer to run some test cases with 4 lights and 1 junction and check that the junction is safe (satisfies the predicate mostlyRed at all times and for all transitions. It comes back with:

“No counterexample found” means the model makes safe junctions. 27ms means it’s freakin’ fast. The alloy Analyzer is not an exhaustive model checker, but rather uses a SAT solver, which gives Alloy an efficient way to check huge spaces. Checking a few billion cases in the modeling phase is a lot cheaper, and gives much better coverage with less effort, than running a few hundred unit tests when you’re already writing code.

Here is the diagram generated by Alloy for the small model above:

One slightly annoying thing is that the book uses Alloy 3 syntax, which has been slightly changed for Alloy 4, the current version, but the Alloy team has published a thorough list of changes (”how to update the book for Alloy 4″) which lists all changes and the page numbers on which they occur.

Alloy is free and there are binaries available for OS X, Windows and Linux.

Powered by ScribeFire.