Will My Program Break on This Faulty Processor?
| Autor: | Vince Molnár, Levente Bajczi, András Vörös |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
010302 applied physics
Model checking business.industry Computer science Sequential consistency Consistency model 020207 software engineering Context (language use) 02 engineering and technology Formal methods 01 natural sciences Embedded software Software Hardware and Architecture 0103 physical sciences 0202 electrical engineering electronic engineering information engineering business Formal verification Computer hardware |
| Zdroj: | ACM Transactions on Embedded Computing Systems. 18:1-21 |
| ISSN: | 1558-3465 1539-9087 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|