Asynchronously Communicating Visibly Pushdown Systems
[HTML]
[PDF]
[PS]
[PS.BZ2]
[VIEW]
Bibtex:
@techreport{babic11async,
Author = {Babi\'c, Domagoj and Rakamari\'c, Zvonimir},
Title = {{Asynchronously Communicating Visibly Pushdown Systems}},
Institution = {EECS Department, University of California, Berkeley},
Year = {2011},
Month = {Oct},
Number = {UCB/EECS-2011-108},
}
Abstract:
We introduce an automata-based formal model suitable for specifying,
modeling, analyzing, and verifying asynchronous task-based and
message-passing programs. Our model consists of visibly pushdown
automata communicating over unbounded reliable point-to-point
first-in-first-out queues. Such a combination unifies two branches of
research, one focused on task-based models, and the other on models of
message-passing programs. Our model generalizes previously proposed
models that have decidable reachability in several ways. Unlike
task-based models of asynchronous programs, our model allows sending and
receiving of messages even when stacks are not empty, without imposing
restrictions on the number of context-switches or communication
topology. Our model is strictly more general than the well-known
communicating finite-state machines and allows: (1) individual
components to be visibly pushdown automata, which are more suitable for
modeling (possibly recursive) programs, (2) the set of words (i.e.,
languages) of messages on queues to form a visibly pushdown language,
which permits modeling of remote procedure calls and simple forms of
counting, and (3) the relations formed by tuples of such languages to be
synchronized, which permits modeling of complex interactions among
processes. In spite of these generalizations, we prove that the
composite configuration and control-state reachability are still
decidable for our model.