eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-10-30
8332
1
10
10.4230/DagSemProc.08332.1
article
08332 Abstracts Collection – Distributed Verification and Grid Computing
Bal, Henri E.
Brim, Lubos
Leucker, Martin
From 08/10/2008 to 08/14/2008 the Dagstuhl Seminar 08332 ``Distributed Verification and Grid Computing'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
Links to extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08332/DagSemProc.08332.1/DagSemProc.08332.1.pdf
Parallel Model Checking
Grid Computing
Verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-10-30
8332
1
2
10.4230/DagSemProc.08332.2
article
08332 Executive Summary – Distributed Verification and Grid Computing
Bal, Henri E.
Brim, Lubos
Leucker, Martin
The Dagstuhl Seminar on Distributed Verification and Grid
Computing took place from 10.08.2008 to 14.08.2008 and brought
together two groups of researchers to discuss their recent work and
recent trends related to parallel verification of large scale computer
systems on large scale grids. In total, 29 experts from 12 countries
attended the seminar.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08332/DagSemProc.08332.2/DagSemProc.08332.2.pdf
Grid computing
verification
parallel computing
model checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-10-30
8332
1
2
10.4230/DagSemProc.08332.3
article
A Typical Verification Challenge for the GRID
van de Pol, Jaco
A typical verification challenge for the GRID community is
presented. The concrete challenge is to implement a simple recursive
algorithm for finding the strongly connected components in a
graph. The graph is typically stored in the collective memory of a
number of computers, so a distributed algorithm is necessary.
The implementation should be efficient and scalable, and separate
synchronization and implementation details from the purely algorithmic
aspects. In the end, a framework is envisaged for distributed
algorithms on very large graphs. This would be useful to explore
various alternative algorithmic choices.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08332/DagSemProc.08332.3/DagSemProc.08332.3.pdf
Strongly connected components
distributed algorithms
breadth first search
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-10-30
8332
1
15
10.4230/DagSemProc.08332.4
article
Efficient Large-Scale Model Checking
Verstoep, Kees
Bal, Henri E.
Barnat, Jiri
Brim, Lubos
Model checking is a popular technique to systematically and automatically verify system properties.
Unfortunately, the well-known state explosion problem often limits the extent to which it can
be applied to realistic specifications, due to the huge resulting memory requirements. Distributed memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with
mixed results. We examine one well-known distributed model checker in detail, and show how
a number of additional optimizations in its runtime system enable it to efficiently check very demanding
problem instances on a large-scale, multi-core compute cluster. We analyze the impact of
the distributed algorithms employed, the problem instance characteristics and network overhead.
Finally, we show that the model checker can even obtain good performance in a high-bandwidth
computational grid environment.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08332/DagSemProc.08332.4/DagSemProc.08332.4.pdf
Distributed model checking
Grid-based model checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-10-30
8332
1
3
10.4230/DagSemProc.08332.5
article
Verification of MPI-based Computations
Siegel, Stephen F.
The Message Passing Interface is a widely-used parallel programming model and is the effective standard for high-performance scientific computing. It has also been used in parallel model checkers, such as DiVinE. In this talk we discuss the verification problem for MPI-based programs. The MPI is quite large and the semantics complex. Nevertheless, by restricting to a certain subset of MPI, the verification problem becomes tractable. Certain constructs outside of this subset (such as wildcard receives) can lead to a rapid blowup in the number of states, but MPI-specific reduction techniques have led to progress in combating this state explosion. Specifying correctness is another challenge. One approach is to use a trusted sequential version of the program as the specification, and use model checking and symbolic execution techniques to establish the functional equivalence of the sequential and parallel versions. This approach is supported in extsc{Mpi-Spin}, an extension to the model checker extsc{Spin} for verifying MPI-based programs.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08332/DagSemProc.08332.5/DagSemProc.08332.5.pdf
MPI
Spin
model checking
MPI-Spin
symbolic execution