Continuous technological improvement is the hallmark of the hardware industry. In an ideal world--one without budgets or schedules--software would be redesigned and redeveloped from scratch to leverage each such improvement. But applying this process for software is often infeasible--if not impossible--due to economic constraints and competition. This posting discusses our research in applying verification, namely regression verification, to help the migration of real-time embedded systems from single-core to multi-core platforms.

A key recent technological hardware improvement is the advent of larger multi-core architectures. In theory, software written for single-core hardware should be reused as-is on multi-core hardware. After all, software that has been validated extensively on single-core hardware--and is not being modified--should behave unchanged on multi-core hardware. In practice, however, this migration isn't so easy due to many factors that influence software behavior, including the architectural assumptions made by the underlying hardware. Multi-threaded programs are particularly problematic since key assumptions (such as one-at-a-time thread execution) made when these programs were developed for a single core are often invalidated by the true parallelism of multi-core hardware.

Reusing software written for single-core hardware can be dangerous without first verifying that it works correctly on multi-core hardware. At the SEI we've seen many instances where software ported from single- to multi-core hardware is less robust than its single-core counterpart. Addressing this problem is increasingly essential for the Department of Defense (DoD). The DoD is one of the largest users of software--especially mission- and safety-critical real-time embedded software where the consequences of defects can be deadly and the right answer delivered too late becomes the wrong answer.

Formal verification techniques ensure that a program will work. These techniques use mathematical models of programs to prove (or disprove) that the software will function correctly under certain conditions. Although verification provides strong guarantees of correctness, the verification process itself is expensive and time-consuming, in part due to a lack of scalable automated tools and the need for formal specifications.

Over the next year, my colleagues and I plan to study an application of a particular formal verification technique known as regression verification by applying it to the problem of migrating real-time embedded software from single- to multi-core hardware. Regression verification involves deciding the behavioral equivalence of two, closely related programs, e.g., Pold and Pnew. This technique is potentially simpler in practice than applying functional verification to Pnew against a user-defined, high-level specification since it circumvents the complex and error-prone problem of creating specifications. Moreover, this technique is also potentially more scalable since the computational effort will ideally be proportional to the difference between Pnew and Pold, rather than the size of Pold, as is the case with conventional testing and functional verification techniques.

Joining me on this project will be Sagar Chaki and Dionisio de Niz, senior members of the technical staff in the SEI Research, Technology, and System Solutions (RTSS) program, together with Ofer Strichman, a visiting scientist in RTSS and the co-inventor of regression verification. Based on our work thus far, regression verification appears particularly relevant when migrating from single-core to multi-core hardware in safety-critical domains, such as real-time embedded systems, where validation is necessary (and costly using conventional verification techniques). Moreover, real-time embedded systems are often highly restricted (e.g., they use limited programmatic features and specific task scheduling disciplines) and these restrictions can be leveraged to improve the tractability of regression verification.

Our goal over the next year is to explore the application of regression verification to software migration across hardware platforms. We will work with Professor Strichman to develop regression verification algorithms for multi-core hardware migration. We will also develop and test a formal definition of regression verification for migration of real-time embedded systems from single-core to multi-core hardware.

Addressing the single-core to multi-core migration problem is crucial for DoD and industry. One of the biggest challenges that both face is migrating complex cyber software infrastructure to leverage the latest hardware capabilities, such as multi-core. I will blog about the progress of our research throughout the course of the year.