Uses This

Who are you, and what do you do?

I'm Gerard Holzmann, a software researcher. I'm probably best known for developing the Spin tool for verifying multi-threaded code. Spin is based on logic model checking algorithms, but nicely tries to hide that from the user. We've applied the tool to lots of cool applications, and not just to analyze the flight software of interplanetary spacecraft. We used it, for instance, in the analysis of Toyota's engine control software as part of NASA's investigation of the possible causes for unintended acceleration.

What hardware do you use?

At home I have a 32-core machine with 64 GB of memory, running Ubuntu 12.04 LTS, and a more standard 4-core 3.3 GHz 64-bit Windows 7 PC with a measly 8 GB of memory. I have two levels of backup for my system. The first level has four 1 TB disks for nightly backups. The second layer has two 3 TB backup disks in a different part of the house for some extra protection (they backup the backups: yes, I know).

At JPL I have a 64-core machine (4x16 AMD Opteron running at 2.2GHz) with 128 GB of memory, running Ubuntu 12.04 LTS, for the bigger crunch jobs.

My laptop is a small Toshiba Portege Z930-S9301 Ultrabook running Windows 7. I use this mostly for travel and for giving presentations, but it is wonderful. I do a lot of photography, mostly portraits, and I've accumulated almost as many cameras as laptops and PCs. My first PC was a TRS-80 Model II that I bought in 1981. My largest camera is a traditional Cambo studio camera that can take negatives up to 8x10". The camera I currently use most, though, is a Canon 5D Mark II.

And what software?

I write most of my code in C, using the standard Unix development tools (bash, make, grep, sed, awk, etc.). I for instance wrote some digital darkroom software at Bell Labs in 1983 called pico. For text editing I use Rob Pike's sam screen editor - an old-time favorite of the former Center 1127 gang from Bell Labs. For presentations I admit to using PowerPoint, although I wish that the OpenOffice tools would become good enough to surpass it. And then of course I use Photoshop and Adobe Bridge for photography.

What would be your dream setup?

I'd love to have unlimited access to a Google-sized network of CPUs to run jobs on. It would have to be a couple of thousand always available computers that are as simple to invoke as the cores in my work and home machines. It would be incredibly empowering. We also still do not have very good visualization tools for studying software systems. There is, for instance, no default method for looking at executing code, so that one can hunt for patterns and spot the unpredictable small anomalies in an execution.