Michael Weber: Random Bits and Pieces

De Hortus

2007-08-12 :: /events

Irina and I visited De Hortus, a botanical garden in Amsterdam. Pictures abound. Here's a selection:

Lisp Logo (by Conrad Barsky)

Some time ago, Xach mentioned his Elisp snippet which inserts DEFPACKAGE forms into the current buffer.

I finally beefed up my version a little, so that it uses Emacs' buffer filename as default package name. For quick dabbling, visiting a new file and typing RET RET RET is enough. Otherwise, packages to be USEd can be autocompleted from the lists of loaded packages, thanks to SLIME.

Here goes:

(define-skeleton mwe:cl-defpackage-skeleton
  "Inserts a Common Lisp DEFPACKAGE skeleton."
  (skeleton-read "Package: " (if v1
  (if (setq v1 (bobp)) ";;; -*- Mode:Lisp; Syntax:ANSI-Common-Lisp;")
  & (if buffer-file-coding-system
        (concat " Coding:"
                 (coding-system-get buffer-file-coding-system 
  & " -*-"
  & \n
  & \n "(defpackage #:" str
  \n "(:nicknames" ("Nickname: " " #:" str) & ")" | '(kill-whole-line -1)
  \n "(:use #:CL" ((slime-read-package-name "USEd package: ") " #:" str) ")"
  ")" \n
  (if v1 "(in-package #:") & str & ")" & \n &

Works with skeleton mode from GNU Emacs (version 22.0.92). First-time users of autoinsert might want to use the following additional setup:

(eval-after-load 'autoinsert
     (push '(lisp-mode . mwe:cl-defpackage-skeleton) auto-insert-alist)
     (auto-insert-mode +1)))

(require 'autoinsert)

It is also possible to just M-x mwe:cl-defpackage-skeleton. If done somewhere else than at the beginning of a buffer, the comment and IN-PACKAGE form is not generated (useful for a packages.lisp file containing multiple package forms.)

UPDATE 2008-01-08: Old News...

The above skeleton is part of Redshank mode now.

New Paper

A Database Approach to Distributed State Space Generation (accepted for publication to PDMC 2007).


We study distributed state space generation on a cluster of workstations. It is explained why state space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive datatypes. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree-compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors.

This solution is implemented and linked to the μCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g., PROMELA models via the NIPS virtual machine. Our experiments show the trade-offs between keeping the database global, replicated, or local, depending on the available network bandwidth and latency.

The work described here has been in successful production use for some time. Still, during the measurements of the paper, we got a truckload of ideas for improvements. Watch this space...

Fun war story: when measuring, we found that 2% of the zillion queries between the cluster nodes and the database were unproportionally slow: They took a whopping 200 milliseconds round-trip! With some analyzer gear plugged into the switch and the help of our networking guys, we were able to predict when one of the slow messages would appear (confirmed by program instrumentation). In the end we traced it down to a driver problem. Switching to a different brand of network cards made the problem go away.

Your Vote Decides!

2007-05-13 :: /rants
Eurovision Song Contest 2007 (Logo)

Quoting from the article Radical Serbia speaker steps down (source: The Beeb, emphasis mine):

Earlier, opposition MP Nenad Canak said Mr Nikolic's nationalist and anti-European stand no longer had a place - especially as Serbia had just won the Eurovision Song Contest.

Mr Canak said Serbia's neighbours had all awarded his country maximum points in the contest. But Russia, described by Mr Nikolic as Serbia's only friend, had only awarded his country five points.

Clearly, five points are not enough to prove friendship, don't you see?

New Paper

An Embeddable Virtual Machine for State Space Generation (accepted for publication to SPIN 2007).


The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages. Several tools have been built on top of the VM implementation we developed, to evaluate the benefits of the proposed approach.

This is one pixel in a bigger picture.

Page 13/29: « 9 10 11 12 13 14 15 16 17 »