Development

Using Promela and Spin to verify parallel algorithms

August 1, 2007
This article was contributed by Paul McKenney

Validating Parallel Algorithms

Parallel algorithms can be hard to write, and even harder to debug. Testing, though essential, is insufficient, as fatal race conditions can have extremely low probabilities of occurrence. Proofs of correctness can be valuable, but in the end are just as prone to human error as is the original algorithm.

It would be very helpful to have a tool that could somehow locate all race conditions. Such a tool in fact exists in the form of the language Promela and its compiler Spin.

What are Promela and Spin?

Promela is a language designed to help verify protocols, but which can also be used to verify small parallel algorithms. You recode your algorithm and correctness constraints in the C-like language Promela, and then use Spin to translate it into a C program that you can compile and run. The resulting program conducts a full state-space search of your algorithm, either verifying or finding counter-examples for assertions that you can include in your Promela program.

This full-state search can be extremely powerful, but can also be a two-edged sword. If your algorithm is too complex or your Promela implementation is careless, there might be more states than fit in memory. Furthermore, even given sufficient memory, the state-space search might well run for longer than the expected lifetime of the universe. Therefore, use this tool for compact but complex parallel algorithms. Attempts to naively apply it to even moderate-scale algorithms (let alone the full Linux kernel) will end badly.

Promela and Spin may be downloaded from here.

The above site also gives links to Gerard Holzmann's excellent book on Promela and Spin, as well as online references starting here.

The remainder of this article describes how to use Promela to debug parallel algorithms, starting with simple examples and progressing to more complex uses.

