Verification of Data Races in Concurrent Interrupt Handlers
Data races are common in interrupt-driven programs and have already led to well-known real-world problems. Unfortunately, existing dynamic tools for reporting data races in interrupt-driven programs are not only unsound, but they also fail to verify the existence of data races in such programs. This...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-11-01
|
| Series: | International Journal of Distributed Sensor Networks |
| Online Access: | https://doi.org/10.1155/2013/953593 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850211058594086912 |
|---|---|
| author | Guy Martin Tchamgoue Kyong Hoon Kim Yong-Kee Jun |
| author_facet | Guy Martin Tchamgoue Kyong Hoon Kim Yong-Kee Jun |
| author_sort | Guy Martin Tchamgoue |
| collection | DOAJ |
| description | Data races are common in interrupt-driven programs and have already led to well-known real-world problems. Unfortunately, existing dynamic tools for reporting data races in interrupt-driven programs are not only unsound, but they also fail to verify the existence of data races in such programs. This paper presents an efficient and scalable on-the-fly technique that precisely detects, without false positives, apparent data races in interrupt-driven programs. The technique combines a tailored lightweight labeling scheme to maintain logical concurrency between the main program and every instance of its interrupt handlers with a precise detection protocol that analyzes conflicting shared memory accesses by storing at most two accesses for each shared variable. We implemented a prototype of this technique, called i Race, on top of the Avrora simulation framework. An empirical evaluation of i Race revealed the presence of data races in some existing TinyOS components and applications with a worst-case slowdown of only about 6 times on average and an increased average memory consumption of only about 20% in comparison with the original program execution. The evaluation also proved that the labeling scheme alone generates an average runtime overhead of only about 0.4x while consuming only about 12% more memory than the original program execution. |
| format | Article |
| id | doaj-art-894b165884e646e78b074e09ab900713 |
| institution | OA Journals |
| issn | 1550-1477 |
| language | English |
| publishDate | 2013-11-01 |
| publisher | Wiley |
| record_format | Article |
| series | International Journal of Distributed Sensor Networks |
| spelling | doaj-art-894b165884e646e78b074e09ab9007132025-08-20T02:09:38ZengWileyInternational Journal of Distributed Sensor Networks1550-14772013-11-01910.1155/2013/953593Verification of Data Races in Concurrent Interrupt HandlersGuy Martin TchamgoueKyong Hoon KimYong-Kee JunData races are common in interrupt-driven programs and have already led to well-known real-world problems. Unfortunately, existing dynamic tools for reporting data races in interrupt-driven programs are not only unsound, but they also fail to verify the existence of data races in such programs. This paper presents an efficient and scalable on-the-fly technique that precisely detects, without false positives, apparent data races in interrupt-driven programs. The technique combines a tailored lightweight labeling scheme to maintain logical concurrency between the main program and every instance of its interrupt handlers with a precise detection protocol that analyzes conflicting shared memory accesses by storing at most two accesses for each shared variable. We implemented a prototype of this technique, called i Race, on top of the Avrora simulation framework. An empirical evaluation of i Race revealed the presence of data races in some existing TinyOS components and applications with a worst-case slowdown of only about 6 times on average and an increased average memory consumption of only about 20% in comparison with the original program execution. The evaluation also proved that the labeling scheme alone generates an average runtime overhead of only about 0.4x while consuming only about 12% more memory than the original program execution.https://doi.org/10.1155/2013/953593 |
| spellingShingle | Guy Martin Tchamgoue Kyong Hoon Kim Yong-Kee Jun Verification of Data Races in Concurrent Interrupt Handlers International Journal of Distributed Sensor Networks |
| title | Verification of Data Races in Concurrent Interrupt Handlers |
| title_full | Verification of Data Races in Concurrent Interrupt Handlers |
| title_fullStr | Verification of Data Races in Concurrent Interrupt Handlers |
| title_full_unstemmed | Verification of Data Races in Concurrent Interrupt Handlers |
| title_short | Verification of Data Races in Concurrent Interrupt Handlers |
| title_sort | verification of data races in concurrent interrupt handlers |
| url | https://doi.org/10.1155/2013/953593 |
| work_keys_str_mv | AT guymartintchamgoue verificationofdataracesinconcurrentinterrupthandlers AT kyonghoonkim verificationofdataracesinconcurrentinterrupthandlers AT yongkeejun verificationofdataracesinconcurrentinterrupthandlers |