Global progress for dynamically interleaved multiparty sessions

摘要

A multiparty session forms a unit of structured communication among many participantsrnwhich follow communication sequences specified as a global type. When a process isrnengaged in two or more sessions simultaneously, different sessions can be interleaved andrncan interfere at runtime. Previous work on multiparty session types has ignored sessionrninterleaving, providing a limited progress property ensured only within a single session, byrnassuming non-interference among different sessions and by forbidding delegation. This paperrndevelops, besides a more traditional, compositional communication type system, a novelrnstatic interaction type system for global progress in dynamically interleaved and interferedrnmultiparty sessions. The interaction type system infers causalities of channels making surernthat processes do not get stuck at intermediate stages of sessions also in presence ofrndelegation.