Critical real-time systems are getting more and more complex and require ever more computing power. Multi-core platforms, GPUs, and custom accelerators promise to deliver this needed performance. However, these platforms are notoriously hard to analyze and lack predictability in terms of timing properties. Computer architectures and platforms that offer both predictability and performance are thus needed. This work investigates the use of the interactive proof assistant Coq in order to model complex DRAM memory controllers (MCs) for multi-core platforms. The design of predictable high-performance MCs is particularly challenging, since memory requests have to be processed efficiently, while facing interference from other cores in the system. The problem is exacerbated by the complexity of DRAM devices and the various timing constraints they impose. Specifically, this work extends a previous Coq framework by focusing on reusability, which allows designers to develop and prove complex MCs. As a use-case, we present TDMShelve, an MC balancing performance and isolation.

Abstract In order to prove conformance to memory standards and bound memory access latency, recently proposed real-time DRAM controllers rely on paper and pencil proofs, which can be troubling: they are difficult to read and review, they are often shown only partially and/or rely on abstractions for the sake of conciseness, and they can easily diverge from the controller implementation, as no formal link is established between both. We propose a new framework written in Coq, in which we model a DRAM controller and its expected behaviour as a formal specification. The trustworthiness in our solution is two-fold: (1) proofs that are typically done on paper and pencil are now done in Coq and thus certified by its kernel, and (2) the reviewer’s job develops into making sure that the formal specification matches the standards—instead of performing a thorough check of the mathematical formalism. Our framework provides a generic DRAM model capturing a set of controller properties as proof obligations, which all implementations must comply with. We focus on properties related to the assertiveness that timing constraints are respected, every incoming request is handled in bounded time, and the DRAM command protocol is respected. We refine our specification with two implementations based on widely-known arbitration policies—First-in First-Out (FIFO) and Time-Division Multiplexing (TDM). We extract proved code from our model and use it as a “trusted core” on a cycle-accurate DRAM simulator.

This paper introduces a formal workflow for modeling software/hardware systems in order to explore the effects of fault injections and evaluate the robustness to fault injection attacks. We illustrate this workflow on four versions of a PIN authentication code, embedding different software countermeasures. The code is symbolically evaluated on two implementations of the RISC-V CV32E40P core: the original implementation from the OpenHW group and an implementation that integrates protection of the pipeline control signals. On the original, unprotected core, our formal workflow exposes various vulnerabilities, including previously unknown ones, whereas, on the protected core, it confirms the effectiveness of the proposed countermeasures.

Safety-critical applications require well-defined and documented timing behavior. These requirements shape the design and implementation of a timing analyzer based on a formal Instruction-Set Architecture (ISA) semantics and formal micro-architecture models. In this paper we present the key elements of such a timing analyzer and how to systematically combine the formal components to address timing properties such as evaluating memory interferences. We also report preliminary experiments of memory interference analysis of multi-threaded applications in a multicore context.

Static worst-case timing analysis is important in the context of safety-critical systems as it is one approach that could be used to validate the required timing bounds. In order to derive accurate bounds, the worst-case timing analysis is performed under (micro)-architecture consideration, consequently, these bounds are expressed in processor cycles. The required (micro)-architecture models are usually constructed by hand, from processor manuals and validated through testing. Recent advances in hardware design promote open hardware initiatives and high-level Hardware Description Languages (HDLs), revisiting the perspectives to automatically construct (micro)-architecture models for worst-case timing analysis. In this paper, we present an approach concerning the construction of pipeline datapath models from processor designs described in high-level HDLs. We propose a methodology based on the Chisel/FIRRTL Hardware Compiler Framework which we apply on several open-source RISC-V processors.

Safety-critical systems rely on worst-case timing analysis under architecture considerations to ensure that their timing bounds could be guaranteed. Usually, such architecture models are constructed by hand, from processor manuals. However, with open hardware initiatives and high-level Hardware Description Languages (HDL), automation would and should be possible. In this paper, we present an approach for constructing pipeline datapath models from processor designs described in high-level HDLs. We propose a methodology based on the Chisel/FIRRTL Hardware Compiler Framework and we report preliminary results on several open-source RISC-V processors.

Intuitively, a counter-intuitive timing anomaly manifests when a locally faster execution becomes globally slower. While the presence of such timing anomalies threatens the soundness and/or scalability of timing analyses, tools to systematically detect them do not exist. The main reason lies in the absence of a definition of counter-intuitive timing anomalies that establishes relations between local and global timing effects. In this paper, we address these relations through an important concept, that of causality, which we further use to revise the formalization of counter-intuitive timing anomalies. We also propose a specialized instance of the notions to implement a detection procedure for out-of-order pipelines.

Correctness is an important concern during the development of real-time systems. In addition to the functional correctness, the timing behavior is often formally verified in order to ensure that correct results are delivered in-time for all possible execution conditions. The timing behavior of real-time software is thus often validated through a rigorous timing analysis that aims at determining the worst-case execution time.Timing anomalies present a major obstacle during the validation of timing properties on modern computer platforms. Out-of-order execution and concurrent accesses to shared resources may sometimes lead to – at first sight – surprising timing behavior. Several (semi-)formal definitions have been proposed in the literature in order to capture such situations. However, as we present in this work, none of the existing definitions appears to be precise enough to be systematically used for detecting timing anomalies in modern processors with out-of-order execution.

Computer architectures used in safety-critical domains are subjected to worst-case execution time analysis. The presence of performance-driven microarchitectures may trigger undesired timing phenomena, called timing anomalies, and complicate the timing analysis. This paper investigates pipelines specifically designed to simplify the worst-case execution time analysis (also called predictable pipelines). We propose formal and executable models of four research-oriented pipelines and one industrial pipeline to validate some of their claims related to their timing behavior. We indeed validate, via bounded model checking, the absence of a type of timing anomalies called amplification timing anomalies, or its potential presence by identifying prerequisite to situations where they can occur.