Jun 10, 2014: Tom van Dijk: Multicore MDDs (developments in MaDriD project)

June 10, 2014Multicore MDDs (developments in MaDriD project)
Room: HalB 2FTom van Dijk

We present recent developments in the MaDriD project. In a paper we are currently submitting, we compare work-stealing using different queues. We will discuss three queues: our own queue (a non-blocking split deque), Wool (the original work-stealer in our project) and a 'private queue' implementation. The results of the benchmarks show that task-based parallelism on multi-core systems (such as our 48-core and our 64-core system) has low overhead and nice scalability, for all three implementations.

We will also show how task-based parallelism is applied to the "ListDD" datastructure in LTSmin and how it is applied to LTSmin itself. We present some preliminary results on symbolic reachability of models in the BEEM database using parallelized LDD compared to BDD, ListDD and the multicore tool on explicit-state reachability. (Spoiler alert: it's quite a game changer.) The audience is invited to help find more applications of the MDD decision diagrams other than symbolic reachability in LTSmin.