[Editor's note: the remainder of this article is long. Interested readers are encouraged to read the full article on its own page.]

Comments (6 posted)

Release 2.1.2 of Linux-HA is now available

Version 2.1.2 of Linux-HA, a cluster control system, is out. "This release has been extensively tested and is considered stable. At this time, there are no known regressions fro previous stable releases, or the Novell SLES10 SP1 release. It fixes the annoying installation problems that were observed in 2.1.1, and also fixes a small number of other bugs as well."

Full Story (comments: none)

PostgreSQL Weekly News

The July 29, 2007 edition of the PostgreSQL Weekly News is online with the latest PostgreSQL DBMS articles and resources.

Full Story (comments: none)

Grsync 0.6 released

Stable version 0.6 of Grsync has been announced. "Grsync is a GUI for rsync, the command line directory synchronization tool. While it can work with remote hosts, its focus is to synchronize local directories."

Comments (none posted)

libnfnetlink 0.0.30 released

Version 0.0.30 of libnfnetlink is out with new capabilities and bug fixes. "libnfnetlink is the low-level library for netfilter related kernel/userspace communication. It provides a generic messaging infrastructure for in-kernel netfilter subsystems (such as nfnetlink_log, nfnetlink_queue, nfnetlink_conntrack) and their respective users and/or management tools in userspace."

Full Story (comments: none)

conntrack-tools 0.9.5 released

Version 0.9.5 of conntrack-tools, a netfilter firewall configuration utility, is out with new features, some code rework and bug fixes.

Full Story (comments: none)

libnetfilter_conntrack 0.0.81 released

Version 0.0.81 of libnetfilter_conntrack has been released. "libnetfilter_conntrack is a userspace library providing a programming interface (API) to the in-kernel connection tracking state table. This release includes minor changes and bugfixes."

Full Story (comments: none)

CUPS 1.3rc2 has been released

Version 1.3rc2 of CUPS, the Common Unix Printing System, has been announced. "This is an updated release candidate that fixes a scheduler crash and two other non-critical bugs."

Comments (none posted)

Django weekly roundup

The July 30, 2007 edition of the Django weekly roundup covers the latest developments on the Django web platform.

Comments (none posted)

lighttpd 1.4.16 released

Version 1.4.16 of lighttpd, a light weight web server, is out. "We all could use some refreshment in this hot summer. So how about a fresh and shiny new lighttpd release? Sadly the main reasons are again a few security fixes. (Bad developers, bad!) But we broke it, we fix it. On the other hand we squeezed in a new cool feature aswell. The E-Tag generation is now configurable. So if your files are on a NFS cluster you can now e.g. disable the inode number usage for the E-Tag."

Comments (none posted)

mnoGoSearch 3.3.4 released

Version 3.3.4 of mnoGoSearch, a web site search engine, is out with better support for huge documents and other new features. See the change log for more information.

Comments (none posted)

Developing Web Services Using PHP (O'ReillyNet)

Deepak Vohra uses PHP to write web services in an O'Reilly article. "As Software as a Service becomes more of a trend in the industry, Web Services are gaining in importance. When most people think of Web Services, they think of Java or .NET, but as Deepak Vohra shows in this article, it's simple enough to implement them in PHP."

Comments (none posted)

lshw B.02.11 released

Stable version B.02.11 of Hardware Lister (lshw) has been announced. "lshw can report exact memory configuration, firmware version, mainboard configuration, CPU version and speed, cache configuration, bus speed, etc. on DMI-capable x86 or EFI (IA-64) systems and on some PowerPC machines (PowerMac G4 is known to work). Information can be output in plain text, XML or HTML."

Comments (none posted)

MouseClick 0.8.1 released

Stable version 0.8.1 of MouseClick has been announced. "MouseClick is an ergonomic software intended to help those suffering some form of RSI (Repetitive Strain Injury) or other computer related illnesses and cannot click the mouse or other pointing devices. Whenever the mouse pauses briefly, MouseClick sends a click, the amount of time it waits before it clicks is adjustable. In drag mode, it clicks down and then pauses before it clicks up; if you move the mouse while it is down, MouseClick will wait until you are done before clicking up."

Comments (none posted)

Ardour 2.0.4 released

Version 2.0.4 of Ardour, a multi-track audio editor, is out. "Squeaking just before of the end of July, the Ardour project brings you release 2.0.4 ( tarball, DMG to follow), another mix of important bug fixes with some great new features." See the release notes for more information.

Comments (none posted)

FLAC 1.2.0 released

Version 1.2.0 of FLAC, the Free Lossless Audio Codec, is out. "New in this release are small speed improvements, and some new options and bug fixes. Also the decoder has been updated to pave the way for some format improvements, so if your software supports FLAC be sure to check it out."

Comments (none posted)

Frugal Windowing Environment 0.1.5 released

Stable version 0.1.5 of the Frugal Windowing Environment has been announced. "Frugal Windowing Environment is a user-space client-server windowing environment that uses the framebuffer. It is the next logical development of FBUI."

Comments (none posted)

GNOME Software Announcements

The following new GNOME software has been announced this week:

• Accerciser 0.1.6 (bug fixes and translation work)
• atk 1.19.6 (bug fix)
• Empathy 0.10 (new features and bug fixes)
• Evince 0.9.3 (new features, bug fixes and translation work)
• gail 1.19.6 (bug fixes)
• Gazpacho 0.7.2 (bug fixes and other improvements)
• gcalctool 5.19.6 (bug fixes and translation work)
• Glade 3.3.3 (new features, bug fixes and translation work)
• gnome-applets 2.19.0 (new features, bug fixes and translation work)
• gnome-control-center 2.19.6 (new features, bug fixes and translation work)
• gnome-games 2.19.6 (bug fixes)
• gnome-keyring 2.19.6 (new features and translation work)
• GNOME Power Manager 2.19.6 (bug fixes and translation work)
• gnome-speech 0.4.16 (bug fix)
• gnome-system-tools 2.19.1 (new features and translation work)
• Gnumeric 1.7.11 (new features and bug fixes)
• Gtk2Hs 0.9.12 (new features and bug fixes)
• Gtk2-Perl 2.19.6 (new API and bug fixes)
• GtkImageView 1.3.0 (unspecified)
• gtkmm 2.11.6 and glibmm 2.13.9 (new features)
• libgee 0.1.0 (initial release)
• Orca 2.19.6 (new features, bug fixes and translation work)
• Rarian 0.5.2 (new features, bug fixes and documentation work)
• Rarian 0.5.4 (new features and bug fixes)
• Sawfish 1.3.1 (new features and documentation work)
• Tomboy 0.7.3 (new features)
• Vala 0.1.2 (new features and bug fixes)
• Yelp 2.19.1 (new features and code cleanup)

You can find more new GNOME software releases at gnomefiles.org.

Comments (none posted)

KDE Software Announcements

The following new KDE software has been announced this week:

• AmarokScreenSaver 0.4.0 (new features and bug fixes)
• Beesoft Tracer 0.04 (new features and documentation work)
• Cue to Iso converter 0.1 (initial release)
• Essential Contact Manager Release 0.2.0 Alpha (new features and bug fixes)
• h264enc 7.8.3 (new features)
• Jukebox3D 0.1.0 (initial release)
• Kaffeine Player 0.8.5 (new features and bug fixes)
• Kirocker Music Display 3.4 (new features and bug fixes)
• KPlayer 0.6.3 (new features, bug fixes and translation work)
• ktikz 0.1 (initial release)
• LyX 1.5.0 / 1.4.5.1 (new features and bug fixes)
• Qwiimote 0.0.2 (bug fixes)
• ReMoot 0.3.1 (unspecified)
• ReMoot 0.3.1.2 (new feature and bug fixes)
• SpeedCrunch 0.8 (new features, bug fixes and translation work)
• Tellico 1.2.13 (new features and bug fixes)
• TorK 0.18-beta (new features and bug fixes)
• Transcogg 1.0 (initial release)

You can find more new KDE software releases at kde-apps.org.

Comments (none posted)

Xorg Software Announcements

The following new Xorg software has been announced this week:

• libXi 1.1.2 (bug fix)
• xf86-input-mouse 1.2.2 (new features and documentation work)
• xorg-server 1.3.99.0 (new features, bug fixes and documentation work)

More information can be found on the X.Org Foundation wiki.

Comments (none posted)

LyX 1.4.5.1 released

Version 1.4.5.1 of the LyX typesetter is available. "This is expected to be the last release in the 1.4.x stable branch. Besides the obligatory bug fixes, its main feature is the ability to read files created by LyX 1.5.0 (this feature requires python 2.3.4 or later). The only change over release 1.4.5 is the addition to the distribution of one file necessary to read and write lyx 1.5 files."

Full Story (comments: none)

LyX 1.5.0 released

Version 1.5.0 of the LyX typesetter has been released. "Since the announcement of release candidate 2, we have fixed bugs and we have updated the documentation. Following the ad hoc tradition of 1.5.0 pre-releases, called respectively Ruby (alpha), Towny (beta) and Quinta ("farm" in Portuguese for the release candidates) this release starts the Vintage selection that is (will be) the 1.5 series."

Full Story (comments: none)

Announcing GNU Radio release 3.0.4

Version 3.0.4 of GNU Radio, a software-defined radio transmitter system, has been announced. "This is a bug fix release, back-porting all applicable bug fixes on the development trunk into the stable release branch."

Full Story (comments: none)

gSpiceUI 0.9.33 released

Version 0.9.33 of gSpiceUI, a GUI frontend to the spice electronic simulation language, is out. See the change log for a list of new features and bug fixes.

Comments (none posted)

Icarus Verilog 0.8.5 released

Version 0.8.5 of Icarus Verilog, an electronic simulation language compiler, is out. See the change log document for more information on this release.

Comments (none posted)

PostBooks accounting package released

The company once known as OpenMFG, now called xTuple, has announced the release of PostBooks, a Qt-based accounting package seemingly aimed at winning over QuickBooks users. It is available under the CPAL license, which just got its "open source" seal of approval from the OSI.

Comments (5 posted)

Wine 0.9.42 is available

Version 0.9.42 of Wine has been announced. Changes include: Support for activation contexts and side-by-side assemblies, Many more gdiplus functions, More messaging support in crypt32.dll, Many HTTP protocol handling fixes and Lots of bug fixes.

Comments (none posted)

Thunderbird to find new home as Mozilla Foundation focuses on Firefox (MozillaZine)

MozillaZine reports that management of the Mozilla Thunderbird mail client will be separated from the Mozilla Firefox browser. "On her weblog, Mozilla Corporation CEO Mitchell Baker has announced that Mozilla Thunderbird is to move to a "new, separate organizational setting" as the Mozilla Foundation continues to focus ever more closely on Mozilla Firefox. While the Mozilla Foundation supports a number of projects, its taxable subsidiary the Mozilla Corporation is responsible for only Firefox and Thunderbird. However, it has become increasingly clear that Firefox is the priority."

Comments (21 posted)

HylaFAX 4.4.0 released

Version 4.4.0 of HylaFAX, a FAX modem control program, has been announced. "The 4.4 branch of HylaFAX has been in development for the past 4 months. This release includes many improvements over the 4.3 branch of HylaFAX and as such, is a recommended upgrade."

Comments (none posted)

OpenOffice.org Newsletter

The July, 2007 edition of the OpenOffice.org Newsletter is out with the latest OO.o office suite articles and events.

Full Story (comments: none)

UFRaw 0.12 released

Version 0.12 of UFRaw, a utility that can read and manipulate raw images from digital cameras, is out. "UFRaw-0.12 was just released with many new features including full color management, cropping, rotating, scrolling, noise reduction, two new interpolations, a cinepaint plug-in, 21 new cameras and more."

Full Story (comments: none)

Firefox 2.0.0.6 released

Firefox 2.0.0.6 is out - this is yet another security update. The worst of the fixed vulnerabilities involves passing unescaped URIs to external programs. "If you are still running Firefox 1.5.0.x, you are highly encouraged to upgrade to the Firefox 2 series as Mozilla ceased supporting Firefox 1.5.0.x in May 2007."

Full Story (comments: none)

Caml Weekly News

The July 31, 2007 edition of the Caml Weekly News is out with new Caml language articles.

Full Story (comments: none)

IcedTea 1.2 Fonts and Graphics release

Version 1.2 of IcedTea has been announced, testers are needed. "The IcedTea project provides a harness to build the source code from OpenJDK using Free Software build tools and provides replacements libraries for the binary plugs with code from the GNU Classpath project."

Full Story (comments: none)

Restlet 1.0.4 released

Version 1.0.4 of Restlet, a Lightweight REST framework for Java, is out with lots of bug fixes and a few new features. See the changes document for details.

Comments (none posted)

The Python 3000 FAQ

Guido van Rossum has published the Python 3000 FAQ: "Some questions that people often ask about Python 3000 (and answers)."

Comments (none posted)

Python-URL! - weekly Python news and links

The July 30, 2007 edition of the Python-URL! is online with a new collection of Python article links.

Full Story (comments: none)

Tcl-URL! - weekly Tcl news and links

The August 1, 2007 edition of the Tcl-URL! is online with new Tcl/Tk articles and resources.

Full Story (comments: none)

XQuery, libferris, and Virtual Filesystems (XML.com)

Ben Martin discusses libferris in an O'Reilly XML.com article. "By bringing together an XQuery engine and a virtual filesystem you can use a familiar query language to access relational databases, Berkeley db4 databases, kernel filesystems, and network files as well as XML. libferris, at its, core is a virtual filesystem allowing many different data sources to be exposed through a filesystem interface. These include the expected things like file://, http://, ftp:// as well as not so expected things like databases, XML files, and even applications like emacs, Evolution, XWindow, and Firefox."

Comments (none posted)

AutoGen version 5.9.2 released

Version 5.9.2 of AutoGen, a tool designed to simplify the creation and maintenance of programs that contain large amounts of repetitious text, has been announced. It adds several new capabilities and some bug fixes.

Comments (none posted)