Static detection of error of double locking of mutex
This paper describes algorithm for static search for error of double locking of mutex. The algorithm allows emitting warnings with low level of false positives. We considered finding errors for abstract library containing functions of mutex lock, unlock and conditional locking. We defined a set of r...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/806 |
| _version_ | 1818393481184280576 |
|---|---|
| author | Alexey Borodin |
| author_facet | Alexey Borodin |
| author_sort | Alexey Borodin |
| collection | DOAJ |
| description | This paper describes algorithm for static search for error of double locking of mutex. The algorithm allows emitting warnings with low level of false positives. We considered finding errors for abstract library containing functions of mutex lock, unlock and conditional locking. We defined a set of regular languages, which models locks and unlocks during concrete execution of a program. We have defined a domain approximated set of regular languages. The algorithm is implemented in terms of data flow analysis. In the analysis elements of the domain are used as the data flow properties. The algorithm is described for a program that has only one mutex and does not contain any aliases. In that case every emitted warning will correspond to a real error which may occur during program execution. The algorithm is implemented in system of static analysis Svace developed in Institute for System Programming of the Russian Academy of Sciences. Svace performs alias analysis and matching of formal and actual function parameters. This makes it possible to apply the algorithm to search for double locking of a program containing only one mutex, and the rest of the work will be executed by Svace. The search algorithm of the double lock implemented in Svace can emit some number of false positives because Svace performs nonconservative analysis. |
| first_indexed | 2024-12-14T05:46:00Z |
| format | Article |
| id | doaj.art-a2af42063cc74440aaa123ab6debab78 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-14T05:46:00Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-a2af42063cc74440aaa123ab6debab782022-12-21T23:14:52ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0126310311210.15514/ISPRAS-2014-26(3)-5806Static detection of error of double locking of mutexAlexey Borodin0ИСП РАНThis paper describes algorithm for static search for error of double locking of mutex. The algorithm allows emitting warnings with low level of false positives. We considered finding errors for abstract library containing functions of mutex lock, unlock and conditional locking. We defined a set of regular languages, which models locks and unlocks during concrete execution of a program. We have defined a domain approximated set of regular languages. The algorithm is implemented in terms of data flow analysis. In the analysis elements of the domain are used as the data flow properties. The algorithm is described for a program that has only one mutex and does not contain any aliases. In that case every emitted warning will correspond to a real error which may occur during program execution. The algorithm is implemented in system of static analysis Svace developed in Institute for System Programming of the Russian Academy of Sciences. Svace performs alias analysis and matching of formal and actual function parameters. This makes it possible to apply the algorithm to search for double locking of a program containing only one mutex, and the rest of the work will be executed by Svace. The search algorithm of the double lock implemented in Svace can emit some number of false positives because Svace performs nonconservative analysis.https://ispranproceedings.elpub.ru/jour/article/view/806статический анализсемафорошибка повтороной блокировкианализ потока данныхрегулярные языки |
| spellingShingle | Alexey Borodin Static detection of error of double locking of mutex Труды Института системного программирования РАН статический анализ семафор ошибка повтороной блокировки анализ потока данных регулярные языки |
| title | Static detection of error of double locking of mutex |
| title_full | Static detection of error of double locking of mutex |
| title_fullStr | Static detection of error of double locking of mutex |
| title_full_unstemmed | Static detection of error of double locking of mutex |
| title_short | Static detection of error of double locking of mutex |
| title_sort | static detection of error of double locking of mutex |
| topic | статический анализ семафор ошибка повтороной блокировки анализ потока данных регулярные языки |
| url | https://ispranproceedings.elpub.ru/jour/article/view/806 |
| work_keys_str_mv | AT alexeyborodin staticdetectionoferrorofdoublelockingofmutex |