Alors que l'informatique est devenue omniprésente dans notre société actuelle, assurer la qualité d'un logiciel revêt une importance grandissante. Pour accroître cette qualité, l'une des conditions à respecter est la correction du système. Dans cette thèse, nous nous intéressons plus particulièrement aux systèmes distribués mettant en œuvre un ou plusieurs programmes exécutés sur plusieurs machines qui communiquent entre elles à travers le réseau. Dans ce contexte, assurer leur correction est rendu plus difficile par leur hétérogénéité mais également par leurs spécificités communes. Les algorithmes correspondants sont parfois complexes et la prédiction de leur comportement difficilement réalisable sans une étude avancée. Les travaux réalisés au cours de cette thèse mettent en œuvre la vérification dynamique formelle de propriétés temporelles sur des applications distribuées. Cette approche consiste à vérifier l'implémentation réelle d'une application à travers son exécution. L'enjeu majeur est de réussir à appliquer les techniques associées au Model checking dans le cadre d'une vérification sur des implémentations réelles d'applications distribuées et non plus sur des modèles abstraits. Pour cela, nous proposons dans un premier temps une analyse sémantique dynamique par introspection mémoire d'un état système permettant de détecter des états sémantiquement identiques. Puis, nous mettons en œuvre la vérification dynamique formelle de certaines propriétés temporelles : les propriétés de vivacité, formulées à l'aide de la logique LTL_X, et le déterminisme des communications dans les applications MPI. Une évaluation de chacune de ces contributions est réalisée à travers plusieurs expériences / While computers have become ubiquitous in our current society, ensuring the software quality takes on an increasing importance. One of the requirements to enhance this quality is the system correctness. In this thesis, we are particularly interested in distributed systems implementing one or more programs executed on several machines which communicate with each other through a network. Ensuring the system correctness is more difficult in this context, due to their heterogeneity but also their common characteristics. Corresponding algorithms are sometimes complex and the prediction of their behavior may be difficult to realize without an advanced study. The work done during this thesis implement the dynamic formal verification of some temporal properties on legacy distributed applications. This approach consists of checking the real implementation of an application by its systematic execution. The challenge in this approach is how to apply the methods derived from Model checking in the context of the verification of legacy distributed applications (without access to source code) and no longer on abstract models. For that, we propose in a first step a dynamic semantic analysis of a system state permitting the detection of identical states. Then, we implement the dynamic formal verification of some temporal properties: liveness properties, specified with the LTL_X logic, and the communications determinism in MPI applications. These contributions are experimentaly validated and evaluated with different series of experiments

