Negotiations: A Model for Tractable Concurrency.

点击翻译按钮获取中文摘要

Concurrency theory has devoted much effort to thestudy of a large variety of communication primitives, likeshared variables, point-to-point FIFO channels, rendez-vous, or reliable broadcasts. In particular, the complexity of verification problems for abstract machines communicating by means of these primitives is very well studied. Unfortunately,the worst-case complexity in the size of the system is very high, ranging from PSPACE-hard to lower bounds expressed in terms oftower of exponentials, or even non-primitive recursive functions. We have recently initiated the study of a novel communication primitive, called negotiation. Negotiation is a combination of synchronization and nondeterministic choice(the name is due to the fact that in a negotiation a numberof parties meet--i.e., synchronize--in order to select one outof a number of outcomes--i.e., to conduct a nondeterministic choice).In order to conduct our study, we have introduced negotiation diagrams,a concurrency model with atomic negotiations as primitive. The modelis close to 1-safe colored Petri nets. Our work has identified a subclass of the model, called deterministicnegotiation diagrams, that exhibits exceptionally good properties. In particular, even though the model is subject tothe state-explosion problem, fundamental properties like soundness(a property similar to absence of deadlocks and livelocks) can be checked in polynomial time. We have alsodesigned a small programming language which captures exactly the sounddeterministic negotiation diagrams. Taking deterministic negotiation diagrams as starting point, we propose to study increasingly expressive models of concurrent systems,while at the same time remaining below the PSPACE complexity barrier.While the motivation of this work is mostly theoretical,we will use the results to design a small programminglanguage for parallel programs, together with a simple Hoare logic, and tool support to automatically produce distributedimplementations of programs.