Interprocess communications: deadlock conditions

This work is concerned with the behaviour of system composed by several asynchronous modules. In particular, systems whose modules communicate by means of send and receive primitives are considered and deadlock conditions, that may arise by using these message passing primitives, are analyzed. For this purpose we introduce a formal model based on computation schemata. First of all we introduce sequential schemata and then we define cyclic sequential schemata in order to model cyclic sequential processes. Systems composed by a set of concurrent processes are modelled by means of parallel combination of cyclic sequential schemata. On the ground of both processes structure and connections structure, systems are classified in three types: 1) time and data independent systems; 2) data dependent and time independent systems; 3) time and data dependent systems. For the first two types of system a set of properties are proved. In particular,for first type of system we prove that: if a deadlock condition arises in a particular computation, then the same deadlock condition will arise in every computation. For the second type of systems a similar argument can be proved, that is: if, given a set of input data, a deadlock condition arises in a particular computation, then,with the same input data, the same deadlock condition will arise in every computation.