Utilize este identificador para referenciar este registo: http://hdl.handle.net/10451/15855
Título: Synthesis of correct-by-construction MPI programs
Autor: Lemos, Filipe Emanuel Ventura Pires de Matos
Orientador: Vasconcelos, Vasco Thudichum, 1964-
Marques, Eduardo Resende Brandão
Palavras-chave: MPI
Tipos de sessão
Síntese de código
Verificação formal
Programação paralela
Teses de mestrado - 2014
Data de Defesa: 2014
Resumo: MPI (Message Passing Interface) é o padrão de programação concorrente mais usado em super-computadores. Devido à sua portabilidade, diversidade de funções e desenvolvimento constante, MPI é usado mundialmente em diversos campos de investigação, como na pesquisa de curas para o cancro, previsões metereológicas, investigação de fontes de energia alternativas e mais. Este tipo de programas contém trocas de mensagens complexas e operações colectivas que dificultam a sua implementação. Independentemente do talento ou cuidado do programador, é fácil introduzir erros que bloqueiam toda a execução do programa e a sua análise tornase igualmente complicada. Dada a complexidade e importância das áreas em que o MPI é usado, ferramentas que facilitem o desenvolvimento e análise deste tipo de programas são necessárias. Ferramentas actuais para análise de código MPI usam técnicas refinadas como a verificação de modelos ou execução simbólica. Na maioria dos casos estas soluções não acompanham a escalabilidade dos programas, sendo fiáveis até 1024 processos, pouco quando comparado com as aplicações MPI que correm em computadores com milhares de processadores. Os programadores de aplicações paralelas têm lidar com duas partes principais: a parte de computação e a parte de comunicação. Computação representa a parte lógica e aritmética do programa, enquanto que a coordenação refere-se à interação entre processos / participantes. A programação paralela inclui frequentemente programação de baixo nível. Mesmo primitivas MPI usadas para enviar mensagens contém um mínimo de seis parâmetros. Ao desenvolver aplicações paralelas complexas, lidar com funções de baixo nível pode ser um aborrecimento. Se de alguma forma fosse possível contornar esta questão, o desenvolvimento de aplicações paralelas seria muito mais fácil. Misturar computação com comunicação complica ainda mais esta tarefa, pelo que há uma necessidade de dividir as duas partes, tanto para fins de modificabilidade como de organização. Esqueletos de aplicações paralelas podem ser definidos de muitas maneiras, mas o conceito principal é que o esqueleto permite que os programadores tenham uma visão de topo da parte de comunicação do programa, dando-lhes uma estrutura correcta à partida, aliviando o seu trabalho. Assim sendo, o foco do desenvolvimento recai na parte de computação do programa. A ferramenta MPI Sessions, criada antes do ínicio desta tese mas na qual esta se insere, difere das restantes ferramentas de verificação MPI pela possibilidade de usar análise estática para verificar propriedades ligadas à concorrencia, possivelmente em tempo polinomial. A framework, criada antes do ínicio desta tese, baseia-se na teoria dos tipos de sessão multi-participante. A teoria dos tipos de sessão passa por caracterizar o padrão de comunicação entre vários processos de um programa e, verificando-se que os participantes seguem o protocolo de comunicação especificado, é garantido que certas propriedades como a ausencia de interbloqueio e coerencia de tipos são garantidas. O desafio encontrasse na forma de analisar se certo programa C+MPI obedece a um protocolo de comunicação especificado. Para este fim é usado o VCC, um verificador de programas C desenvolvido pela Microsoft Research. O processo de uso do MPI Sessions passa por primeiro especificar um protocolo de comunicação, numa linguagem desenvolvida para este fim, num plugin Eclipse que avalia automaticamente se o protocolo está bem formado. Se sim, o plugin traduz automaticamente o protocolo para um formato reconhecido pelo VCC. Para guiar o processo de validação são necessárias anotações no código fonte, nomeadamente nas funções MPI e operadores de controlo de fluxo. Estas anotações ajudam a identificar os campos das funções MPI que vão ser comparadas com o que está especificado no protocolo, a fim de identificar se a ordem de operações no código corresponde à que está no protocolo. No caso das funções MPI criou-se uma biblioteca especial que contém contractos para cada função. Esta biblioteca é incluida no ficheiro fonte pelo que apenas as anotações relacionadas com o controlo de fluxo têm de ser inseridas manualmente. Este tese estende as funcionalidades da ferramenta MPI Sessions, possibilitando a síntese de um esqueleto C+MPI fiel ao protocolo de comunicação especificado. Este esqueleto contém a parte de comunicação programa e dita o seu fluxo de execução. O esqueleto é composto por funções MPI e por chamadas a funções a ser definidas pelo utilizador, a parte de computação do programa. A ferramenta complementa automáticamente o código gerado com anotações VCC, permitindo a verificação da fidelidade do código ao protocolo - portanto, o programa contém uma prova que certifica a sua correcção. As funções de computação complementares são fornecidas pelo utilizador sob a forma de funções “callback”, usadas para definir os buffers de dados a serem transmitidos ou armazenados durante/após a comunicação, as condições envolvidas na implementação de ciclos e escolhas, e as funções de processamento de dados. Devido a uma especificação de protocolos aumentada, com marcas simples que identificam os pontos de funções “callback”, é possível ligar esqueleto ao código a ser definido pelo utilizador. A ferramenta consome estas marcas e gera um cabeçalho C com os protótipos necessários (assinaturas) para as funções “callback” que serão implementadas pelo utilizador. O código gerado e o definido pelo utilizador podem então ser compilados juntamente com a biblioteca MPI instalada no sistema para obter um executável. Em suma, a nossa abordagem tem as seguintes características principais: 1. Protocolos de comunicação apartir dos quais é feita a síntese automática de programas C+MPI. As etapas manuais do desenvolvimento do programa são apenas a definição do próprio protocolo, e a implementação de funções “callback” necessárias ao controle do fluxo de dados e as funções de processamento. 2. A correção do código sintetizado é certificada, também de forma automatizada, através das anotações de verificação que são copuladas com o esqueleto C+MPI. 3. A abordagem utiliza a infra-estrutura MPI Sessions já em existente para a especificação e verificação de protocolos MPI. Os aperfeiçoamentos compreendem a síntese “back-end” que se alimenta da estrutura de protocolos e o uso de marcas adicionais dentro do protocolo para definir funções “callback”. As nossa solução foi testada com recurso a sete programas MPI, obtidos em livros de texto e da “suite” de “benchmark” FEVS [2]. Através da especificação de protocolos de comunicação, baseados nesses programas, comparámos os tempos de execução dos programas síntetizados com os programas originais (a fim de verificarmos a qualidade dos programas gerados), o número de linhas de código geradas automáticamente, a diferença de linhas de código entre as duas versões (a fim de termos uma primeira noção se o esforço do utilizador é diminuído seguindo o nosso método). É também apresentada uma análise dos tempos de verificação para cada um dos exemplos e as anotações geradas automáticamente necessárias para essa verificação. Concluíndo, é definido o processo de síntese de código C+MPI funcional e correcto, com base em protocolos de comunicação aumentados para esse propósito e que seguem a teoria de tipos de sessão multi-participante. São explicadas as alterações feitas ao plugin para acomodar as mudanças necessárias para suportar a síntese de código, bem como outras funcionalidades adicionadas para facilitar o uso do plugin. É validado o nosso trabalho através de vários testes que avaliam tanto a parte funcional dos programas gerados (tempo de execução), bem como a vantagem da nossa solução face ao processo desenvolvimento normal - os programas gerados são correctos por construção. Na conclusão são propostas várias ideias para a continuidade do melhoramento não só da vertente de síntese da ferramenta, bem como do projecto como um todo. O resultado é uma ferramenta funcional e útil, disponibilizada publicamente na internet, incluindo exemplos prontos a usar e um manual práctico.
Message Passing Interface (MPI) is the de facto standard for programming high performance parallel applications, with implementations that support hundreds of thousands of processing cores. MPI programs, written in C or Fortran, adhere to the Single Program Multiple Data (SPMD) paradigm, in which a single program specifies the behavior of the various processes, each working on different data, and that communicate through message-passing. Errors in MPI programs are easy to introduce, given the complexity in designing parallel programs and of MPI itself, plus the low-level and unchecked semantics of C and Fortran. One can easily write programs that cause processes to deadlock waiting for messages, or that exchange data of mismatched type or length. In the general case, it is impossible to certify that a program avoids these errors, or that it overall complies with an intended communication pattern. To deal with this general problem, we propose the synthesis of C+MPI programs from well-founded protocol specifications, based on the theory of multiparty session types. The idea is to depart from a high-level protocol specification that defines an intended communication pattern, and automatically synthesize a C+MPI code skeleton that is faithful to the source protocol specification. To define the functionality of a complete program, the skeleton needs only to be complemented by user-provided functions that do not employ any MPI calls, and merely implement the bindings for the skeleton’s control and data flow logic. The underlying multiparty session types’ theory ensures the preservation of key properties from protocol specification to synthesized code, such as deadlock freedom and type safety. For certification of the whole synthesis process, the C+MPI skeleton also includes annotations that are processed by a software verifier to mechanically verify compliance with the protocol. This thesis presents the design, implementation, and evaluation of the proposed approach, within a software framework called MPI Sessions.
Descrição: Tese de mestrado, Engenharia Informática (Engenharia de Software), Universidade de Lisboa, Faculdade de Ciências, 2014
URI: http://hdl.handle.net/10451/15855
Designação: Mestrado em Engenharia Informática (Engenharia de Software)
Aparece nas colecções:FC-DI - Master Thesis (dissertation)

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
ulfc112322_tm_Filipe_Lemos.pdf2,23 MBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.