This paper proposes to model the Worst-Case Execution Time (WCET) of a GPU thread block as the Worst-Case Response Time (WCRT) of the warps composing the block. Inspired by the WCRT analyzes for classical CPU tasks, the response time of a warp is modeled as its execution time in isolation added to an interference term that accounts for the execution of higher priority warps. We provide an algorithm to build a representation of the execution of each warp of a thread block that distinguishes phases of execution on the functional units and phases of idleness due to operations latency. A simple formula relying on this model is then proposed to safely upper bound the WCRT of warps scheduled under greedy policies such as Greedy-Then-Oldest (GTO) or Loose Round-Robin (LRR). We experimented our approach using simulations of kernels from a GPU benchmark suite on the Accel-Sim simulator. We also evaluated the model on a GPU program that is likely to be found in safety critical systems : SGEMM (Single-precision GEneral Matrix Multiplication). This work constitutes a promising first building block of an analysis pipeline for enabling static WCET computation on GPUs.

The verification of a time-critical system requires precise analysis of execution times, which makes assumptions on the system's behavior, especially when it is poorly documented. One of those assumptions, when the system features a GPU accelerator, relates to the policy that each Streaming Multiprocessor (SM) follows to schedule warps. We argue that the literature overlooks the lack of synchronization between the instruction fetch and instruction issue schedulers, while this is likely to make the behavior of existing GPUs unpredictable. We propose to coordinate the action of the fetch and issue stages in GPU pipelines in order to enable reliable static timing analysis. We implement our approach in Vortex, a RISC-V-based open-source GPU. We report experiments that show that it makes warp scheduling predictable with little performance costs.

In critical real-time systems, the worst-case execution time (WCET) of software tasks must be statically bounded in order to guarantee that they all satisfy their timing constraints (e.g. deadlines). Obtaining such bounds is challenging due to the complexity of the software and of the acceleration mechanisms implemented in the hardware. Particular behaviors, known as timing anomalies, break some simplifying assumptions for the computation of WCET in single and multi-core processors. Some cores have been designed to implement a pipeline-level property known as monotonicity that guarantees that no timing anomaly can occur in the pipeline. Proving the monotonicity of a pipeline is tedious and error-prone, and so is reading the proof and convincing oneself of its validity. We thus propose to rely on the Coq proof assistant to guarantee the soundness of the proofs. In this paper, we show how the monotonicity property and the standard elements composing a pipeline can be modelled in Coq. Using an example based on an open-hardware RISC-V core from the literature, we introduce the main elements of the proof and discuss their reusability for other cores. We conclude that the model and proofs that we provide can be easily adapted to describe other in-order pipelines of equivalent complexity.

The resource-constrained environment and the certification requirements underlying embedded safety-critical real-time systems impose an adapted development process for software applications. In this work, we propose an efficient and traceable implementation of an existing blocked general matrix multiplication (GEMM) algorithm. We target time-predictability in a COTS processor with single-instruction multiple-data (SIMD) extensions. We provide a set of rules for tuning the algorithm parameters and predict with precision its number of memory accesses and cache misses, which paves the way for a static WCET analysis. Our experiments show that time-predictability comes at the cost of a performance degradation of only 2.54% on average. Moreover, tuning the parameters allows for reducing cache misses by up to 60% in certain parts of the algorithm.

Abstract Interference between tasks running on separate cores in multi-core processors is a major challenge to predictability for real-time systems, and a source of over-estimation of worst-case execution duration bounds. This paper investigates how the multi-phase task model can be used together with static scheduling algorithms to improve the precision of the interference analysis. The paper focuses on single-period task systems (or multi-periodic systems that can be expanded over an hyperperiod). In particular, we propose an Integer Linear Programming (ILP) formulation of a generic scheduling problem as well as 3 heuristics that we evaluate on synthetic benchmarks and on 2 realistic applications. We observe that, compared to the classical 1-phase model, the multi-phase model allows to reduce the effect of interference on the worst-case makespan of the system by around 9% on average using the ILP on small systems, and up to 24% on our larger case studies. These results pave the way for future heuristics and for the adoption of the multi-phase model in multi-core context.

We present MINOTAuR, an open-source RISC-V core designed to be timing predictable, i.e., free of timing anomalies: this property enables a compositional timing analysis in a multicore context. MINOTAuR features speculative execution: thanks to a specific design of its pipeline, we formally prove that speculation does not break timing predictability while sensibly increasing performance. We propose architectural extensions that enable the use of a return address stack and of any cache replacement policy, which we implemented in the MINOTAuR core. We show that a trade-off can be found between the efficiency of these components and the overhead they incur on the die area consumption, and that using them yields a performance equivalent to that of the baseline RISC-V Ariane core, while also enforcing timing predictability.

