Predicate Abstraction Based Configurable Method for Data Race Detection in Linux Kernel
| Autor: | Alexey Khoroshilov, Vadim Mutilin, Pavel Andrianov |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Computer science
Programming language 010102 general mathematics 020207 software engineering Linux kernel 02 engineering and technology Thread (computing) Static analysis computer.software_genre 01 natural sciences Predicate abstraction 0202 electrical engineering electronic engineering information engineering Memory model 0101 mathematics Static data computer Counterexample |
| Zdroj: | Communications in Computer and Information Science ISBN: 9783319717333 |
| DOI: | 10.1007/978-3-319-71734-0_2 |
| Popis: | The paper presents a configurable method for static data race detection. The method is based on a lightweight approach that implements Lockset algorithm with a simplified memory model. The paper contributes two heavyweight extensions which allow to adjust required precision of the analysis by choosing the balance between spent resources and a number of false alarms. The extensions are (1) counterexample guided refinement based on predicate abstraction and (2) thread analysis. The approach was implemented in the CPALockator tool and was applied to Linux kernel modules. Real races found by the tool have been approved and fixed by Linux kernel developers. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|