LWN Weekly Edition
Front pageSecurity
Kernel development
Distributions
Development
Linux in the news
Announcements
->One big page
This page
Previous weekFollowing week
Sponsored link
Vyatta –
Linux & Open Source
Alternative to Cisco –
Advanced Routing,
Firewall, VPN, QoS..
Free Download ->
| |||||||||||
DevelopmentUsing Promela and Spin to verify parallel algorithms
Validating Parallel AlgorithmsParallel 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.]
System Applications Clusters and Grids 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."
Database Software PostgreSQL Weekly News The July 29, 2007 edition of the PostgreSQL Weekly News is online with the latest PostgreSQL DBMS articles and resources.
Filesystem Utilities 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."
Libraries 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."
Networking Tools 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.
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."
Printing 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."
Web Site Development Django weekly roundup The July 30, 2007 edition of the Django weekly roundup covers the latest developments on the Django web platform.
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."
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.
Web Services 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."
Miscellaneous 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."
Desktop Applications Accessibility 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."
Audio Applications 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.
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."
Desktop Environments 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."
GNOME Software Announcements The following new GNOME software has been announced this week:
KDE Software Announcements The following new KDE software has been announced this week:
Xorg Software Announcements The following new Xorg software has been announced this week:
Desktop Publishing 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."
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."
Electronics 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."
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.
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.
Financial Applications 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.
Interoperability 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.
Mail Clients 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."
Office Applications 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."
Office Suites OpenOffice.org Newsletter The July, 2007 edition of the OpenOffice.org Newsletter is out with the latest OO.o office suite articles and events.
Digital Photography 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."
Web Browsers 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."
Languages and Tools Caml Caml Weekly News The July 31, 2007 edition of the Caml Weekly News is out with new Caml language articles.
Java 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."
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.
Python The Python 3000 FAQ Guido van Rossum has published the Python 3000 FAQ: "Some questions that people often ask about Python 3000 (and answers)."
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.
Tcl/Tk 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.
XML 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."
Miscellaneous 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.
Page editor: Forrest Cook |
|||||||||||