Protocol based programming of concurrent systems

Tese de mestrado, Engenharia Informática (Engenharia de Software), Universidade de Lisboa, Faculdade de Ciências, 2014Desenvolver sistemas de software concorrentes (e paralelos) seguros é difícil. É muito mais difícil verificar software paralelo do que é fazer o mesmo para aplicações sequenciais. A Message Passing Interface (MPI) é uma especificação independente de linguagem para protocolos de comunicação, utilizada para programar computadores paralelos e baseada no paradigma de troca de mensagens, seguindo o paradigma Single Program Multiple Data (SMPD) em que um único pedaço de código é partilhado por todos os processos. Programas MPI apresentam uma séria de desafios de correção: o tipo de dados trocados na comunicação pode não corresponder, o que resulta em computações erradas, ou o programa pode entrar numa situação de impasse resultando em recursos desperdiçados. Este trabalho tem como objective melhorar o estado-da-arte da verificação de programas paralelos. O estado-da-arte na verificação de programas MPI utiliza técnicas de verificação de modelos que não escalam com o número de processos e são tipicamente feitas em tempo de execução, o que desperdiça recursos e está dependente da qualidade do conjunto de testes. A nossa abordagem é inspirada em tipos de sessão multi-participante (multi-party session types). A teoria dos tipos de sessão parte da caracterização da comunicação entre vários processos de um programa de um ponto de vista global (mensagem do processo 0 para o processo 1 corresponderia a envio para o processo 1 no processo 0 e recebo do processo 0 no processo 1 localmente). A esta caracterização dá-se o nome de protocolo. Protocolos bem formados são por construção livres de impasse e a comunicação é correcta (o tipo de dados enviado é o mesmo que o tipo de dados recebido). Se for provado que um programa segue um protocolo, então essas mesmas propriedades (ausência de impasses e correcção na comunicação) são preservadas para o programa. Primeiro, um protocolo é especificado numa linguagem desenhada para o efeito. As primitivas suportadas pela linguagem de protocolos são baseadas nas primitivas MPI, com a adição de escolhas e ciclos colectivos. Estas primitivas representam tomadas de decisão colectivas que não recorrerem a comunicação. Tomadas de decisão colectivas acontecem em programas SPMD porque todos os processos partilham o mesmo código, e como tal é possível garantir que todos os programas calculam o mesmo valor num certo ponto do programa se os dados forem iguais. Além disso, foi adicionada uma primitiva foreach, que expande um pedaço de protocolo para uma gama de valores. Esta primitiva permite que protocolos sejam paramétricos quanto ao número de processos. Os dados enviados nas mensagens podem ter restrições associadas, especificadas recorrendo a tipos dependentes. Os protocolos são escritos num plugin Eclipse. O plugin valida a boa formação dos protocolos com base numa teoria, utilizando o SMT solver Z3 da Microsoft Research para provar certas propriedades, e que as restrições nos tipos dependentes são congruentes. O plugin foi implementado recorrendo a Xtext, uma framework para desenvolvimentos de plugins Eclipse. O plugin, além de validar a boa formação, compila os protocolos para vários formatos, entre os quais o formato Why. Why é uma das linguagens da plataforma Why3, uma plataforma para verificação dedutiva de software. A linguagem Why é utilizada para escrever teorias, e é aliada à linguagem WhyML (inspirada em OCaml) para escrita de programas. Foi desenvolvida em Why uma teoria para protocolos, em que protocolos são especificados como um tipo de dados da linguagem. O ficheiro gerado pelo plugin especifica um protocolo utilizando os construtores deste tipo de dados Para especificar as restrições de tipos dependentes, uma teoria de funções anónimas incluída com a plataforma Why3 é utilizada. Além disso, foi desenvolvida uma biblioteca WhyML para programação paralela. Esta biblioteca inclui primitivas inspiradas em MPI, e primitivas para escolhas colectivas e ciclos colectivos. Estas primitivas têm como pré-condição que a cabeça do protocolo é a primitiva esperada, e que os dados a serem enviados respeitam a restrição do tipo de dados a ser enviado. Todas as primitivas têm como parâmetro o estado actual do protocolo, e na sua pós-condição consomem a primitiva à cabeça. Graças a estas anotações é possível saber se o programa segue o protocolo, confirmando no final do programa se o protocolo foi consumido por completo. Dado um programa paralelo escrito em WhyML, o protocolo em formato Why e a teoria de protocolos, o programador pode utilizar o Why3 IDE para verificar a conformidade do programa face ao protocolo. O Why3 IDE permite dividir a prova em partes, e provar cada parte com um SMT solver diferente. Caso nenhum SMT solver seja capaz de provar uma das sub-provas, o programador pode recorrer a um proof assistant e tratar da sub-prova manualmente. Além das anotações de primitivas colectivas, o programador também precisa de por um anotação no final de cada bloco que verifica se o protocolo está vazio naquele ponto (sem a qual não é possível garantir que o protocolo foi seguido), de marcar que partes do código correspondem a que expansão da primitiva foreach, e precisa de adicionar variantes e invariantes aos ciclos. Em resumo, a nossa abordagem é a seguinte: 1. O programador escreve um protocolo que explicita globalmente a comunicação que deve ocorrer.2. Este protocolo, se bem formado, é correcto por construção. A comunicação é correcta e é livre de impasses.3. A boa formação do protocolo é feita num plugin Eclipse, que também o compila para vários formatos, entre os quais o formato Why. 4. O programador escreve o seu programa paralelo em WhyML, recorrendo a uma biblioteca de programação paralela inspirada em MPI desenvolvida neste projecto. 5. As primitivas da biblioteca são anotadas com pré e pós-condições que verificam a conformidade do programa face ao protocolo. 6. Oprograma, aliado ao protocolo em formato Why e a uma teoria de protocolos, é verificado no Why3 IDE 7. O Why3 IDE permite dividir a prova em partes, e provar cada parte com um SMT solver diferente. No caso em que nenhum SMT solver consiga tratar da sub-prova, o programador pode recorrer a um proof assistant e tratar da sub-prova manualmente. 8. Se o programa passar na verificação, as propriedades do protocolo (correcção na comunicação e ausência de empasses) são garantidas para o programa. Estas anotações impõe trabalho extra ao programador, mas são dentro do esperado para este tipo de ferramenta. A nossa solução foi testada com recurso a três programas MPI, obtidos em livros de texto. Foram verificados vários exemplos clássicos de programação paralela, adaptados de livros de texto. Comparativamente à ferramenta mais próxima (que utiliza o verificador de programas C, VCC), o número de anotações da nossa solução é menor, as anotações enquadram-se melhor com o código e o tempo de verificação é semelhante. No entanto, a nossa solução recorre a uma linguagem que não é apropriada para a industria, a linguagem WhyML. As linguagens C ou Fortran aliadas à biblioteca MPI são o gold standard para programação paralela de alta performance, e são as linguagens com que os programadores no ramo estão familiarizados. Como tal, para trabalho futuro, propomos o desenvolvimento de uma linguagem de alto nível o mais semelhante possível a C ou Fortran, com primitivas de programação paralela built-in, incluindo escolhas colectivas e ciclos colectivos. Esta linguagem deverá compilar para código C ou Fortran, convertendo as primitivas da linguagem em primitivas MPI. Este passo de conversão pode também optimizar o programa, recorrendo a primitivas de comunicação MPI mais eficientes que as usadas, sendo esta uma funcionalidade importante para programação paralela de alta performance cuja principal preocupação é a eficiência do programa. Compilando também para WhyML, estes programas podem ser verificados. E como as primitivas de programação paralela são built-in na linguagem, a grande maioria das anotações necessárias pode ser gerada automaticamente. É também necessário suportar mais funcionalidades MPI, incluindo comunicação assíncrona, topologias e comunicadores.Developing safe, concurrent (and parallel) software systems is hard. It is much more difficult to debug or verify parallel software than it is to do the same for sequential applications. The Message Passing Interface (MPI) [12] is a languageindependent specification for communication protocols, used to program parallel computers and based on the message-passing paradigm. MPI programs present a number of correctness challenges: communication may not match, resulting in errant computations, or the program may deadlock resulting in wasted resources. This work hopes to improve the state-of-the-art of MPI program verification. The state-of-the-art in MPI program verification relies on model-checking techniques which do not scale with the number of processes and are typically done at runtime, which wastes resources and is dependent on the quality of the test set. Our approach is inspired by multi-party session types. First, a protocol is specified in a language designed for the purpose. A well-formed protocol is communication-safe and deadlock free. An Eclipse plugin verifies the well-formation of the protocol, and compiles it to Why, a language of a deductive software verification platform called Why3. This compiled protocol, allied with a theory for protocols also written in Why, is used to verify parallel WhyML programs, WhyML being another language of the Why3 platform. If a program passes verification, the properties of communication safety and deadlock freedom are preserved for the program. This verification occurs at compile time and is not dependent on any kind of test set, avoiding the issues of model-checking techniques. We verified several parallel programs from textbooks using our approach