Modular composition of session types

Abstract

En el campo de los sistemas distribuidos, lograr la coordinación entre diversas unidades de cómputo y sub-sistemas es una tarea compleja, pues cada unidad de computo se comporta distinta a las demás, de forma concurrente y de manera descentralizada. Con el fin de expresar como diversas unidades de computo se comunican unas con otras, se utilizan definiciones de protocolos. Session types son una disciplina de tipos que permite lograr la coordinación entre muchos participantes de un sistema distribuido, mediante la definición de un protocolo coreográfico. La disciplina de tipos impone condiciones sobre la coreografía con el fin de asegurar que el sistema distribuido que la implementa se comporta de la forma en la que fue definido y además posee garantías sobre propiedades de la comunicación. Entre las propiedades importantes se encuentran la ausencia de: deadlocks, mensajes huérfanos y recepciones inesperadas de mensajes. La coreografía es expresada como una entidad global, la cual es projectada a distintos tipos, uno para cada participante involucrado en la coreografía. Dichos tipos son usados para un proceso de typecheck que verifica que las implementaciones de las unidades distribuidas, llamadas procesos, se comportaran en la interacción global como se espera. Se muestra que lograr modularidad en session types no es trivial. Para ello, se presenta un caso de estudio en el que el uso de definiciones modulares para session types introduce problemas en el comportamiento global luego de su composición. Comenzando desde el caso de estudio, se explica como se introducen dichos problemas al componer sub-sessiones. Se muestra como los problemas globales pueden ser evitados gracias al uso de un mecanismo de composición que se basa en interacciones de bloqueo entre participantes. En este trabajo se desarrolla una extensión de un sistema de tipos que permite la composición modular de session types (MCST). MCST se basa en condiciones impuestas sobre definiciones modulares de sub-sessiones, además de un sistema de tipos que permite verificar sub-sessiones por separado, y un mecanismo de composición que produce sistemas bien formados. La solución presentada es modular, dado que mantiene sus definiciones separadas con el fin de reusarlas. Las condiciones para verificar correctitud no dependen del contexto en el cual una sub-session es llamada.El mecanismo de composición reusa conceptos de inlining y composición con ciclos de trabajos previos, haciéndolas aplicables en más casos, lo que resulta en un sistema más expresivo. MCST mantiene las garantías de comunicación de session types mencionadas previamente. Ademas, MCST mejora la expresividad de session types, dado que la nueva disciplina de tipos con el mecanismo de composición permite definir coreografías que no son permitidas en el estado del arte de session types.