Argonne National Laboratory

SPINning Parallel Systems Software

TitleSPINning Parallel Systems Software
Publication TypeConference Paper
Year of Publication2001
AuthorsMatlin, OS, Lusk, EL, McCune, W
Conference Name9th International SPIN Workshop, Lecture Notes in Computer Science, Springer
Date Published11/2001
Conference LocationGrenoble, France, 2002

We describe our experiences in using Spin to verify parts of the Multi-Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of processes connected by Unix network sockets. Its dynamic nature is easily expressible in the Spin/Promela framework but poses performance and scalability challenges. We present here the results of expressing some of the parallel algorithms of MPD and executing verification runs with Spin.