Nesta tese é apresentado um novo workflow de simulação para avaliar o desempenho do balanceamento de carga dinâmico baseado em sobre-decomposição aplicado a aplicações paralelas iterativas. Seus objetivos são realizar essa avaliação com modificações mínimas da aplicação e a baixo custo em termos de tempo e de sua necessidade de recursos computacionais. Muitas aplicações paralelas sofrem com desbalanceamento de carga dinâmico (temporal) que não pode ser tratado a nível de aplicação. Este pode ser causado por características intrínsecas da aplicação ou por fatores externos de hardware ou software. Como demonstrado nesta tese, tal desbalanceamento é encontrado mesmo em aplicações cujo código não aparenta qualquer dinamismo. Portanto, faz-se necessário utilizar mecanismo de balanceamento de carga dinâmico a nível de runtime. Este trabalho foca no balanceamento de carga dinâmico baseado em sobre-decomposição. No entanto, avaliar e ajustar o desempenho de tal técnica pode ser custoso. Isso geralmente requer modificações na aplicação e uma grande quantidade de execuções para obter resultados estatisticamente significativos com diferentes combinações de parâmetros de balanceamento de carga Além disso, para que essas medidas sejam úteis, são usualmente necessárias grandes alocações de recursos em um sistema de produção. Simulated Adaptive MPI (SAMPI), nosso workflow de simulação, emprega uma combinação de emulação sequencial e replay de rastros para reduzir os custos dessa avaliação. Tanto emulação sequencial como replay de rastros requerem um único nó computacional. Além disso, o replay demora apenas uma pequena fração do tempo de uma execução paralela real da aplicação. Adicionalmente à simulação de balanceamento de carga, foram desenvolvidas técnicas de agregação espacial e rescaling a nível de aplicação, as quais aceleram o processo de emulação. Para demonstrar os potenciais benefícios do balanceamento de carga dinâmico com sobre-decomposição, foram avaliados os ganhos de desempenho empregando essa técnica a uma aplicação iterativa paralela da área de geofísica (Ondes3D). Adaptive MPI (AMPI) foi utilizado para prover o suporte a balanceamento de carga dinâmico, resultando em ganhos de desempenho de até 36.58% em 288 cores de um cluster Essa avaliação também é usada pra ilustrar as dificuldades encontradas nesse processo, assim justificando o uso de simulação para facilitá-la. Para implementar o workflow SAMPI, foi utilizada a interface SMPI do simulador SimGrid, tanto no modo de emulação, como no de replay de rastros. Para validar esse simulador, foram comparadas execuções simuladas (SAMPI) e reais (AMPI) da aplicação Ondes3D. As simulações apresentaram uma evolução do balanceamento de carga bastante similar às execuções reais. Adicionalmente, SAMPI estimou com sucesso a melhor heurística de balanceamento de carga para os cenários testados. Além dessa validação, nesta tese é demonstrado o uso de SAMPI para exploração de parâmetros de balanceamento de carga e para planejamento de capacidade computacional. Quanto ao desempenho da simulação, estimamos que o workflow completo é capaz de simular a execução do Ondes3D com 24 combinações de parâmetros de balanceamento de carga em 5 horas para o nosso cenário de terremoto mais pesado e 3 horas para o mais leve. / In this thesis we present a novel simulation workflow to evaluate the performance of dynamic load balancing with over-decomposition applied to iterative parallel applications at low-cost. Its goals are to perform such evaluation with minimal application modification and at a low cost in terms of time and of resource requirements. Many parallel applications suffer from dynamic (temporal) load imbalance that can not be treated at the application level. It may be caused by intrinsic characteristics of the application or by external software and hardware factors. As demonstrated in this thesis, such dynamic imbalance can be found even in applications whose codes do not hint at any dynamism. Therefore, we need to rely on runtime dynamic load balancing mechanisms, such as dynamic load balancing based on over-decomposition. The problem is that evaluating and tuning the performance of such technique can be costly. This usually entails modifications to the application and a large number of executions to get statistically sound performance measurements with different load balancing parameter combinations. Moreover, useful and accurate measurements often require big resource allocations on a production cluster. Our simulation workflow, dubbed Simulated Adaptive MPI (SAMPI), employs a combined sequential emulation and trace-replay simulation approach to reduce the cost of such an evaluation Both sequential emulation and trace-replay require a single computer node. Additionally, the trace-replay simulation lasts a small fraction of the real-life parallel execution time of the application. Besides the basic SAMPI simulation, we developed spatial aggregation and applicationlevel rescaling techniques to speed-up the emulation process. To demonstrate the real-life performance benefits of dynamic load balance with over-decomposition, we evaluated the performance gains obtained by employing this technique on a iterative parallel geophysics application, called Ondes3D. Dynamic load balancing support was provided by Adaptive MPI (AMPI). This resulted in up to 36.58% performance improvement, on 288 cores of a cluster. This real-life evaluation also illustrates the difficulties found in this process, thus justifying the use of simulation. To implement the SAMPI workflow, we relied on SimGrid’s Simulated MPI (SMPI) interface in both emulation and trace-replay modes.To validate our simulator, we compared simulated (SAMPI) and real-life (AMPI) executions of Ondes3D. The simulations presented a load balance evolution very similar to real-life and were also successful in choosing the best load balancing heuristic for each scenario. Besides the validation, we demonstrate the use of SAMPI for load balancing parameter exploration and for computational capacity planning. As for the performance of the simulation itself, we roughly estimate that our full workflow can simulate the execution of Ondes3D with 24 different load balancing parameter combinations in 5 hours for our heavier earthquake scenario and in 3 hours for the lighter one.

