SPINning Parallel Systems Software
|Title||SPINning Parallel Systems Software|
|Publication Type||Conference Paper|
|Year of Publication||2001|
|Authors||Matlin, OS, Lusk, EL, McCune, W|
|Conference Name||9th International SPIN Workshop, Lecture Notes in Computer Science, Springer|
|Conference Location||Grenoble, 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.