Termination of Probabilistic Concurrent Programs

Sergiu Hart, Micha Sharir and Amir Pnueli


   
(Acrobat PDF files)


Abstract

The asynchronous execution behavior of several concurrent processes, which may use randomization, is studied. Viewing each process as a discrete Markov chain over the set of common execution states, necessary and sufficient conditions are given for the processes to converge almost surely to a given set of goal states under any fair, but otherwise arbitrary, schedule, provided that the state space is finite. (These conditions can be checked mechanically.) An interesting feature of the proof method is that it depends only on the topology of the transitions and not on the actual values of the probabilities. It is also shown that in this model synchronization protocols that use randomization are in certain cases no more powerful than deterministic protocols. This is demonstrated by (1) establishing lower bounds, similar to those known for deterministic protocols, on the size of a shared variable necessary to ensure mutual exclusion and lockout-free behavior of a "randomized" protocol and (2) showing that no fully symmetric "randomized" protocol can ensure mutual exclusion and freedom from lockout.

Categories and Subject Descriptors:

General Terms: Algorithms, Theory, Verification

Additional Key Words and Phrases: Program analysis, Markov chains, ergodic sets


Related papers on probabilistic programs by S. Hart, A. Pnueli and M. Sharir: