MOVES-Seminar, 9. Jan 2008, 11:00, Seminarraum I 7
Dragan Bosnacki
(Technical University Eindhoven, NL)
Multi-core Model Checking
Abstract:
The new generations of multi-core processors bring the challenge
of how to exploit the parallelism they offer for efficient model
checking. In this talk, we describe an algorithm for parallel
model checking on multi-core processors. We show how the algorithm
can be made compatible with partial-order reduction.
The algorithm is based on depth first search with a limited depth.
When it generates a state which is beyond the depth limit, each
CPU (core) hands off a state to another CPU. One of the main
challenges was to find a counterpart in the parallel setting of
the condition that prevents action ignoring, also known as the
cycle proviso. We give an efficient solution to this problem.
The algorithm was implemented on top of the model checker SPIN
and it was tested on several case studies with encouraging results.
(This is joint work with Gerard Holzmann, NASA Jet Prop. Lab.)
The new generations of multi-core processors bring the challenge
of how to exploit the parallelism they offer for efficient model
checking. In this talk, we describe an algorithm for parallel
model checking on multi-core processors. We show how the algorithm
can be made compatible with partial-order reduction.
The algorithm is based on depth first search with a limited depth.
When it generates a state which is beyond the depth limit, each
CPU (core) hands off a state to another CPU. One of the main
challenges was to find a counterpart in the parallel setting of
the condition that prevents action ignoring, also known as the
cycle proviso. We give an efficient solution to this problem.
The algorithm was implemented on top of the model checker SPIN
and it was tested on several case studies with encouraging results.
(This is joint work with Gerard Holzmann, NASA Jet Prop. Lab.)
