Scalable trace analysis of distributed systems: finding data races

Abstract

Distributed Systems and Protocols are widely employed in the infrastructure that supports the Internet and the services available online such as streaming services and social networks. At the same time, they are well known for usually being hard to implement correctly, even when this task is left to experienced programmers. Consequently, Distributed Systems are prone to suffer from distributed concurrency bugs, which are a frequent source of significant service outages. Thus, it is of the utmost importance to ensure that widely-used distributed systems are reliable and do not suffer from this kind of bugs. Formal Verification looks like a promising way to achieve this. However, we argue that the currently available techniques require too much of an investment in order to verify correctness of implementations of complex distributed systems. Instead, we defend the usage of clever testing techniques and tools for all but the most critical of contexts. In this dissertation, we present one such tool – Spider – designed to automatically detect data races from traced executions of distributed systems. Data races originate when two memory accesses to the same memory location occur concurrently and they have been shown to be a major source of concurrency bugs in distributed systems. Unfortunately, data races are often triggered by non-deterministic event orderings that are hard to detect when testing complex distributed systems. Spider encodes the causal relations between the events in the trace as a symbolic constraint model, which is then fed into an SMT solver to check for the presence of conflicting concurrent accesses. To reduce the constraint solving time, Spider employs a pruning technique aimed at removing redundant portions of the trace. Our experiments with multiple benchmarks show that Spider is effective in detecting data races in distributed executions in a practical amount of time, providing evidence of its usefulness as a testing tool.

Os sistemas e protocolos distribuídos são amplamente utilizados na infraestrutura que suporta a Internet e os serviços disponíveis online tais como, por exemplo, serviços de streaming e redes sociais. Ao mesmo tempo, os sistemas distribuídos são reconhecidamente difíceis de implementar corretamente e tendem a sofrer de bugs de concorrência distribuída, mesmo quando são desenvolvidos por programadores experientes. Este tipo de bugs é uma causa frequentemente de falhas nos serviços e, por esta razão, é da maior importância garantir que os sistemas distribuídos amplamente utilizados são confiáveis e não sofrem deste tipo de erros. A área de verificação formal fornece ferramentas poderosas que permitem evitar que estes bugs cheguem a código de produção. No entanto, consideramos que as técnicas do estado da arte disponíveis atualmente exigem grandes investimentos caso se pretenda verificar que uma implementação de um sistema distribuído está correta. Em vez disso, defendemos o uso de técnicas e ferramentas sofisticadas de teste para assegurar a confiabilidade das implementações de sistemas distribuídos excepto nos contextos mais críticos, onde se devem empregar técnicas de verificação formal. Nesta dissertação, apresentamos a Spider, uma ferramenta de teste e debug de sistemas distribuídos desenvolvida para detectar automaticamente data races a partir de traces obtidos aquando da execução de sistemas distribuídos. As data races surgem quando dois acessos ao mesmo endereço de memoria ocorrem concorrentemente. A existência de data races é uma das principais causas de erros de concorrência em sistemas distribuídos. Ao mesmo tempo, são extremamente difíceis de detetar uma vez que se manifestam raramente e de forma não determinística. A ferramenta Spider codifica as relações causais entre os eventos no trace como um modelo de restrições, e, através de um SMT solver, e capaz de inferir que pares de instruções podem levar a acessos concorrentes ao mesmo endereço de memória. Para reduzir o tempo da análise, o Spider emprega uma técnica de eliminação de eventos que remove partes redundantes do trace. Com recurso a vários benchmarks, mostramos experimentalmente que o Spider é eficaz a detetar data races a partir de traces de sistemas distribuídos e que tal é exequível em tempo útil, indiciando que a Spider é útil como ferramenta de teste.