Nesta tese é apresentado um novo workflow de simulação para avaliar o desempenho do balanceamento de carga dinâmico baseado em sobre-decomposição aplicado a aplicações paralelas iterativas. Seus objetivos são realizar essa avaliação com modificações mínimas da aplicação e a baixo custo em termos de tempo e de sua necessidade de recursos computacionais. Muitas aplicações paralelas sofrem com desbalanceamento de carga dinâmico (temporal) que não pode ser tratado a nível de aplicação. Este pode ser causado por características intrínsecas da aplicação ou por fatores externos de hardware ou software. Como demonstrado nesta tese, tal desbalanceamento é encontrado mesmo em aplicações cujo código não aparenta qualquer dinamismo. Portanto, faz-se necessário utilizar mecanismo de balanceamento de carga dinâmico a nível de runtime. Este trabalho foca no balanceamento de carga dinâmico baseado em sobre-decomposição. No entanto, avaliar e ajustar o desempenho de tal técnica pode ser custoso. Isso geralmente requer modificações na aplicação e uma grande quantidade de execuções para obter resultados estatisticamente significativos com diferentes combinações de parâmetros de balanceamento de carga Além disso, para que essas medidas sejam úteis, são usualmente necessárias grandes alocações de recursos em um sistema de produção. Simulated Adaptive MPI (SAMPI), nosso workflow de simulação, emprega uma combinação de emulação sequencial e replay de rastros para reduzir os custos dessa avaliação. Tanto emulação sequencial como replay de rastros requerem um único nó computacional. Além disso, o replay demora apenas uma pequena fração do tempo de uma execução paralela real da aplicação. Adicionalmente à simulação de balanceamento de carga, foram desenvolvidas técnicas de agregação espacial e rescaling a nível de aplicação, as quais aceleram o processo de emulação. Para demonstrar os potenciais benefícios do balanceamento de carga dinâmico com sobre-decomposição, foram avaliados os ganhos de desempenho empregando essa técnica a uma aplicação iterativa paralela da área de geofísica (Ondes3D). Adaptive MPI (AMPI) foi utilizado para prover o suporte a balanceamento de carga dinâmico, resultando em ganhos de desempenho de até 36.58% em 288 cores de um cluster Essa avaliação também é usada pra ilustrar as dificuldades encontradas nesse processo, assim justificando o uso de simulação para facilitá-la. Para implementar o workflow SAMPI, foi utilizada a interface SMPI do simulador SimGrid, tanto no modo de emulação, como no de replay de rastros. Para validar esse simulador, foram comparadas execuções simuladas (SAMPI) e reais (AMPI) da aplicação Ondes3D. As simulações apresentaram uma evolução do balanceamento de carga bastante similar às execuções reais. Adicionalmente, SAMPI estimou com sucesso a melhor heurística de balanceamento de carga para os cenários testados. Além dessa validação, nesta tese é demonstrado o uso de SAMPI para exploração de parâmetros de balanceamento de carga e para planejamento de capacidade computacional. Quanto ao desempenho da simulação, estimamos que o workflow completo é capaz de simular a execução do Ondes3D com 24 combinações de parâmetros de balanceamento de carga em 5 horas para o nosso cenário de terremoto mais pesado e 3 horas para o mais leve. / In this thesis we present a novel simulation workflow to evaluate the performance of dynamic load balancing with over-decomposition applied to iterative parallel applications at low-cost. Its goals are to perform such evaluation with minimal application modification and at a low cost in terms of time and of resource requirements. Many parallel applications suffer from dynamic (temporal) load imbalance that can not be treated at the application level. It may be caused by intrinsic characteristics of the application or by external software and hardware factors. As demonstrated in this thesis, such dynamic imbalance can be found even in applications whose codes do not hint at any dynamism. Therefore, we need to rely on runtime dynamic load balancing mechanisms, such as dynamic load balancing based on over-decomposition. The problem is that evaluating and tuning the performance of such technique can be costly. This usually entails modifications to the application and a large number of executions to get statistically sound performance measurements with different load balancing parameter combinations. Moreover, useful and accurate measurements often require big resource allocations on a production cluster. Our simulation workflow, dubbed Simulated Adaptive MPI (SAMPI), employs a combined sequential emulation and trace-replay simulation approach to reduce the cost of such an evaluation Both sequential emulation and trace-replay require a single computer node. Additionally, the trace-replay simulation lasts a small fraction of the real-life parallel execution time of the application. Besides the basic SAMPI simulation, we developed spatial aggregation and applicationlevel rescaling techniques to speed-up the emulation process. To demonstrate the real-life performance benefits of dynamic load balance with over-decomposition, we evaluated the performance gains obtained by employing this technique on a iterative parallel geophysics application, called Ondes3D. Dynamic load balancing support was provided by Adaptive MPI (AMPI). This resulted in up to 36.58% performance improvement, on 288 cores of a cluster. This real-life evaluation also illustrates the difficulties found in this process, thus justifying the use of simulation. To implement the SAMPI workflow, we relied on SimGrid’s Simulated MPI (SMPI) interface in both emulation and trace-replay modes.To validate our simulator, we compared simulated (SAMPI) and real-life (AMPI) executions of Ondes3D. The simulations presented a load balance evolution very similar to real-life and were also successful in choosing the best load balancing heuristic for each scenario. Besides the validation, we demonstrate the use of SAMPI for load balancing parameter exploration and for computational capacity planning. As for the performance of the simulation itself, we roughly estimate that our full workflow can simulate the execution of Ondes3D with 24 different load balancing parameter combinations in 5 hours for our heavier earthquake scenario and in 3 hours for the lighter one.

