Parallel Partial Order Reduction with Topological Sort Proviso

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Parallel Partial Order Reduction with Topological Sort Proviso. In Software Engineering and Formal Methods (SEFM 2010). Los Alamos: IEEE Computer Society Press, 2010, p. 222-231. ISBN 978-0-7695-4153-2.

Basic information

• Original name: Parallel Partial Order Reduction with Topological Sort Proviso
• Name in Czech: Paralelní redukce částečného uspořádání s využitím topologického třídění
• Authors: BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and Petr ROČKAI (703 Slovakia, belonging to the institution).
• Edition: Los Alamos, Software Engineering and Formal Methods (SEFM 2010), p. 222-231, 10 pp. 2010.
• Publisher: IEEE Computer Society Press

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Italy
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: printed version "print"
• RIV identification code: RIV/00216224:14330/10:00045912
• Organization unit: Faculty of Informatics
• ISBN: 978-0-7695-4153-2
• Keywords (in Czech): LTL ověřování modelu; Redukce čístečného uspořádání; Paralelní a distribuované výpočty; DiVinE
• Keywords in English: LTL Model Checking; Partial Order Reduction; Parallel and Distributed Processing; DiVinE
• Tags: International impact, Reviewed

Abstract

Partial order reduction and distributed-memory processing are the two essential techniques to fight the wellknown state space explosion problem in explicit state model checking. Unfortunately, these two techniques have not been integrated yet to a satisfactory degree. The main source of difficulties is the cycle proviso that requires one fully expanded state on every cycle in the reduced state space graph. In this paper we suggest a new technique that guarantees correct construction of the reduced state space graph w.r.t. the cycle proviso. Our new technique is fully compatible with the parallel graph traversal procedure while at the same time it provides competitive reduction of the state space if compared to the serial case. The new technique has been implemented within the parallel and distributed-memory LTL model checker DIVINE and its performance is reported in this paper.

Abstract (in Czech)

Redukce částečného uspořádání a počítáni v distribuované paměti jsou dvě klíčové techniky pro boj se stavovou explozí v kontextu enumerativní verifikace. Hlavním výsledkem této práce je nový paralelní algoritmus pro výpočet množiny vrcholů pokrývající všechny cykly v grafu, který umožňuje uspokojivou integraci obou klíčových technik. Nová technika byla implementována v rámci nástroje DiVinE.

Links

• GA201/09/1389, research and development project: Name: Verifikace a analýza velmi velkých počítačových systémů

Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems

• GP201/09/P497, research and development project: Name: Automatizovaná formální verifikace s využitím soudobého hardware

Investor: Czech Science Foundation, Automated formal verification using modern hardware

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• MUNI/A/0914/2009, interní kód MU: Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)

Investor: Masaryk University, Category A

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science