SYNCHRONIZATION CALCULUS FOR MESSAGE ORIENTED PROGRAMMING.

A calculus is outlined for studying in a systematic way the synchronization properties for message oriented programming. These properties include such things as absence/prescence of deadlocks, unpaired primitives, use of unbounded buffers (capacity of the channels involved in the communication), etc. In order to study these questions, a technique (called the synchronization tree) which is a finite representation for the reachability set is introduced. The main result presented is that, given any message oriented program, it is decidable whether the processes involved ever enter a configuration in which some subset of processes is deadlocked.