Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/68770
Título: | Testing for race conditions in distributed systems via smt solving |
Autor(es): | Pereira, João Carlos Machado, Nuno Pinto, Jorge Sousa |
Data: | 2020 |
Editora: | Springer |
Revista: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Citação: | Pereira J.C., Machado N., Sousa Pinto J. (2020) Testing for Race Conditions in Distributed Systems via SMT Solving. In: Ahrendt W., Wehrheim H. (eds) Tests and Proofs. TAP 2020. Lecture Notes in Computer Science, vol 12165. Springer, Cham. https://doi.org/10.1007/978-3-030-50995-8_7 |
Resumo(s): | Data races, a condition where two memory accesses to the same memory location occur concurrently, 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. In this paper, we propose Spider, an automated tool for identifying data races in distributed system traces. 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/68770 |
ISBN: | 978-3-030-50994-1 |
e-ISBN: | 978-3-030-50995-8 |
DOI: | 10.1007/978-3-030-50995-8_7 |
ISSN: | 0302-9743 |
Versão da editora: | https://link.springer.com/chapter/10.1007%2F978-3-030-50995-8_7 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
P-00S-B2E.pdf | Accepted Manuscript | 764,43 kB | Adobe PDF | Ver/Abrir |