Utilize este identificador para referenciar este registo: http://hdl.handle.net/10451/12406
Título: Static verification of data races in openMP
Autor: Silva, Kátya Thaís Martins da
Orientador: Mostrous, Dimitris, 1979-
Palavras-chave: Boogie
Data race
OpenMP
Paralelismo
Verificação
Teses de mestrado - 2014
Data de Defesa: 2014
Resumo: Com o uso de linguagens paralelas nascem alguns problemas como data race , uma argura para os programadores durante o seu trabalho. Data race são quando dois ou mais threads em um único processo acedem a mesma posic¸ ão de memória ao mesmo tempo, sendo que um ou mais acessos são para a escrita/leitura, sem sincronização adequada. A nossa ferramenta (SVDR: Static Verification of Data race in OpenMP) foi desenvolvida com o propósito de verificar a ausência de data races em OpenMP (uma linguagem de programac¸ ão paralela). Empregamos a verificação estática com intençãoo de encontrar data races sem necessariamente executar o programa, possibilitando dessa forma ao utilizador, encontrar o problema antes de receber o resultado do mesmo. Para melhor compreensão de como funciona a ferramenta, é pertinente apresentar de forma concisa, as linguagens de programac¸ ˜ao aqui abordadas: OpenMP e Boogie. OpenMP (Aberto Multi-Processing) 2.1 ´e um API usado na programação (C, Fortran, C++) em multiprocessadores com memória partilhada em multiplataformas e funciona em quase todos Sistemas operativos e arquitecturas. Boogie [2, 17] ´e uma linguagem de verificação intermédia, projectada como uma camada sobre a qual é possível construir outros verificadores para outras línguaguens. Uma vez aclaradas as definições, é mais fácil contextualizar e compreender como a ferramenta funciona. Como já foi referido previamente, o objectivo da ferramenta é traduzir código OpenMP em código Boogie com o propósito de verificar se existe ou não data race no ficheiro de entrada. Assim sendo, é possível aferir que existem duas etapas para o processo de verificação: a primeira é a tradução de OpenMP em Boogie, e a segunda é a verificação de data race no ficheiro de entrada - que é do tipo bpl, ou seja, código Boogie. A primeira fase não é tratado pela ferramenta, de modo que é necessária uma tradução manual do código OpenMP para o código Boogie. A segunda fase é a ferramenta que foi implementada, SVDR. O SVDR funciona da seguinte forma: recebe como entrada um ficheiro bpl (um OpenMP traduzido em código Boogie) e retorna como resultado um ficheiro bpl com o algoritmo necessário para verificar se há ou não um data race no ficheiro de entrada. O algoritmo criado é baseado no uso de não determinismo, invariantes e assertions. Este funciona do seguinte modo, para verificar a existência de data race num ciclo While, o que se faz é guardar numa variável global, que designamos de current off, o valor actual do índice do array (independentemente de se tratar de uma leitura ou uma escrita, o processo é o mesmo), e atribuir a outra variável global, que denominamos de current,o valor de true. Após guardados os referidos valores, o que se faz a seguir, é a incrementação do ciclo, atribuímos os valores do current e do current off a duas novas variáveis globais previous e previous off. Estas atribuições são feitas para evitar que se aceda duas vezes seguidas a mesma posição, porque isso poderia conduzir a data race. Tanto as atribuições de current como de previous, são feitas dentro de if não determinísticos. Não determinismo é por definição “Uma propriedade da computação na qual pode ter um ou mais resultados”, mas neste caso especifico significa que não é possível saber se entra ou não no if. A razão para o seu uso, é apenas a não necessidade, neste caso, de se guardar todos os valores do currrent, e mudar todos os valores do previous (até porque se tivermos em consideração todas as possibilidade de execução do programa, haverá sempre uma para cada tarefa). Depois de guardados os valores é necessário validá-los de alguma forma, até porque senão, seriam apenas if num programa, ou seja, não teriam nenhum efeito especifico. A modo utilizado para verificar, é empregando assercoes, ou seja, criamos um assert na qual se afirma que caso o previous seja verdadeiro, então o previous off será sempre diferente do índex actual do vector. Caso isto seja verdade, ou seja, caso se ocorra no programa a veracidade dessa afirmação, então não existem data race, caso contrário, existem. Mas para que esse assert seja sempre verdade, durante o programa, é indispensável a criação de uma invariant para suportar a sua veracidade. No nosso caso, as invariantes são testadas usando Houdini 2.2. São criadas bases de invariantes pela ferramenta, que posteriormente ao realizar-se a verificação do ficheiro com o algoritmo no Verificador Boogie, adiciona um atributo relativo ao Houdini. Por fim, para saber se existe ou não data race no código, utilizamos o Verificador Boogie para atestar o programa com o algoritmo. Como conclusão, o que se pode dizer é que a ferramenta apresentou resultados bastante satisfatórios, e que em todos os exemplos apresentados e testados, o efeito foi o esperado. Apesar de algumas limitações, a ferramenta cumpre com o que foi descrito anteriormente Verifica estaticamente a existência de data race na linguagem OpenMP.
Increasingly, programmers use multi-core processors to develop code with multiple threads, i.e, parallel programs. There are some tools that support parallelism such as Intel Parallel Lint 2.4.1 or Intel Thread checker 2.4.2 and some parallel programming languages such as OpenMP 2.1. With the use of parallel languages emerged some problems such as data races that no programmer likes to come across when working. Data races are when two or more threads in a single process access the same memory location concurrently and one or more of the accesses are for writing without proper synchronization. Our tool (SVDR: Static Verification of Data race in OpenMP) was developed with the intention to verify data race freedom in OpenMP (a parallel programming language). We used static verification because we wanted to try to find data races without running the program because that way the user discovers the problem before getting results from the program. The SVDR tool works as follows: it receives as input a bpl file (a file with the translated OpenMP code into Boogie code), then the tool performs executes the algorithm on the input, and gives as output the execution, i.e, the Boogie code with the algorithm necessary to verify if there is or not a data race. Next the output of the SVDR is going to be used as input in the Boogie Verifier that will determine whether or not there exists a data race in the input. If there is a data race then the verifier will give an error, otherwise the verifier will verifies the code without any problem. After several tests it was possible for us to verify that the tool works correctly in all tests that we ran. The examples that we ran were with nested loops, but just one of them was parallel, and also with simple loops, with reads and writes, and all of the examples were verified as expected by the Boogie Verifier. The tool is useful to help the user to verify is exists any data race problem in code so that they can solve the problem if it exists.
Descrição: Tese de mestrado em Engenharia Informática (Engenharia de Software), Universidade de Lisboa, Faculdade de Ciências, 2014
URI: http://hdl.handle.net/10451/12406
Designação: Mestrado em Engenharia Informática
Aparece nas colecções:FC-DI - Master Thesis (dissertation)

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
ulfc111930_tm_Kátya_Silva.pdf568,38 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.