Verification of Data Races in Concurrent Interrupt Handlers. (21st November 2013)

• Record Type: Journal Article
• Authors: Tchamgoue, Guy Martin; Kim, Kyong Hoon; Jun, Yong-Kee
• Is Part Of: International journal of distributed sensor networks. Volume 9:Number 11(2013)
• Publication Date: 2013-11-21
• Subjects: Sensor networks -- Periodicals; Intelligent agents (Computer software) -- Periodicals; Multisensor data fusion -- Periodicals; 681.2
• DOI: 10.1155/2013/953593
• Languages: English
• ISSNs: 1550-1329

Abstract

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.