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 | |
Rok publikování | 2005 |
Druh | Článek ve sborníku |
Konference | FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference |
Fakulta / Pracoviště MU | |
Citace | |
Obor | Informatika |
Klíčová slova | bounded reachability; symbolic reachability; asynchronous dynamic pushdown network |
Popis | 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í. |
Související projekty: |