A GPU Tree Database for Many-Core Explicit State Space Exploration

Anton Wijs; Muhammad Osama

doi:10.1007/978-3-031-30823-9_35

A GPU Tree Database for Many-Core Explicit State Space Exploration

Anton Wijs (Corresponding author)
, Muhammad Osama

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

5 Citations (Scopus)

16 Downloads (Pure)

Abstract

Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to implement a tree database to store states as binary trees in GPU memory. We present fine-grained parallel algorithms to find and store trees, experiment with a number of GPU-specific configurations, and propose a novel hashing technique, called Cleary-Cuckoo hashing, which enables the use of Cleary compression on GPUs. We are the first to assess the effectiveness of using a tree database, and Cleary compression, on GPUs. Experiments show processing speeds of up to 131 million states per second.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I
Editors	Sriram Sankaranarayanan, Natasha Sharygina
Place of Publication	Cham
Publisher	Springer
Pages	684-703
Number of pages	20
ISBN (Electronic)	978-3-031-30823-9
ISBN (Print)	978-3-031-30822-2
DOIs	https://doi.org/10.1007/978-3-031-30823-9_35
Publication status	Published - 22 Apr 2023
Event	29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023) - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023 https://etaps.org/2023/tacas

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	13993
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023)
Abbreviated title	TACAS 2023
Country/Territory	France
City	Paris
Period	22/04/23 → 27/04/23
Internet address	https://etaps.org/2023/tacas

Keywords

Explicit state space exploration
GPU
finite-state machines

Access to Document

10.1007/978-3-031-30823-9_35

pdfFinal published version, 1.01 MBLicence: CC BY

Cite this

Wijs, A., & Osama, M. (2023). A GPU Tree Database for Many-Core Explicit State Space Exploration. In S. Sankaranarayanan, & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I (pp. 684-703). (Lecture Notes in Computer Science (LNCS); Vol. 13993). Springer. https://doi.org/10.1007/978-3-031-30823-9_35

Wijs, Anton ; Osama, Muhammad. / A GPU Tree Database for Many-Core Explicit State Space Exploration. Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I. editor / Sriram Sankaranarayanan ; Natasha Sharygina. Cham : Springer, 2023. pp. 684-703 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{8f9c3c3b02f240d7bb857342cfbb9339,

title = "A GPU Tree Database for Many-Core Explicit State Space Exploration",

abstract = "Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to implement a tree database to store states as binary trees in GPU memory. We present fine-grained parallel algorithms to find and store trees, experiment with a number of GPU-specific configurations, and propose a novel hashing technique, called Cleary-Cuckoo hashing, which enables the use of Cleary compression on GPUs. We are the first to assess the effectiveness of using a tree database, and Cleary compression, on GPUs. Experiments show processing speeds of up to 131 million states per second.",

keywords = "Explicit state space exploration, GPU, finite-state machines",

author = "Anton Wijs and Muhammad Osama",

year = "2023",

month = apr,

day = "22",

doi = "10.1007/978-3-031-30823-9\_35",

language = "English",

isbn = "978-3-031-30822-2",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "684--703",

editor = "Sriram Sankaranarayanan and Natasha Sharygina",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), TACAS 2023 ; Conference date: 22-04-2023 Through 27-04-2023",

url = "https://etaps.org/2023/tacas",

}

Wijs, A & Osama, M 2023, A GPU Tree Database for Many-Core Explicit State Space Exploration. in S Sankaranarayanan & N Sharygina (eds), Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I. Lecture Notes in Computer Science (LNCS), vol. 13993, Springer, Cham, pp. 684-703, 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Paris, France, 22/04/23. https://doi.org/10.1007/978-3-031-30823-9_35

A GPU Tree Database for Many-Core Explicit State Space Exploration. / Wijs, Anton (Corresponding author); Osama, Muhammad.
Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I. ed. / Sriram Sankaranarayanan; Natasha Sharygina. Cham: Springer, 2023. p. 684-703 (Lecture Notes in Computer Science (LNCS); Vol. 13993).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A GPU Tree Database for Many-Core Explicit State Space Exploration

AU - Wijs, Anton

AU - Osama, Muhammad

PY - 2023/4/22

Y1 - 2023/4/22

N2 - Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to implement a tree database to store states as binary trees in GPU memory. We present fine-grained parallel algorithms to find and store trees, experiment with a number of GPU-specific configurations, and propose a novel hashing technique, called Cleary-Cuckoo hashing, which enables the use of Cleary compression on GPUs. We are the first to assess the effectiveness of using a tree database, and Cleary compression, on GPUs. Experiments show processing speeds of up to 131 million states per second.

AB - Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to implement a tree database to store states as binary trees in GPU memory. We present fine-grained parallel algorithms to find and store trees, experiment with a number of GPU-specific configurations, and propose a novel hashing technique, called Cleary-Cuckoo hashing, which enables the use of Cleary compression on GPUs. We are the first to assess the effectiveness of using a tree database, and Cleary compression, on GPUs. Experiments show processing speeds of up to 131 million states per second.

KW - Explicit state space exploration

KW - GPU

KW - finite-state machines

UR - https://www.scopus.com/pages/publications/85161460354

U2 - 10.1007/978-3-031-30823-9_35

DO - 10.1007/978-3-031-30823-9_35

M3 - Conference contribution

SN - 978-3-031-30822-2

T3 - Lecture Notes in Computer Science (LNCS)

SP - 684

EP - 703

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Sankaranarayanan, Sriram

A2 - Sharygina, Natasha

PB - Springer

CY - Cham

T2 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023)

Y2 - 22 April 2023 through 27 April 2023

ER -

Wijs A, Osama M. A GPU Tree Database for Many-Core Explicit State Space Exploration. In Sankaranarayanan S, Sharygina N, editors, Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I. Cham: Springer. 2023. p. 684-703. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-031-30823-9_35

A GPU Tree Database for Many-Core Explicit State Space Exploration

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this