Context-Bounded Analysis of Concurrent Queue Systems

Provided by: University of Illinois at Urbana Champaign
Topic: Big Data
Format: PDF
The authors show that the bounded context-switching reachability problem for concurrent finite systems communicating using unbounded FIFO queues is decidable, where in each context a process reads from only one queue (but is allowed to write onto all other queues). Their result also holds when individual processes are finite-state recursive programs provided a process dequeues messages only when its local stack is empty. They then proceed to classify architectures that admit a decidable (un-bounded context switching) reachability problem, using the decidability of bounded context switching.

Find By Topic