Nesta tese é apresentado um novo workflow de simulação para avaliar o desempenho do balanceamento de carga dinâmico baseado em sobre-decomposição aplicado a aplicações paralelas iterativas. Seus objetivos são realizar essa avaliação com modificações mínimas da aplicação e a baixo custo em termos de tempo e de sua necessidade de recursos computacionais. Muitas aplicações paralelas sofrem com desbalanceamento de carga dinâmico (temporal) que não pode ser tratado a nível de aplicação. Este pode ser causado por características intrínsecas da aplicação ou por fatores externos de hardware ou software. Como demonstrado nesta tese, tal desbalanceamento é encontrado mesmo em aplicações cujo código não aparenta qualquer dinamismo. Portanto, faz-se necessário utilizar mecanismo de balanceamento de carga dinâmico a nível de runtime. Este trabalho foca no balanceamento de carga dinâmico baseado em sobre-decomposição. No entanto, avaliar e ajustar o desempenho de tal técnica pode ser custoso. Isso geralmente requer modificações na aplicação e uma grande quantidade de execuções para obter resultados estatisticamente significativos com diferentes combinações de parâmetros de balanceamento de carga Além disso, para que essas medidas sejam úteis, são usualmente necessárias grandes alocações de recursos em um sistema de produção. Simulated Adaptive MPI (SAMPI), nosso workflow de simulação, emprega uma combinação de emulação sequencial e replay de rastros para reduzir os custos dessa avaliação. Tanto emulação sequencial como replay de rastros requerem um único nó computacional. Além disso, o replay demora apenas uma pequena fração do tempo de uma execução paralela real da aplicação. Adicionalmente à simulação de balanceamento de carga, foram desenvolvidas técnicas de agregação espacial e rescaling a nível de aplicação, as quais aceleram o processo de emulação. Para demonstrar os potenciais benefícios do balanceamento de carga dinâmico com sobre-decomposição, foram avaliados os ganhos de desempenho empregando essa técnica a uma aplicação iterativa paralela da área de geofísica (Ondes3D). Adaptive MPI (AMPI) foi utilizado para prover o suporte a balanceamento de carga dinâmico, resultando em ganhos de desempenho de até 36.58% em 288 cores de um cluster Essa avaliação também é usada pra ilustrar as dificuldades encontradas nesse processo, assim justificando o uso de simulação para facilitá-la. Para implementar o workflow SAMPI, foi utilizada a interface SMPI do simulador SimGrid, tanto no modo de emulação, como no de replay de rastros. Para validar esse simulador, foram comparadas execuções simuladas (SAMPI) e reais (AMPI) da aplicação Ondes3D. As simulações apresentaram uma evolução do balanceamento de carga bastante similar às execuções reais. Adicionalmente, SAMPI estimou com sucesso a melhor heurística de balanceamento de carga para os cenários testados. Além dessa validação, nesta tese é demonstrado o uso de SAMPI para exploração de parâmetros de balanceamento de carga e para planejamento de capacidade computacional. Quanto ao desempenho da simulação, estimamos que o workflow completo é capaz de simular a execução do Ondes3D com 24 combinações de parâmetros de balanceamento de carga em 5 horas para o nosso cenário de terremoto mais pesado e 3 horas para o mais leve. / In this thesis we present a novel simulation workflow to evaluate the performance of dynamic load balancing with over-decomposition applied to iterative parallel applications at low-cost. Its goals are to perform such evaluation with minimal application modification and at a low cost in terms of time and of resource requirements. Many parallel applications suffer from dynamic (temporal) load imbalance that can not be treated at the application level. It may be caused by intrinsic characteristics of the application or by external software and hardware factors. As demonstrated in this thesis, such dynamic imbalance can be found even in applications whose codes do not hint at any dynamism. Therefore, we need to rely on runtime dynamic load balancing mechanisms, such as dynamic load balancing based on over-decomposition. The problem is that evaluating and tuning the performance of such technique can be costly. This usually entails modifications to the application and a large number of executions to get statistically sound performance measurements with different load balancing parameter combinations. Moreover, useful and accurate measurements often require big resource allocations on a production cluster. Our simulation workflow, dubbed Simulated Adaptive MPI (SAMPI), employs a combined sequential emulation and trace-replay simulation approach to reduce the cost of such an evaluation Both sequential emulation and trace-replay require a single computer node. Additionally, the trace-replay simulation lasts a small fraction of the real-life parallel execution time of the application. Besides the basic SAMPI simulation, we developed spatial aggregation and applicationlevel rescaling techniques to speed-up the emulation process. To demonstrate the real-life performance benefits of dynamic load balance with over-decomposition, we evaluated the performance gains obtained by employing this technique on a iterative parallel geophysics application, called Ondes3D. Dynamic load balancing support was provided by Adaptive MPI (AMPI). This resulted in up to 36.58% performance improvement, on 288 cores of a cluster. This real-life evaluation also illustrates the difficulties found in this process, thus justifying the use of simulation. To implement the SAMPI workflow, we relied on SimGrid’s Simulated MPI (SMPI) interface in both emulation and trace-replay modes.To validate our simulator, we compared simulated (SAMPI) and real-life (AMPI) executions of Ondes3D. The simulations presented a load balance evolution very similar to real-life and were also successful in choosing the best load balancing heuristic for each scenario. Besides the validation, we demonstrate the use of SAMPI for load balancing parameter exploration and for computational capacity planning. As for the performance of the simulation itself, we roughly estimate that our full workflow can simulate the execution of Ondes3D with 24 different load balancing parameter combinations in 5 hours for our heavier earthquake scenario and in 3 hours for the lighter one.

