Skip to Main content Skip to Navigation

Performance and correctness assessmet of distributed systems

Abstract : Distributed systems are in the mainstream of information technology. It has become standard to rely on multiple distributed units to improve the performance of the application, help tolerate component failures, or handle problems too large to fit in a single processing unit. The design of algorithms adapted to the distributed context is particularly difficult due to the asynchrony and the nondeterminism that characterize distributed systems. Simulation offers the ability to study the performance of distributed applications without the complexity and cost of the real execution platforms. On the other hand, model checking allows to assess the correctness of such systems in a fully automatic manner. In this thesis, we explore the idea of integrating a model checker with a simulator for distributed systems in a single framework to gain performance and correctness assessment capabilities. To deal with the state explosion problem, we present a dynamic partial order reduction algorithm that performs the exploration based on a reduced set of networking primitives, that allows to verify programs written for any of the communication APIs offered by the simulator. This is only possible after the development of a full formal specification with the semantics of these networking primitives, that allows to reason about the independency of the communication actions as required by the DPOR algorithm. We show through experimental results that our approach is capable of dealing with non trivial unmodified C programs written for the SimGrid simulator. Moreover, we propose a solution to the problem of scalability for CPU bound simulations, envisioning the simulation of Peer-to-Peer applications with millions of participating nodes. Contrary to classical parallelization approaches, we propose parallelizing some internal steps of the simulation, while keeping the whole process sequential. We present a complexity analysis of the simulation algorithm, and we compare it to the classical sequential algorithm to obtain a criteria that describes in what situations a speed up can be expected. An important result is the observation of the relation between the precision of the models used to simulate the hardware resources, and the potential degree of parallelization attainable with this approach. We present several case studies that benefit from the parallel simulation, and we show the results of a simulation at unprecedented scale of the Chord Peer-to-Peer protocol with two millions nodes executed in a single machine
Document type :
Complete list of metadatas

Cited literature [68 references]  Display  Hide  Download
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:29:43 AM
Last modification on : Friday, October 23, 2020 - 5:02:10 PM
Long-term archiving on: : Thursday, September 13, 2018 - 12:25:30 PM


Files produced by the author(s)


  • HAL Id : tel-01746271, version 1


Cristian Rosa. Performance and correctness assessmet of distributed systems. Other [cs.OH]. Université Henri Poincaré - Nancy 1, 2011. English. ⟨NNT : 2011NAN10113⟩. ⟨tel-01746271⟩



Record views


Files downloads