Utilize este identificador para referenciar este registo: http://hdl.handle.net/10451/10051
Título: Formal verification of parallel C+MPI programs
Autor: Martins, Nuno Alexandre Dias
Orientador: Marques, Eduardo Resende Brandão
Vasconcelos, Vasco Thudichum, 1964-
Palavras-chave: MPI
Programação paralela
Verificação
Tipos de sessão
Teses de mestrado - 2013
Data de Defesa: 2013
Resumo: O Message Passing Interface (MPI) [6] é o padrão de referência para a programação de aplicações paralelas de alto desempenho em plataformas de execução que podem ir até centenas de milhares de cores. O MPI pode ser utilizado em programas C ou Fortran, sendo baseado no paradigma de troca de mensagens. De acordo com o paradigma Single Program, Multiple Data (SPMD), um único programa define o comportamento de vários processos, utilizando chamadas a primitivas MPI, como por exemplo para comunicações ponto-a-ponto ou para comunicações colectivas. O uso de MPI levanta questões de fiabilidade, uma vez que é muito fácil escrever um programa contendo um processo que bloqueie indefinidamente enquanto espera por uma mensagem, ou que o tipo e a dimensão dos dados enviados e esperados por dois processos não coincidam. Assim, não é possível garantir à partida (em tempo de compilação) uma série de propriedades fundamentais sobre a execução de um programa. Lidar com este desafio não é de todo trivial. A verificação de programas MPI utiliza tipicamente técnicas avançadas como a verificação de modelos ou execução simbólica [9, 39]. Estas abordagens deparam-se frequentemente com o problema de escalabilidade, dado o espaço de estados do processo de verificação crescer exponencialmente com o número de processos considerados. A verificação em tempo útil pode estar limitada a menos de uma dezena de processos na verificação de aplicações real-world [41]. A verificação é ainda adicionalmente complicada por outros aspectos, como a existência de diversos tipos de primitivas MPI com diferentes semânticas de comunicação [39], ou a dificuldade em destrinçar o fluxo colectivo e individual de processos num único corpo comum de código [2]. A abordagem considerada para a verificação de programas MPI é baseada em tipos de sessão multi-participante [19]. A ideia base passa por especificar o protocolo de comunicação a ser respeitado por um conjunto de participantes que comunicam entre si trocando mensagens. A partir de um protocolo expresso desta forma, é possível extrair por sua vez o protocolo local de cada um dos participantes, segundo uma noção de projecção de comportamentos. Se para cada participante (processo) no programa MPI se verificar a aderência ao protocolo local respectivo, são garantidas propriedades como a ausência de condições de impasse e a segurança de tipos. A verificação desta aderência é feita sobre programas C que usam MPI, usando a ferramenta VCC da Microsoft Research [5]. Para codificar protocolos, foi utilizada uma linguagem formal de descrição de protocolos, apropriada à expressão dos padrões mais comuns de programas MPI. A partir de um protocolo expresso nessa linguagem. é gerado um header C que exprime o tipo num formato compatível com a ferramenta VCC [5]. Para além da codificação protocolo, a verificação é ainda guiada por um conjunto de contratos pré-definidos para primitivas MPI e por anotações no corpo do programa C. As anotações no programa são geradas automaticamente ou, em número tipicamente mais reduzido, introduzidas pelo programador. Os protocolos que regem as comunicações globais num programa MPI são especificados numa linguagem de protocolos, desenhada especificamente para o efeito no contexto do projecto MULTICORE em complemento ao trabalho desta tese, e em associação um plugin Eclipse que verifica a boa formação dos protocolos e que gera a codificação do protocolo na linguagem VCC. As ações básicas dos protocolos descrevem no caso geral primitivas MPI, por exemplo para comunicação ponto-a-ponto ou comunicação colectiva. Os valores associados a ações podem ser do género inteiro ou vírgula flutuante, bem como vectores. Além disso, qualquer um destes géneros pode ser refinado com imposição de restrições aos valores dos dados. As ações básicas são compostas através de operadores de sequência, iteração, e ainda de fluxo de controlo coletivo em correspondência a escolhas ou ciclos executados de forma síncrona por todos os participantes. A partir da especificação de um protocolo, a sua tradução no formato VCC define uma função de projecção. A função de projecção toma como argumento o índice do processo MPI, conhecido como rank, e devolve a codificação de um protocolo local a ser verificado para execução do participante, em linha com o enunciado pela noção de projeção [19]. Esta codificação reflecte de resto todas as características gerais da especificação do protocolo, em termos de ações básicas, o uso de tipos refinados, e operadores de composição. O processo de verificação tem por fim certificar a aderência do programa C+MPI face ao protocolo, para cada participante. Entre a inicialização e o término das comunicaçoes MPI, a verificação deve operar a redução progressiva do protocolo até ao protocolo vazio. As reduções são definidas mediante pontos de chamadas a primitivas MPI e características do fluxo de controlo de programa. Para manter o estado, a verificação manipula uma variável “fantasma” desde o ponto de entrada da programa (a função main()) que representa o protocolo. Para além da aderência ao protocolo, são ainda verificados aspectos complementares, como por exemplo se os dados usam regiões válidas de memória. Esta verificação usa um corpo base de definições, a que chamamos a “MPI anotada”. A MPI anotada compreende a lógica de protocolos e um corpo de contratos para um conjunto de primitivas MPI. A lógica de protocolos permite definir a estrutura de protocolos e definir as regras de redução, enquanto que os contratos das primitivas definem casos base para redução via ações de comunicação. Este corpo base pode ser importado para o contexto de verificação de um programa em particular, mediante a inclusão de um header C, a versão anotada do header convencional da MPI (mpi.h) [6]. Usando esta lógica base, o programa C pode ser anotado para verificação. As anotações relacionam-se com uma diversidade de aspectos que impactam da verificação do programa, tais como o fluxo de controlo colectivo, contratos de funções, invariantes de ciclos, asserções respeitantes ao uso de memória, ou a declaração de assunções até aí implícitas no comportamento do programa. O processo de anotação é um desafio para um programador, já que requer o domínio de uma lógica complexa de verificação. Para automatizar o processo, foi desenvolvido um anotador que gera uma parte significativa das anotações necessárias, transformando código C usando a biblioteca clang/LLVM [4]. O seu funcionamento base guia-se por anotações de alto nível para identificação de fluxo de controlo relevante e marcas de anotação simples introduzidas pelo programador, por forma a gerar em correspondência a um conjunto mais vasto e complexo de anotações. Após este processo automático, há anotações complementares que têm de ser introduzidas manualmente para a verificação bem sucedida de um programa. Estas últimas relacionam-se com aspectos diversos que ou são de inferência complexa, por exemplo o uso de memória, ou ainda não tratados na aproximação atual com um processo automatizado. Esta aproximação à verificação de programas C+MPI foi testada com um conjunto de exemplos tirados de livros de texto. Além de demonstrar a aplicabilidade da aproximação geral considerada, é apresentada uma análise do esforço de anotação e do tempo de verificação. O esforço de anotação mede a comparação entre o número de anotações automáticas face ao número de anotações manuais, verificando-se no caso geral que o número de anotações manuais é inferior ao número das automáticas. O tempo de verificação diz respeito ao tempo de execução da ferramenta VCC para o código anotado final de um programa. A análise de escalabilidade do mesmo face a um número crescente de processos permitiu identificar casos distintos: casos em que o tempo de execução é insensível ao número de processos e outros em que este tempo cresce exponencialmente face ao número de processos. Em conclusão, é definida uma metodologia para a verificação formal de programas MPI e demonstrada a sua aplicabilidade, combinando os paradigmas da teoria de tipos de sessão multi-participante e da verificação dedutiva de programas. Para lidar com uma maior gama de programas MPI, em particular programas real-world, ao longo do texto foram discutidos vários desafios que se colocam para uma evolução da metodologia, de tipo conceptual ou relacionados com a automação e escalabilidade. Para lidar com esses desafios, propõe-se na parte final um conjunto de linhas gerais para trabalho futuro.
Message Passing Interface (MPI) is the de facto standard for message-based parallel applications. Two decades after the first version of its specification, MPI applications routinely execute on supercomputers and computer clusters. MPI programs incarnate the Single Program Multiple Data (SPMD) paradigm. A single body of code, written in C or Fortran, defines the behavior of all participant processes in a program. The number of processes is defined at runtime, and any partial distinction of behavior between participants is based on the unique rank (numerical identifier) of each process. The communication between processes is defined through point-to-point or collective communication primitives. As a result, programs may easily exhibit intricate behaviors mixing collective and participant-specific flow, making it difficult to verify a priori desirable properties like absence of deadlocks or adherence to a desired communication protocol. In line with the concern for verifiable program behavior in MPI, the theory of multiparty session types provides a framework for well-structured communication protocols by an arbitrary number of participant processes. By construction, a multi-party global protocol declares a desired interaction behavior that guarantees properties such as type safety and absence of deadlocks, and implicitly defines the individual local protocols per participant. Provided that the actual program specification of each participant conforms to the corresponding local protocol, the safety properties and the intended choreography of the global protocol are preserved by the program. This thesis proposes the application of multi-party session type theory to C+MPI programs, coupled with the use of deductive software verification. A framework is proposed for the expression of multi-party session protocols in the MPI context and their verification using a deductive software tool. The framework also addresses concerns for automation through semi-automatic annotation of verification logic in program code. An evaluation of the applicability of the approach is conducted over a sample set of programs.
Descrição: Tese de mestrado em Engenharia Informática (Engenharia de software), apresentada à Universidade de Lisboa, através da Faculdade de Ciências, 2013
URI: http://hdl.handle.net/10451/10051
Aparece nas colecções:FC - Dissertações de Mestrado

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
ulfc105872_tm_Nuno_Alexandre_Martins.pdf624,63 kBAdobe 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.