Cache persistence analysis is an important part of worst-case execution time (WCET) analysis. It has been extensively studied in the past twenty years. Despite these efforts, all existing persistence analyses are approximative in the sense that they are not guaranteed to find all persistent memory blocks. In this paper, we close this gap by introducing the first exact persistence analysis for caches with least-recently-used (LRU) replacement. To this end, we first introduce an exact abstraction that exploits monotonicity properties of LRU to significantly reduce the information the analysis needs to maintain for exact persistence classifications. We show how to efficiently implement this abstraction using zero-suppressed binary decision diagrams (ZDDs) and introduce novel techniques to deal with uncertainty that arises during the analysis of data caches. The experimental evaluation demonstrates that the new exact analysis is competitive with state-of-the-art inexact analyses in terms of both memory consumption and analysis run time, which is somewhat surprising as we show that persistence analysis is NP-complete. We also observe that while prior analyses are not exact in theory they come close to being exact in practice.

We introduce the strictly in-order core (SIC), a timing-predictable pipelined processor core. SIC is provably timing compositional and free of timing anomalies. This enables precise and efficient worst-case execution time (WCET) and multi-core timing analysis. SIC's key underlying property is the monotonicity of its transition relation w.r.t. a natural partial order on its microarchitectural states. This monotonicity is achieved by carefully eliminating some of the dependencies between consecutive instructions from a standard in-order pipeline design. SIC preserves most of the benefits of pipelining: it is only about 6-7% slower than a conventional pipelined processor. Its timing predictability enables orders-of-magnitude faster WCET and multi-core timing analysis than conventional designs.

Write-back caches are a popular choice in embedded microprocessors as they promise higher performance than write-through caches. So far, however, their use in hard real-time systems has been prohibited by the lack of adequate worst-case execution time (WCET) analysis support. In this paper, we introduce a new approach to statically analyze the behavior of write-back caches. Prior work took an "eviction-focussed perspective", answering for each potential cache miss: May this miss evict a dirty cache line and thus cause a write back? We complement this approach by exploring a "store-focussed perspective", answering for each store: May this store dirtify a clean cache line and thus cause a write back later on? Experimental evaluation demonstrates substantial precision improvements when both perspectives are combined. For most benchmarks, write-back caches are then preferable to write-through caches in terms of the computed WCET bounds.

Multi-core processors share common hardware resources between several processor cores. As a consequence, the performance of one processor core is influenced by the programs executed on the concurrent cores. We refer to this phenomenon as shared-resource interference. An explicit consideration of all such interference effects is in general combinatorially infeasible. This makes a precise worst-case execution time (WCET) analysis for multi-core processors challenging. In order to reduce the complexity, WCET analyses for multi-core processors coarsely approximate the behavior of the considered applications. However, current approaches are only applicable to rather restricted classes of hardware platforms. We propose a framework for the derivation of WCET analyses for multi-core processors. It relaxes the restricting assumptions that existing approaches are based on. The derivation starts from a WCET analysis that makes maximally pessimistic assumptions about the shared-resource interference. More precise interference bounds for the concrete system are subsequently lifted to the approximation of the analysis. The lifted bounds are finally incorporated in the analysis in order to model the interference in a more precise way.

We introduce Selfish-LRU, a variant of the LRU (least recently used) cache replacement policy that improves performance and predictability in preemptive scheduling scenarios. In multitasking systems with conventional caches, a single memory access by a preempting task can trigger a chain reaction leading to a large number of additional cache misses in the preempted task. Selfish-LRU prevents such chain reactions by first evicting cache blocks that do not belong to the currently active task. Simulations confirm that Selfish-LRU reduces the CRPD (cache-related preemption delay) as well as the overall number of cache misses. At the same time, it simplifies CRPD analysis and results in smaller CRPD bounds.

Static cache analysis is an indispensable part of static timing analysis, which is employed to verify the timing behaviour of programs in safety-critical real-time systems. State-of-the-art cache analyses classify memory references as `always hit', `always miss', or `unknown'. To do so, they rely on a preceding address analysis that tries to determine the referenced addresses. If a referenced address is not determined precisely, however, those cache analyses cannot predict this reference as hit or miss. On top of that, information about other cache contents is lost upon such references. We present a novel approach to static cache analysis that alleviates the dependency on precise address analysis. Instead of having to argue about concrete addresses, we only need to argue about relations between referenced addresses, e.g. `accesses same memory block' or `maps to different cache set'. Such relations can be determined by congruence analyses, without precise knowledge about the actual addresses. The subsequent cache analysis then only relies on relations to infer cache information and to classify references. One advantage of this approach is that hits can be predicted for references with imprecisely determined addresses, even if there is no information about accessed addresses. In particular, this enables the prediction of hits for references whose addresses depend on an unknown stack pointer or even depend on the program input. Relational cache analysis is always at least as precise as the corresponding state-of-the-art cache analysis. Furthermore, we demonstrate significant improvements for three classes of program constructs.