Termination of Probabilistic Concurrent Programs
Sergiu Hart, Micha Sharir and Amir Pnueli
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 lockoutfree 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:
 D.1.3 [Programming Techniques]:
Concurrent Programming
 D.2.4 [Software Engineering]:
Program Verification  correctness proofs
 D.4.1 [Operating Systems]:
Process Management  concurrency; mutual exclusion;
scheduling; synchronization
 G.3 [Mathematics of Computing]: Probability and
Statistics  probabilistic algorithms (including Monte Carlo)
General Terms: Algorithms, Theory, Verification
Additional Key Words and
Phrases: Program analysis, Markov chains, ergodic sets

Proceedings of the 9th Annual ACM Symposium on Principles of
Programming Languages (POPL) (1982), 16
[Extended Abstract]

ACM Transactions on Programming Languages and Systems
(TOPLAS) 5 (1983), 3, 356380
[Full Paper]
Related papers on probabilistic programs by S. Hart, A. Pnueli
and M. Sharir: