Making Session Types Go

Abstract

The ubiquitous nature of today’s multi-core processors means concurrency is ever more important to effectively use available computing resources. By its very nature however, concurrent programming is complex and error-prone - accounting for random process interleavings and managing shared resource control is difficult and can lead to instances of incorrect behavior or deadlocks in concurrent programs. As such, ensuring the cor- rectness of concurrent programs is of the utmost importance. Session types are a typing discipline for message-passing concurrency that is able to ensure strong compile-time correctness guarantees for concurrent programs by providing a protocols-as-types view of communication. In particular, we make use of the interpretation of intuitionistic linear logic formulas as session types, which serves as the basis for logical session types. These logical session types offer stronger guarantees at compile-time than simple session types. In this work we implement a (logically) session-typed functional language, along with its associated type checker, and develop a compiler for said language targeting the Go language. Our work features standard functional programming features combined with channel-based, session-typed, concurrency primitives and thread spawning. Concurrency and pure functional values are separated via a monad-like interface, in the style of Haskell. Our compilation pipeline takes a program, type checks it to ensure the absence of dead- locks and communication errors, and then translates it to valid Go code, leveraging Go’s channel and lightweight thread infrastructure. The translation requires compensating the mismatch between Go’s channel types and session types, which we achieve via a state machine view of session types. We showcase the expressiveness of our language via a series of examples, encoding concurrency idioms in the style of map-reduce, among others. We also perform a performance evaluation of our implementation, experimenting with different settings and testing it against a native Go implementation. We follow with a discussion of the experimental results. Finally, we end by discussing possible approaches to future work, namely in terms of compiler optimizations and increase in language expressiveness.

Atualmente, a natureza ubíqua de processadores multi-core faz da concorrência algo cada vez mais importante para utilização eficaz dos recursos. Mas a programação concorrente é complexa e dada a erros – antecipar a execução intercalada de processos e gerir o controlo de recursos partilhados é difícil; pode levar a comportamento incorreto, ou deadlocks em programas concorrentes. Assim, assegurar a correção de programas concorrentes é da maior importância. Tipos de sessão são uma disciplina de tipos para concorrência baseada na troca de mensagens que é capaz de dar fortes garantias de correção em tempo de com- pilação para programas concorrentes, oferecendo uma visão da comunicação em termos de protocolos-como-tipos. Utilizamos a interpretação de fórmulas da lógica linear intuici- onista como tipos de sessão, que serve de base para tipos de sessão lógicos que oferecem garantias mais fortes do que tipos de sessão simples. Neste trabalho implementamos uma linguagem funcional, com tipos de sessão (lógicos), juntamente com o seu type checker, e desenvolvemos um compilador para a dita linguagem que tem por alvo a linguagem Go. A linguagem apresenta as funcionalidades standard da programação funcional, combinadas com thread spawning e primitivas de concorrência baseadas em canais e tipificadas com tipos de sessão. A concorrência e valores funcionais são separados por uma interface tipo monad, ao estilo de Haskell. O processo de compilação recebe um programa, verifica o seu tipo para assegurar a ausência de deadlocks e erros de comunicação, e tradu-lo para código Go, utilizando a infraestrutura de canais e lightweight threads de Go. A tradução implica uma compensação da diferença entre os tipos de canais em Go e os tipos de sessão, que alcançamos através duma visão de tipos de sessão como máquinas de estados. Demons- tramos a expressividade da linguagem através duma série de exemplos, implementando idiomas de concorrência como map-reduce, entre outros. Realizamos uma avaliação de desempenho da implementação, experimentado definições diferentes e testando-a contra uma implementação nativa em Go, discutindo depois os resultados experimentais. Por fim, propomos várias abordagens para trabalho futuro, em termos de optimização do compilador e aumento da expressividade da linguagem.