Overview

Writing reliable software for sensor networks is particularly difficult because of the intrinsic nature of such software: distributed, timing-sensitive, event-driven, and closely coupled to hardware. In this project we are developing tools and techniques to analyze sensor network software in order to detect important classes of errors. Our goal is to eliminate these errors before they can manifest in a running system. At a high level our technical approach, which is detailed in the next section, is one of staged checking: a sequence of checks that rely on increasing scope and knowledge are performed on the code at compile, load, and run times. Our checkers target three principle classes of errors: violations of application conventions and programming interfaces, mismanagement of resources, and configuration and dependency problems. We are currently instantiating our checkers in the context of the SOS operating system for sensor nodes, and we plan to adapt the techniques we develop to the EmStar system in the future.

Approach

The goal of our approach is to detect errors as early as possible in the software development cycle. As such, staged checking is a natural fit, since it allows errors to be detected as soon as the relevant program information becomes available. We are focusing on a three-staged process. First, many interesting checks can be performed statically, when each individual software module is compiled. For example, each SOS module must be checked to handle the INIT and FINAL messages, which are sent by the kernel in order to respectively initialize and destroy a module. Second, SOS supports dynamic loading of modules, and several system errors can be detected at module load/unload time. For example, it is possible for a module to be removed even though another module is still subscribing to a function published by that module. Finally, run-time checking can be used to trap errors right before they would actually occur. For example, run-time monitoring can detect if two modules ever attempt to simultaneously obtain exclusive access to some device, throwing an exception or invoking a user-defined error handler to recover at that point.

Systems/Experiments

We are currently developing a static checker for SOS. The checker is implemented in the CIL tool, which parses C code into a simple intermediate format upon which analyses are performed. Each SOS module can be analyzed in isolation, and the checker produces a set of warnings about possibly erroneous situations. The analyses do not modify any code, so users can continue to compile their SOS modules with the C compiler of their choice. We are actively extending the static checker to support the variety of checks described in the previous section. We have also begun experimentation in two ways. First, the checker was deployed as part of the SOS build process for student projects in a graduate course in embedded systems. The logs from these builds provide us with information on the kinds of errors that novice SOS users make and the extent to which our checker detects these errors. Second, we have begun running the checker on the existing SOS code base to better understand the practical utility and limitations of our approach.

Accomplishments

Our static checker currently supports detection of two important classes of errors. First, it includes an arsenal of style checks to ensure that SOS conventions, like the presence of INIT and FINAL handlers, are obeyed. Second, SOS uses an ownership model of memory management, in which each chunk of dynamically allocated memory has a unique owner, who has unrestricted access to the memory but is also responsible for its eventual deallocation. This ownership model helps to ensure the absence of both dangling pointers and memory leaks. We have introduced new annotations that allow programmers to express their ownership intentions (e.g., to take or transfer ownership of some memory), and our static checker ensures that these annotations are properly respected. We have also begun formalizing SOS’s ownership model, in order to make precise the properties that it can ensure on system resources like memory.

Future Directions

We plan to continue gaining experience with our static checker on the SOS code base, in order to determine necessary improvements. For example, we may need to generalize our notion of memory ownership to allow controlled forms of shared ownership, in order to handle some programming idioms involving communication among multiple modules. We also plan to extend our checker to validate properties concerning the event-based nature of SOS modules. For example, given a finite-state machine that formalizes the legal orders in which events may be passed to each module, we can perform a combination of load-time and run-time checking to ensure that programs respect these specifications.

People

Faculty Researchers:

• Rupak Majumdar, Assistant Professor, UCLA Computer Science Department
• Todd Millstein, Assistant Professor, UCLA Computer Science Department
• Mani Srivastava, Professor, UCLA Electrical Engineering Department

Graduate Student Researchers:

• Shane Markstrum, Ph.D. student, UCLA Computer Science Department
• Roy Shea, Ph.D. student, UCLA Computer Science Department