Reachability Analysis of Multithreaded Software with Asynchronous Communication

BOUAJJANI, Ahmed; Javier ESPARZA; Stefan SCHWOON a Jan STREJČEK. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005, s. 348-359. ISBN 3-540-30495-9.

Základní údaje

Originální název

Reachability Analysis of Multithreaded Software with Asynchronous Communication

Název česky

Analýza dosažitelnosti pro vícevláknové programy s asynchronní komunikací

Autoři

BOUAJJANI, Ahmed; Javier ESPARZA; Stefan SCHWOON a Jan STREJČEK

Vydání

Berlin, Heidelberg, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, od s. 348-359, 12 s. 2005

Nakladatel

Springer-Verlag

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/05:00012714

Organizační jednotka

Fakulta informatiky

ISBN

3-540-30495-9

UT WoS

000234885800028

Klíčová slova anglicky

bounded reachability; symbolic reachability; asynchronous dynamic pushdown network

Štítky

asynchronous dynamic pushdown network, bounded reachability, symbolic reachability

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We introduce Asynchronous Dynamic Pushdown Networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) [QR05] and DPN (dynamic pushdown networks) [BMOT05]. We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem [QR05], which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations.

Česky

Představujeme Asynchronni dynamické zásobníkové sítě (ADPN) jako nový model pro vícevláknové programy, ve kterém zásobníkové systémy komunikují přes sdílenou paměť. ADPN zobecňuje CPS (souběžné zásobníkové systémy) [QR05] a DPN (dynamické zásobníkové sítě) [BMOT05]. Ukážeme, že ADPN mají několik výhod. Jelikož problém dosažitelnosti pro ADPN je nerozhodnutelný i pro případ bez dynamického vytváření procesů, zabýváme se problémem omezené dosažitelnosti [QR05], který uvažuje jenom ty výpočetní běhy, kde počet změn (indexu) procesu mometálně přistupujícímu ke sdílené paměti omezen daným číslem. Poskytujeme efektivní algoritmy pro analýzu dopředné i zpětné dosažitelnosti. Tyto algoritmy využívají známé techniky pracující s automaty, které reprezentují množiny konfigurací.

---

Návaznosti

GA201/03/1161, projekt VaV	Název: Verifikace nekonečně stavových systémů Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky