A carregar...
Publicação
Handle with Care and Confidence – Extending Cameleer with Algebraic Effects and Effect Handlers. An analysis of algebraic effects and techniques to deductively verify them
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.88 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
The new major release of the OCaml compiler is set to be an important landmark in the
history and ecosystem of the language. The 5.0 version introduces Multicore OCaml, a
multi-threaded implementation of the OCaml runtime. Two new important paradigms
shall arise in the language: parallelism via domains and direct-style concurrency via
algebraic effects and handlers. In this work, we focus precisely on the latter and try to
answer the following research question: "what tools and principles must be developed
in order to apply automated deductive proofs to OCaml programs featuring effects and
handlers?".
Algebraic effects and handlers are a powerful abstraction to build non-local control-flow
mechanisms such as resumable exceptions, lightweight threads, co-routines, generators,
and asynchronous I/O. All of such features have very evolved semantics, hence they pose
very interesting challenges to deductive verification techniques. In fact, there are very
few proposed techniques to deductively verify programs featuring these constructs, even
fewer when it comes to automated proofs. In this report, we outline some of the currently
available techniques for the verification of programs with algebraic effects. We then build
off them to create a mostly automated verification framework by extending Cameleer, a
tool which verifies OCaml code using GOSPEL and Why3. This framework embeds the
behavior of effects and handlers using exceptions and defunctionalized functions.
A próxima iteração do compilador OCaml será histórica no que diz respeito ao ecosistema da linguagem. A versão 5.0 introduzirá Multicore OCaml, uma implementação multi- threaded do runtime OCaml. Nesta versão, dois paradigmas serão adicionados: paralelismo utilizando domains e concorrência em estilo direto na forma de efeitos algébricos e handlers. Neste relatório, focar-nos-emos no segundo ponto, tentado responder à seguinte questão: "que ferramentas e princípios deveremos desenvolver de modo a applicar provas dedutivas automáticas a programas com efeitos e handlers?". Efeitos algébricos e handlers são uma abstrações poderosas que nos permite construir mecanismos para controlar o curso de um programa como, por exemplo, exceções que nos permitem recomeçar a computação, threads lightwheight, corotinas, geradores e I/O asíncrono. Todos estes paradigmas são um grande desafio no contexto de verificação dedutiva pois têm semanticas bastante complexas. Neste relatório iremos abordar algumas das técnicas existentes para provar programas com efeitos algébricos. Ademais, propomos uma estratégia de verificação para provar automáticamente programas com handlers. Para este efeito, extendemos a ferramenta Cameleer, um verificador de código OCaml que utiliza a linguagem de especificação GOSPEL e o prover Why3. Esta extensão visa aproximar o comportamento de handlers utilizando exceções e funções desfuncionalizadas.
A próxima iteração do compilador OCaml será histórica no que diz respeito ao ecosistema da linguagem. A versão 5.0 introduzirá Multicore OCaml, uma implementação multi- threaded do runtime OCaml. Nesta versão, dois paradigmas serão adicionados: paralelismo utilizando domains e concorrência em estilo direto na forma de efeitos algébricos e handlers. Neste relatório, focar-nos-emos no segundo ponto, tentado responder à seguinte questão: "que ferramentas e princípios deveremos desenvolver de modo a applicar provas dedutivas automáticas a programas com efeitos e handlers?". Efeitos algébricos e handlers são uma abstrações poderosas que nos permite construir mecanismos para controlar o curso de um programa como, por exemplo, exceções que nos permitem recomeçar a computação, threads lightwheight, corotinas, geradores e I/O asíncrono. Todos estes paradigmas são um grande desafio no contexto de verificação dedutiva pois têm semanticas bastante complexas. Neste relatório iremos abordar algumas das técnicas existentes para provar programas com efeitos algébricos. Ademais, propomos uma estratégia de verificação para provar automáticamente programas com handlers. Para este efeito, extendemos a ferramenta Cameleer, um verificador de código OCaml que utiliza a linguagem de especificação GOSPEL e o prover Why3. Esta extensão visa aproximar o comportamento de handlers utilizando exceções e funções desfuncionalizadas.
Descrição
Palavras-chave
Deductive Verification Algebraic Effects Effect Handlers Multicore OCaml GOSPEL Why3