XSpeed: Accelerating reachability analysis on multi-core processors

Rajarshi Ray*, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

41 Citations (Scopus)

Abstract

We present XSpeed a parallel state-space exploration algorithm for continuous systems with linear dynamics and nondeterministic inputs. The motivation of having parallel algorithms is to exploit the computational power of multi-core processors to speed-up performance. The parallelization is achieved on two fronts. First, we propose a parallel implementation of the support function algorithm by sampling functions in parallel. Second, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input. A GP-GPU implementation is also presented following a lazy evaluation strategy on support functions. The parallel algorithms are implemented in the tool XSpeed. We evaluated the performance on two benchmarks including an 28 dimension Helicopter model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experiments illustrate that our parallel algorithm with time slicing not only speeds-up performance but also improves precision.

Original languageEnglish
Title of host publicationHardware and Software
Subtitle of host publicationVerification and Testing - 11th International Haifa Verification Conference, HVC 2015, Proceedings
EditorsNir Piterman
PublisherSpringer Verlag
Pages3-18
Number of pages16
ISBN (Print)9783319262864
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event11th International Haifa Verification Conference, HVC 2015 - Haifa, Israel
Duration: 17 Nov 201519 Nov 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9434
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Haifa Verification Conference, HVC 2015
Country/TerritoryIsrael
CityHaifa
Period17/11/1519/11/15

Fingerprint

Dive into the research topics of 'XSpeed: Accelerating reachability analysis on multi-core processors'. Together they form a unique fingerprint.

Cite this