Mixed sessions (Q2055956): Difference between revisions

In the theory of concurrent systems, a choice between alternative actions is internal if the process, and external if its environment determines the choice. The most familiar example of this is input and output. A process sending an integer value to another process can be modelled by an interaction where the former process makes an internal choice between different integers, and the latter makes an external choice. In process algebras, also more general interactions are possible. For instance, each process may be happy with a set of values, in which case the choice is made nondeterministically from the intersection of these sets. If the intersection is empty, and if the processes are committed to the interaction (have no other choice), then deadlock results. Session types specify some aspects of the types of data in interactions and the order in which the interactions occur. Typically, they aim at guaranteeing at compile time that communication through a channel is correct in some sense. They have often been restricted to input-output type of communication. This study makes it possible to use internal and external choice in session types more liberally. This is promised to make programming more flexible and unify synchronisation/communication primitives. Programming is not restricted to the traditional distinction between servers and clients. The study presents how earlier session types can be interpreted or embedded in the new session types, and vice versa. It also proves that correct typing guarantees freedom of certain errors. However, freedom of deadlocks is not guaranteed. An implementation in typical message-passing architectures is sketched, with a brief discussion of its drawbacks. It is based on placing the decision of the choice into a broker process that may, but need not, be integrated into one of the original processes.