Scalable Energy Games Solvers on GPUs

Modeling the consumption of limited resources, e.g., time or energy, plays a central role in the design of reactive systems such as embedded controllers. To this aim, quantitative objectives are defined on game arenas that can be easily modeled as weighted graphs. Instances of these games, called energy games, can be solved in O(|E ||V |W) where W is the maximum weight. Recent work has demonstrated that sequential implementations hardly solve practical instances. Furthermore, emerging approaches, that have investigated the parallelism of CPUs multi-core and GPU for solving the initial credit problem for energy games, still perform poorly due to the non-trivial characteristics of these graphs. In the present work, we first describe a revised version of the algorithm on a multi-core CPU that obtains a faster convergence time on real-world graphs with up to 30x against serial implementation by showing good scalability overall. Second, we provide a new GPU-based parallel implementation based on warp-level primitives that allow to reduce the time-to-solution on several instances with up to 3.6x of speed-up against traditional parallel vertex-based approaches. We also discuss a methodology to build synthetic energy games to validate the scalability of parallel algorithms on two totally different settings.