Uma linguagem de programação com tipos de sessão independentes do contexto

Tese de mestrado, Engenharia Informática (Engenharia de Software) Universidade de Lisboa, Faculdade de Ciências, 2018Os sistemas de software distribuídos têm uma comunicação intensiva onde a complexidade do padrão de mensagens trocadas entre processos tende a tornar a codificação dos mesmos difícil. As tecnologias existentes na área do software concorrente não são muito apropriadas ao desenvolvimento deste tipo de sistemas onde a comunicação é intensiva e bastante complexa devido ao elevado número de mensagens que são trocadas entre processos. É necessário definir mecanismos que permitam verificar se uma determinada sequência de interações feitas num canal de comunicação está bem estruturada e se está de acordo com um protocolo predefinido. Os tipos de sessão foram desenvolvidos com o objetivo de colmatar as lacunas existentes no software concorrente com comunicação intensiva. Permitem definir protocolos que, recorrendo a tipos, representam uma “interação correta” do sistema e ainda garantem outras propriedades como a inexistência de erros na comunicação e de situações de impasse. Garantem também que uma mensagem é recebida ou que a comunicação num canal termina. Têm uma estrutura com recursividade terminal que implica que os protocolos que definem sejam descritos por uma linguagem regular. No entanto, têm limitações na sua estrutura que impossibilitam a descrição eficiente de estruturas em forma de árvore. Os tipos de sessão livres do contexto foram apresentados como uma extensão dos tipos de sessão tradicionais e descrevem estruturas que não são possíveis de descrever recorrendo aos tipos de sessão tradicionais. Neste caso, os protocolos são descritos por linguagens determinísticas livres do contexto. Deste trabalho resulta uma linguagem de programação chamada FreeST que é concorrente e explicitamente tipificada, onde os processos comunicam exclusivamente por troca de mensagens. Esta linguagem recorre a tipos de sessão independentes de contexto de modo a estender a expressividade dos tipos de sessão tradicionais e possibilitar a implementação, com segurança de tipos, de operações remotas em tipos de dados recursivos.The society is highly dependent on software systems that are distributed and communication centered. The available tecnologies on this field are not well suited to develop systems with an intensive communication due to the large number of messages that are exchanged between processes. So, there is a need to establish protocols that are able to verify if a communication between parties is well formed in terms of the sequences of operations performed on a communication channel. Session types were proposed as means to fulfil this kind of requirements such as defining the correct interaction or ensuring some safety properties like the abstence of communication errors and deadlocks. Liveness properties like the eventual receipt of a message or the termination of an interaction are also issues that can be addressed using these types. They describe structured interaction of processes on heterogeneously typed communication channels. This kind of types have a tail-recursive structure that imposes protocols that must be described by a regular language. However, they have a limitation in their structure that makes it impossible to describe, in an efficient way, tree structured data. Context-free session types extend the notion of session types by allowing protocols that aren’t tail-recursive and therefore are correspond to deterministic context-free languages. With this work we aim to offer a concurrent typed programming language called FreeST where processes communicate exclusively by message passing. Using context-free session types we intend to have a programming language that is able to describe the low-level serialization of tree-structured data in a type safe way