Domagoj Babic and Zvonimir Rakamaric

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2011-108

October 3, 2011

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-108.pdf

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.

---

BibTeX citation:

@techreport{Babic:EECS-2011-108,
    Author= {Babic, Domagoj and Rakamaric, Zvonimir},
    Title= {Asynchronously Communicating Visibly Pushdown Systems},
    Year= {2011},
    Month= {Oct},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-108.html},
    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.},
}

EndNote citation:

%0 Report
%A Babic, Domagoj 
%A Rakamaric, Zvonimir 
%T Asynchronously Communicating Visibly Pushdown Systems
%I EECS Department, University of California, Berkeley
%D 2011
%8 October 3
%@ UCB/EECS-2011-108
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-108.html
%F Babic:EECS-2011-108