Submitted by Fabricia Fialho Reginato (fabriciar) on 2015-07-08T01:19:32Z No. of bitstreams: 1 VladimirGuerreiro.pdf: 5547701 bytes, checksum: b807e1f8091b49a5ee1e0b36e2ae4286 (MD5) / Made available in DSpace on 2015-07-08T01:19:32Z (GMT). No. of bitstreams: 1 VladimirGuerreiro.pdf: 5547701 bytes, checksum: b807e1f8091b49a5ee1e0b36e2ae4286 (MD5) Previous issue date: 2014 / Nenhuma / Em ambientes paralelos, uma das alternativas para tratar o dinamismo, tanto em nível de infraestrutura quanto de aplicação é o uso de migração, principalmente em aplicações que executam em fases utilizando BSP (Bulk Synchronous Parallel). Neste contexto, o modelo de reescalonamento MigBSP foi desenvolvido para tratar da realocação de processos em aplica- ções paralelas. Assim como o modelo BSP, ele considera as três fases de execução de uma superetapa: (i) computação local, (ii) comunicação global e (iii) uma barreira de sincroniza- ção; coletando dados localmente durante a computação para efetuar o cálculo do Potencial de Migração (PM) do processo. Com o PM e parâmetros adicionais fornecidos no inicio da execução da aplicação, o MigBSP tem condições de escolher processos candidatos a migração em uma aplicação paralela executando em um ambiente distribuído. Entretanto, as duas heurísticas possíveis de serem utilizadas hoje, dependem de informações fornecidas pelo usuário e/ou podem não selecionar uma quantidade eficiente de processos no momento do reescalonamento, podendo ser necessário várias chamadas para balancear o ambiente. Desta forma, esta disserta- ção apresenta duas novas heurísticas, MigCube e MigHull. Elas utilizam o MigBSP e efetuam a seleção automática de processos candidatos à migração sem a interferência do programador. As informações fornecidas pelo MigBSP são utilizadas nas heurísticas, a combinação das três métricas mensurados, posicionadas em um plano tridimensional, define cada processo como um ponto no espaço que possui as coordenadas x, y e z, onde cada eixo representa uma mé- trica para tomada de decisão. A heurística MigCube monta um cubo a partir das médias das distâncias entre os pontos, utilizando o processo com o maior PM como centro do cubo. A heurística MigHull segue a definição da Envoltória Convexa, tentando envolver todos os pontos, porém utilizando duas adaptações que se fazem necessárias para a aplicação neste trabalho. O MigBSP foi desenvolvido no simulador SimGrid, e este segue sendo utilizado para a criação das duas heurísticas apresentadas nesta dissertação. Nos testes realizados neste simulador, foi possível verificar um ganho de até 45% no tempo de execução da aplicação utilizando a heurística MigHull, e até 42% utilizando a MigCube, quando comparado a aplicação sem o modelo de migração. Porém, em simulações com um maior número de processos, este ganho tende a cair, já que um dos maiores problemas do BSP e aplicações que executam em grades é o tempo de sincronização de tarefas, ou seja, quanto mais processos, maior a necessidade de sincronização, e mesmo o balanceamento dos processos acaba tendo um resultado prejudicado. / In a parallel environment, one of the alternatives to address the dynamism, both at the infrastructure and application levels, is the use of migration, mostly with applications that execute in steps using BSP (Bulk Synchronous Parallel). In this context, the rescheduling model MigBSP was developed to deal with processes reallocation in parallel applications. As BSP model, MigBSP uses the three steps of a superstep: (i) computation, (ii) communication and (iii) a synchronization barrier; collecting local data during the computation step, to compute the processes’ Potential of Migration (PM). With the PM and additional parameters provided in the beginning of the application’s execution, MigBSP have conditions to choose the processes candidate to migrate in a parallel application running in a distributed system. However, the two heuristics possible to be used today depend of information provided by the user and/or may not select the proper quantity of processes in the rescheduling moment, being necessary many executions to balance the environment. This way, this dissertation present two new heuristics, MigCube and MigHull. They make use of MigBSP, and automatically will choose the processes to migrate without user interference. The information provided by MigBSP are used in the heuristics, the combination of the three measured metrics, positioned in a three-dimensional space, defines each process as a point in space and has the coordinates x, y e z, where each axis represents a metric for decision making. The MigCube heuristic build a cube from the average of the distances between points, using the process with the highest PM as the center of the cube. The MigHull follows the definition of a Convex Hull, trying to involve all points, but using two adaptations that are necessary to implement this work. The MigBSP was developed using SimGrid simulator, and it keeps being used to creation of the two heuristics presented in this dissertation. In the conducted tests in this simulator, was possible to achieve a gain of until 45% on application execution time using MigHull, and until 42% using MigCube, when compared with the application without the migration model. However, simulations with a bigger number of processes, this gain tends to fall, since one of the bigger problems of BSP and applications that run in grid is the time of tasks synchronization, that is, as more processes, more need of synchronization, and even the processes balancing ends up having an impaired outcome.