License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2008.1739
URN: urn:nbn:de:0030-drops-17398
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1739/
Go to the corresponding LIPIcs Volume Portal

Atig, Mohamed Faouzi ; Bouajjani, Ahmed ; Touili, Tayssir

Analyzing Asynchronous Programs with Preemption

pdf-format:
08004.AtigMohamed.1739.pdf (0.5 MB)

Abstract

Multiset pushdown systems have been introduced by Sen and
Viswanathan as an adequate model for asynchronous programs where
some procedure calls can be stored as tasks to be processed
later. The model is a pushdown system supplied with a multiset of
pending tasks. Tasks may be added to the multiset at each
transition, whereas a task is taken from the multiset only when
the stack is empty. In this paper, we consider an extension of
these models where tasks may be of different priority level, and
can be preempted at any point of their execution by tasks of
higher priority. We investigate the control point reachability
problem for these models. Our main result is that this problem is
decidable by reduction to the reachability problem for a
decidable class of Petri nets with inhibitor arcs. We also
identify two subclasses of these models for which the control
point reachability problem is reducible respectively to the
reachability problem and to the coverability problem for Petri
nets (without inhibitor arcs).

BibTeX - Entry

@InProceedings{atig_et_al:LIPIcs:2008:1739,
  author =	{Mohamed Faouzi Atig and Ahmed Bouajjani and Tayssir Touili},
  title =	{{Analyzing Asynchronous  Programs with Preemption}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{37--48},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Ramesh Hariharan and Madhavan Mukund and V Vinay},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2008/1739},
  URN =		{urn:nbn:de:0030-drops-17398},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1739},
  annote =	{Keywords: Multiset Pushdown Systems, Multithreaded Asynchronous Programs, Program verification, Verification algorithms}
}

Keywords: Multiset Pushdown Systems, Multithreaded Asynchronous Programs, Program verification, Verification algorithms
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue Date: 2008
Date of publication: 05.12.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI