Kronecker algebra is a matrix calculus which allows the generation of thread interleavings from the source-code of a program. Thread interleavings have been shown effective for proving the absence of deadlocks. Because the number of interleavings grows exponentially in the number of threads, deadlock analysis is still a challenging problem. To make the computation of thread interleavings tractable, we propose a lazy, parallel evaluation method for Kronecker algebra. Our method incorporates the constraints induced by synchronization constructs. To reduce problem size, only interleavings legal under the locking behavior of a program are considered. We leverage the data-parallelism of Kronecker sum- and product-operations for multicores and GPUs. Proposed algebraic transformations further improve performance. For one synthetic and two real-world benchmarks, our GPU implementation is up to 5453 X faster than our multi-threaded version. Lazy evaluation significantly reduces memory consumption compared to both the sequential and the multicore versions of the SPIN model-checker.
|Title of host publication||Euro-Par 2017|
|Subtitle of host publication||Parallel Processing - 23rd International Conference on Parallel and Distributed Computing, Proceedings|
|Editors||Francisco F. Rivera, Tomas F. Pena, Jose C. Cabaleiro|
|Number of pages||15|
|Publication status||Published - 2017|
|Event||23rd International Conference on Parallel and Distributed Computing, Euro-Par 2017 - Santiago de Compostela, Spain|
Duration: 2017 Aug 28 → 2017 Sept 1
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Other||23rd International Conference on Parallel and Distributed Computing, Euro-Par 2017|
|City||Santiago de Compostela|
|Period||17/8/28 → 17/9/1|
Bibliographical noteFunding Information:
Acknowledgments. This research was supported by the Austrian Science Fund (FWF) project I 1035N23, and by the Next-Generation Information Computing Development Program through the National Research Foundation of Korea (NRF), funded by the Ministry of Science, ICT & Future Planning under grant NRF2015M3C4A-7065522.
© 2017, Springer International Publishing AG.
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Computer Science(all)