Abstract

Parity games are a type of game in which two players ’play’ on a directed graph. Solving parity games is equivalent to model checking for μ-calculus. Thus, parity game solvers can be used for model checking. This requires a lot of computational power. Many-core CPUs generally have much more computational power than other CPUs. The Playstation 3 contains an advanced, modern many-core CPU, the IBM Cell Broadband Engine Architecture (CBEA). It is a low-cost option to investigate developing efficient algorithms for many-core CPUs. However, developing efficient algorithms for The Cell remains largely uncharted territory. The Small Progress Measures parity games algorithm, developed by Marcin Jurdzin ́ski, is poised for running on the IBM Cell Broadband Architecture, in particular for the Playstation 3. Here we show there are six important aspects regarding optimizing this algorithm for the Playstation 3: graph subdivision, lifting order, cluster issuing order, capturing cycles, the lifting heuristic and preprocessing the graph. Various optimizations are proposed, e.g.: cluster regeneration, altivec instruction set implementation, and the cluster dependency heuristic. Some of these were implemented and bench-marked. The benchmarks indicate the Playstation 3 seems a viable architecture for the Small Progress Measures algorithm.

Additional Resources

1. The paper