Interrupt Verification via Thread Verification

John Regehr Nathan Cooprider
regehr@cs.utah.edu coop@cs.utah.edu

University of Utah, School of Computing
50 South Central Campus Drive, Room 3190
Salt Lake City, Utah 84112-9205

In Electronic Notes in Theoretical Computer Science (ENTCS). 174(9):139-150, June 2007.

© 2007 Elsevier B.V. This is the author's version of the work. It is posted here by permission of Elsevier B.V. for your personal use. Not for redistribution.

Abstract

Most of the research effort towards verification of concurrent software has focused on multithreaded code. On the other hand, concurrency in low-end embedded systems is predominantly based on interrupts. Low-end embedded systems are ubiquitous in safety-critical applications such as those supporting transportation and medical automation; their verification is important. Although interrupts are superficially similar to threads, there are subtle semantic differences between the two abstractions. This paper compares and contrasts threads and interrupts from the point of view of verifying the absence of race conditions. We identify a small set of extensions that permit thread verification tools to also verify interrupt-driven software, and we present examples of source-to-source transformations that turn interrupt-driven code into semantically equivalent thread-based code that can be checked by a thread verifier. Finally, we demonstrate a proofof-concept program transformation tool that converts interrupt-driven sensor network applications into multithreaded code, and we use an existing tool to find race conditions in these applications.



Nathan Cooprider <coop@cs.utah.edu>