Binary decision diagrams on modern hardware

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F23%3A00137597" target="_blank" >RIV/00216224:14330/23:00137597 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20" target="_blank" >https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_20</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.34727/2023/isbn.978-3-85448-060-0_20" target="_blank" >10.34727/2023/isbn.978-3-85448-060-0_20</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Binary decision diagrams on modern hardware

Popis výsledku v původním jazyce

Binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores.

Název v anglickém jazyce

Binary decision diagrams on modern hardware

Popis výsledku anglicky

Binary decision diagrams (BDDs) are one of the fundamental data structures in formal methods and computer science in general. However, the performance of BDD-based algorithms greatly depends on memory latency due to the reliance on large hash tables and thus, by extension, on the speed of random memory access. This hinders the full utilisation of resources available on modern CPUs, since the absolute memory latency has not improved significantly for at least a decade. In this paper, we explore several implementation techniques that improve the performance of BDD manipulation either through enhanced memory locality or by partially eliminating random memory access. On a benchmark suite of 600+ BDDs derived from real-world applications, we demonstrate runtime that is comparable or better than parallelising the same operations on eight CPU cores.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2023

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023

ISBN

9783854480600

ISSN

—

e-ISSN

2708-7824

Počet stran výsledku

10

Strana od-do

122-131

Název nakladatele

TU Wien Academic Press

Místo vydání

Vienna

Místo konání akce

Ames, Iowa

Datum konání akce

1. 1. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—