Difference between revisions of "Publications/guenezan.19.seminar"
From LRDE
(Created page with "{{CSIReport | authors = Paul Guénézan | title = Distributed State Space Exploration | year = 2019 | number = 1904 | abstract = In the model checking field, the data structur...") |
|||
| Line 4: | Line 4: | ||
| year = 2019 |
| year = 2019 |
||
| number = 1904 |
| number = 1904 |
||
| − | | abstract = In the model checking field, the data structures used to represent a given program can't be stored in memory due to combinatorial explosion. To speed up the exploration of such large data |
+ | | abstract = In the model checking field, the data structures used to represent a given program can't be stored in memory due to combinatorial explosion. To speed up the exploration of such large data structures, we can use parallel or distributed algorithms. In this report, we present an implemention of a distributed state space exploration algorithm proposed by Camille Coti in "One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters". We compare it against a synchronous algorithm and an asynchronous algorithm using threads to communicate with the same machine. We give benchmarks of all these algorithms using the BEEN benchmark. |
| type = techreport |
| type = techreport |
||
| id = guenezan.19.seminar |
| id = guenezan.19.seminar |
||
Latest revision as of 18:22, 9 November 2020
- Authors
- Paul Guénézan
- Type
- techreport
- Year
- 2019
- Number
- 1904
Abstract
In the model checking field, the data structures used to represent a given program can't be stored in memory due to combinatorial explosion. To speed up the exploration of such large data structures, we can use parallel or distributed algorithms. In this report, we present an implemention of a distributed state space exploration algorithm proposed by Camille Coti in "One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters". We compare it against a synchronous algorithm and an asynchronous algorithm using threads to communicate with the same machine. We give benchmarks of all these algorithms using the BEEN benchmark.