We propose a precise and efficient pipeline analysis to tackle the problem of out-of-order resources in modern embedded microprocessors for the computation of the worst-case execution time (WCET). Such resources are prone to timing anomalies (Reineke et al., 2006). To remain sound, the timing analysis must either rely on huge timing over-estimations or consider all possible pipeline states which usually leads to a combinatorial blowup. To cope with this situation, we build an efficient computational model by leveraging the algebraic properties of the execution decision diagram (Bai et al., 2020) which is able to track precisely all pipeline states all along the execution paths of the analyzed program while keeping the analysis time within acceptable range. We show how to apply this analysis at the control flow graph (CFG) level, and how to account for a typical out-of-order resource: the shared memory bus between the instruction and data caches. We observe a gain in precision of the WCET ranging from 20% to 80% compared to the state-of-the-art pipeline analysis of the OTAWA WCET toolset. The analysis time shows that our approach scales to realistic benchmarks, making it appropriate for industrial applications.

This paper investigates how the multi-phase representation of real-time tasks impacts their implementation and the precision of the interference analysis in a multi-core context. In classical scheduling and interference analyses, tasks are represented as a single phase with a duration equal to their Worst-Case Execution Time (WCET) in isolation, annotated with their worst-case number of accesses. We propose a general formal definition of a task model in which tasks are represented as a sequence of such phases: the multi-phase model. We then provide a set of general correction criteria for the implementation of tasks represented in the multi-phase model, which is agnostic of the analysis method applied on the tasks. We also use the multi-phase model on an avionics case-study and study its impact on the interference analysis. Finally, we define a set of efficiency criteria using a statistical study of the most efficient multi-phase shapes.

Due to the dynamic behaviour of acceleration mechanisms such as caches and branch predictors, static Worst-case Execution Time (WCET) analysis methods tend to scale poorly to modern hardware architectures. As a result, a trade-off must be found between the duration and the precision of the analysis, leading to an overestimation of the WCET bounds. In turn, this reduces the schedulability and resource usage of the system. In this article, we present a new data structure to speed up the analysis: the eXecution Decision Diagram (XDD), which is an ad hoc extension of Binary Decision Diagrams tailored for WCET analysis problems. We show how XDDs can be used to represent efficiently execution states in a modern hardware platform. Moreover, we propose a new process to build the Integer Linear Programming system of the Implicit Path Enumeration Technique using XDD. We use benchmark applications to demonstrate how the use of an XDD substantially increases the scalability of WCET analysis and the precision of the obtained WCET.

We present MINOTAuR, a timing predictable open source RISC-V core based on the Ariane core [28]. We first modify Ariane in order to make it timing predictable following the approach used to design the SIC processor [12]. We prove that the instruction parallelism in the Ariane core does not prevent from enforcing timing predictability. We further relax restrictions by enabling a limited amount of speculative execution and we are still able to formally prove that the core is timing predictable. Experimental results show that the performance is reduced by only 10% on average compared to the original Ariane core.

Due to the dynamic behaviour of acceleration mechanisms such as caches and branch predictors, static Worst-Case Execution Time (wcet) analysis methods tend to scale poorly to modern hardware architectures. As a result, a tradeoff must be made between the duration and the precision of the analysis, leading to an overesti- mation of the wcet bounds. This in turn reduces the schedulability and resource usage of the system. In this paper we present a new data structure to speed up the analysis: the eXecution Decision Diagram (xdd), which is an ad-hoc extension of Binary Decision Diagrams tailored for wcet analysis problems. We show how xdds can be used to represent efficiently execution states and durations of instruction sequencesn a modern hardware platform. We demon- strate on realistic applications how the use of an xdd substantially increases the scalability of wcet analysis.

We present thrifty-malloc: a transaction-friendly dynamic memory manager for high-end embedded multicore systems. The manager combines modularity, ease-of-use and hardware transactional memory (HTM) compatibility in a light-weight and memory-efficient design. Thrifty-malloc is easy to deploy and configure for non-expert programmers, yet provides good performance with low memory overhead for highly-parallel embedded applications running on massively parallel processor arrays (MPPAs) or many-core architectures. In addition, the transparent mechanisms that increase our manager's resilience to unpredictable dynamic situations incur a low timing overhead in comparison to established techniques.

We propose a software pipelining technique adapted to specific hard real-time scheduling problems. Our technique optimizes both computation throughput and execution cycle makespan, with makespan being prioritary. It also takes advantage of the predicated execution mechanisms of our embedded execution platform. To do so, it uses a reservation table formalism allowing the manipulation of the execution conditions of operations. Our reservation tables allow the double reservation of a resource at the same dates by two different operations, if the operations have exclusive execution conditions. Our analyses can determine when double reservation is possible even for operations belonging to different iterations.