Formal verification is approaching a point where it will be reliably applicable to
embedded software. Even though formal verification can efficiently analyze multi-threaded
applications, multi-core processors are often considered too dangerous to use in critical
systems, despite the many benefits they can offer. One reason is the advanced memory
consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential
consistency, which is also the naïve view of programmers. Modern multi-core processors,
however, rarely guarantee this assumption by default. In addition, complex processor
architectures may easily contain design faults. Thanks to the recent advances in hardware
verification, these faults are increasingly visible and can be detected even in existing
processors, giving an opportunity to compensate for the problem in software. In this
paper, we propose a generic approach to consider inconsistent behavior of the hardware
in the analysis of software. Our approach is based on formal methods and can be used
to detect the activation of existing hardware faults on the application level and
facilitate their mitigation in software. The approach relies heavily on recent results
of model checking and hardware verification and offers new, integrative research directions.
We propose a partial solution based on existing model checking tools to demonstrate
feasibility and evaluate their performance in this context.
