Concurrency Debugging with MaxSMT
Authors: Miguel Terra-Neves, Nuno Machado, Ines Lynce, Vasco Manquinho1608-1616
AAAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show that using Max SMT can significantly improve the accuracy of the generated reports and, consequently, their usefulness in debugging the root cause of concurrency bugs. |
| Researcher Affiliation | Collaboration | 1INESC-ID / Instituto Superior T ecnico, Universidade de Lisboa, Portugal 2Teradata Spain and HASLab INESC TEC / Universidade do Minho, Portugal |
| Pseudocode | Yes | Algorithm 1: Progressive algorithm for computing an alternate schedule. |
| Open Source Code | Yes | The Max SMT models and algorithms were integrated in the publicly available versions of SYMBIOSIS3 and CORTEX4 tools. 3http://github.com/nunomachado/symbiosis 4http://github.com/nunomachado/cortex-tool |
| Open Datasets | Yes | We consider two sets of test cases. The first includes several C/C++ and Java applications with strictly schedule-dependent bugs, such as shared buffer implementation or an adapted parallel file scanner (Elmas et al. 2013). The second set includes programs with path-schedule dependent bugs from the IBM Con Test benchmark suite, as well as the Ex MCR benchmark. |
| Dataset Splits | No | The paper mentions using "test cases" and "benchmarks" for evaluation but does not specify any training/validation/test dataset splits or cross-validation setup. |
| Hardware Specification | No | The paper does not provide specific details about the hardware used for the experiments, such as GPU/CPU models, memory, or specific cluster configurations. |
| Software Dependencies | Yes | In our experiments, Z3 (Bjørner and Phan 2014) (version 4.6.0) was used as the Max SMT solver. |
| Experiment Setup | Yes | For the inc (incomplete) sub-column, a conflict threshold of 200000 was used. A time limit of 3 hours was imposed for each execution on a particular test case. We consider two types of Max SMT models: one where all criteria are equally significant (i.e., φs = φdf s φbs s φcs s ) and one lexicographic model that optimizes φdf s first, followed by φbs s and then φcs s . |