A carregar...
Publicação
Subtyping Context-Free Session Types
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.21 MB | Adobe PDF |
Resumo(s)
Os tipos de sessão [51, 52, 94] permitem a especificação de protocolos de comunicação em
canais bidirecionais e heterogéneos. Tipicamente, estas especificações incluem o tipo, direção e
ordem das mensagens, bem como pontos de ramificação onde os participantes podem escolher
como deve prosseguir a comunicação.
Ao suportar tipos de sessão, as linguagens de programação conseguem oferecer mais segurança na programação concorrente, permitindo ao seu verificador de tipos assegurar a fidelidade
das sessões (i.e., que a comunicação procede de acordo com o protocolo), a privacidade (i.e., que
os canais de comunicação são conhecidos apenas pelos participantes) e a integridade da comunicação (i.e., que não há incompatibilidades resultantes da ordem e tipos das mensagens). Em certas
formulações, também é possível assegurar que a comunicação nunca chega a um impasse [53].
Até recentemente, os tipos de sessão apenas permitiam a recursão terminal, e estavam, portanto, limitados à especificação de protocolos correspondentes a linguagens regulares (em particular, à união das linguagens regulares e ω-regulares). Esta classe de linguagens exclui muitos
protocolos de interesse prático, sendo o exemplo mais típico a serialização de dados com estrutura
de árvore num só canal. Os tipos de sessão livres de contexto, propostos por Thiemann e Vasconcelos [96], libertam os tipos de sessão desta restrição, permitindo a recursão não-terminal através
de um operador de composição sequencial que forma um monóide com o elemento neutro Skip
(um tipo que representa o protocolo vazio, i.e., sem ação). Tal como o nome indica, os tipos de
sessão livres de contexto conseguem especificar protocolos correspondentes a linguagens livres de
contexto (determinísticas e simples [62]), e são portanto consideravelmente mais expressivos que
os tipos de sessão convencionais.
Na sua busca pela fiabilidade, os tipos de sessão podem tornar a programação demasiado rígida
para os programadores. A subtipagem, um aspeto central de muitos sistemas de tipos, procura
aliviar a tensão entre a fiabilidade e a flexibilidade. É tipicamente justificada por um apelo ao
princípio da substituição segura de Liskov [65]: um tipo T é considerado subtipo de U se um
valor do tipo T puder ser usado no lugar de um valor do tipo U em qualquer contexto, sem violar
as propriedades desejáveis do sistema de tipos em questão.
O que significa dizer que um tipo de sessão livre de contexto é subtipo de outro? Uma possível
resposta, seguindo o princípio de Liskov, pode ser encontrada no influente trabalho de Gay e Hole
[42] sobre os tipos de sessão regulares: um tipo de sessão S é subtipo de R se um canal governado
pelo tipo S puder ser usado em qualquer contexto onde é esperado um canal governado pelo tipo R. De forma mais concreta, a subtipagem para tipos de sessão permite uma maior flexibilidade
nos tipos das mensagens trocadas e nas escolhas oferecidas aos participantes, sem comprometer
as garantias mencionadas acima. Na prática, esta flexibilidade promove a modularidade no desenvolvimento de software concorrente: o protocolo de um participante pode ser refinado, mantendo
intacto o do seu correspondente.
Enquanto que propriedades algorítmicas da subtipagem para os tipos de sessão regulares são
bem conhecidas (graças também ao trabalho de Gay e Hole), o mesmo não pode ser dito sobre os
os tipos de sessão livres de contexto. Os maiores desafios neste sentido são as suas propriedades
algébricas (identidade, associatividade, distributividade e absorção), a sua interpretação equirecursiva e a possibilidade de recursão não-terminal. A investigação de Padovani [82] sobre este tópico
mostrou que o problema da subtipagem para estes tipos, quando formulado segundo os princípios
clássicos de Gay e Hole, é indecidível—o preço habitual a pagar por mais expressividade.
Apesar destes desafios, propomos duas abordagens à subtipagem para os tipos de sessão livres de contexto: uma sintática e baseada em regras de inferência, e outra semântica e apoiada
numa nova noção de pré-ordem observacional a que chamamos de simulação-X YZW, uma generalização da noção de simulação-X Y proposta por Aarts e Vaandrager [1]. Esta relação permite
uma combinação seletiva dos requisitos da simulação simples, simulação inversa e de uma certa
forma de contra-simulação, o que lhe permite suportar a habitual covariância e contravariância
dos construtores de tipos de sessão na sua plenitude (em contraste, a relação proposta por Padovani
não permite qualquer variância nos tipos das mensagens).
A equivalência dos tipos de sessão livres de contexto é baseada na noção de bissimulação [83],
a qual a simulação-X YZW generaliza. Tirando partido deste facto, derivamos um algoritmo de
subtipagem a partir de um algoritmo de equivalência já existente [5]. O nosso algoritmo é correto
(i.e., as suas respostas afirmativas são verdadeiras) mas, devido à indecidibilidade do problema,
necessariamente incompleto.
Este algoritmo foi implementado no verificador de tipos da linguagem FREEST [2, 4, 95],
uma linguagem de programação funcional com suporte para tipos de sessão livres de contexto. De
forma a avaliar a sua performance, construímos um conjunto de 4000 testes, gerados automaticamente com a ajuda da biblioteca Quickcheck para a linguagem Haskell [22]. Obtivémos uma
performance satisfatória, observando apenas 200 timeouts. Para uma avaliação mais realista, e
de forma a comparar a nossa adaptação com o algoritmo original, corremos ambos os algoritmos
lado-a-lado num conjunto de 288 programas FREEST sem subtipagem. Nesta avaliação não observamos diferenças significativas de performance, o que sugere que a aplicação prática do nosso
algoritmo é viável.
O trabalho desenvolvido no âmbito desta tese foi apresentado na 34ª Conferência Internacional
de Teoria da Concorrência (CONCUR 2023) e no INForum 2023, Simpósio de Informática, e
publicado nas atas correspondentes sob a forma de artigo [90] e resumo [92], respetivamente.
Session types allow the specification of structured communication protocols on bidirectional, heterogeneously typed channels. Typically, these specifications include the type, direction and order of messages, as well as branching points where participants can choose how communication should proceed. By supporting session types, programming languages are able to offer safer concurrency, ensuring session fidelity, privacy and communication safety. Until recently, session types were restricted to the description of regular, tail-recursive protocols, considerably limiting their expressiveness. Context-free session types liberate themselves from this restriction by introducing a monoidal type operator to express the sequential composition of any two protocols, making them significantly more expressive. However, in their quest for safe concurrency, session types can make programming too rigid. Subtyping, an important feature of many type systems, is meant to alleviate this tension between safety and flexibility. While the algorithmic properties of subtyping for regular session types are by now well known, the same cannot be said for their context-free counterparts. The main challenges in this respect are the algebraic properties they exhibit, along with their equirecursive interpretation. A previous investigation into this topic by Padovani has shown this problem to be undecidable—the usual, unfortunate price to pay for expressive power. Despite these challenges, we propose two novel approaches to subtyping for context-free session types: one syntactic and based on inference rules, and another semantic and based on a novel kind of observational preorder we call X YZW-simulation, which generalizes X Y-simulation and therefore also bisimulation, on which type equivalence for context-free session types is often based. We take advantage of this fact to derive a sound (but, due to the undecidability of the problem, necessarily incomplete) subtyping algorithm from an existing type equivalence algorithm. We then present an empirical evaluation of its performance in the context of a programming language compiler.
Session types allow the specification of structured communication protocols on bidirectional, heterogeneously typed channels. Typically, these specifications include the type, direction and order of messages, as well as branching points where participants can choose how communication should proceed. By supporting session types, programming languages are able to offer safer concurrency, ensuring session fidelity, privacy and communication safety. Until recently, session types were restricted to the description of regular, tail-recursive protocols, considerably limiting their expressiveness. Context-free session types liberate themselves from this restriction by introducing a monoidal type operator to express the sequential composition of any two protocols, making them significantly more expressive. However, in their quest for safe concurrency, session types can make programming too rigid. Subtyping, an important feature of many type systems, is meant to alleviate this tension between safety and flexibility. While the algorithmic properties of subtyping for regular session types are by now well known, the same cannot be said for their context-free counterparts. The main challenges in this respect are the algebraic properties they exhibit, along with their equirecursive interpretation. A previous investigation into this topic by Padovani has shown this problem to be undecidable—the usual, unfortunate price to pay for expressive power. Despite these challenges, we propose two novel approaches to subtyping for context-free session types: one syntactic and based on inference rules, and another semantic and based on a novel kind of observational preorder we call X YZW-simulation, which generalizes X Y-simulation and therefore also bisimulation, on which type equivalence for context-free session types is often based. We take advantage of this fact to derive a sound (but, due to the undecidability of the problem, necessarily incomplete) subtyping algorithm from an existing type equivalence algorithm. We then present an empirical evaluation of its performance in the context of a programming language compiler.
Descrição
Tese de mestrado, Informática , 2024, Universidade de Lisboa, Faculdade de Ciências
Palavras-chave
Tipos de sessão Subtipagem Simulação Recursão não-terminal Gramáticas simples Teses de mestrado - 2024