ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 10:30 - 11:00 at SUN I - Concurrent and Distributed Systems Chair(s): Marieke Huisman

Saturation is an efficient exploration order for computing the set of reachable states symbolically. Attempts to parallelize saturation have so far resulted in limited speedup. We demonstrate for the first time that on-the-fly symbolic saturation can be successfully parallelized at a large scale. To this end, we implemented saturation in Sylvan’s multi-core decision diagrams used by the LTSmin model checker. We report extensive experiments, measuring the speedup of parallel symbolic saturation on a 48-core machine, and compare it with the speedup of parallel symbolic BFS and chaining. We find that the parallel scalability varies from quite modest to excellent. We also compared the speedup of on-the-fly saturation and saturation for pre-learned transition relations. Finally, we compared our implementation of saturation with the existing sequential implementation based on Meddly. The empirical evaluation uses Petri nets from the model checking contest, but thanks to the architecture of LTSmin, parallel on-the-fly saturation is now available to multiple specification languages.

Wed 10 Apr

tacas-2019-papers
10:30 - 12:30: TACAS 2019 - Concurrent and Distributed Systems at SUN I
Chair(s): Marieke HuismanUniversity of Twente
tacas-2019-papers10:30 - 11:00
Talk
Tom van DijkUniversity of Twente, Jeroen Meijer, Jaco van de PolAarhus University
Link to publication
tacas-2019-papers11:00 - 11:30
Talk
Si Liu, Peter Ölveczky, Min ZhangEast China Normal University, Qi Wang, José Meseguer
Link to publication
tacas-2019-papers11:30 - 12:00
Talk
Link to publication
tacas-2019-papers12:00 - 12:30
Talk
Marius BozgaVerimag/CNRS, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Joseph SifakisVerimag/CNRS
Link to publication