VLDB 2026 Research / reviewers in the wild / expert
Jan Reineke 0001
dblp:67/3331
· DBLP profile ↗
59ranked-venue papers
11as first author
11since 2021 · last 2025
0000-0002-3459-2214ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 23 · 6 first-author · 4 since 2021Software engineering, systems software and programming languages · 19 · 5 first-author · 2 since 2021Security and privacy · 7 · 4 since 2021Theory of computation · 6 · 2 first-authorApplied, interdisciplinary, general and emerging computing · 5 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V ProcessorsabstractLeakage contracts have been proposed as a new security abstraction at the instruction set architecture level. Leakage contracts aim to capture the information that processors may leak via microarchitectural side channels. Recently, the first tools have emerged to verify whether a processor satisfies a given contract. However, coming up with a contract that is both sound and precise for a given processor is challenging, time-consuming, and error-prone, as it requires in-depth knowledge of the timing side channels introduced by microarchitectural optimizations. Zilong Wang 0027, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke 0001, Marco Guarnieri |
CCS | 4 |
| 2025 | A Unified Framework for Quantitative Cache AnalysisabstractIn this work we unify two existing lines of work towards cache analysis for non-LRU policies. To this end, we extend the notion of competitiveness to block competitiveness and systematically analyze the competitiveness and block competitiveness of FIFO and MRU relative to LRU for arbitrary associativities. We show how competitiveness and block competitiveness can be exploited in state-of-the-art WCET analysis based on the results of existing persistence analyses for LRU. Unlike prior work, our approach is applicable to microarchitectures that exhibit timing anomalies. We experimentally evaluate the precision and cost of our approach on benchmarks from TACLeBench. The experiments demonstrate that quantitative cache analysis for FIFO and MRU comes close to the precision of LRU. Sophie Kahlen, Jan Reineke 0001 |
RTAS | 2 |
| 2024 | No Leakage Without State Change: Repurposing Configurable CPU Exceptions to Prevent Microarchitectural AttacksabstractMicroarchitectural side-channel attacks have become significant threats to computer system security. While writing side-channel-resistant code can mitigate these attacks, it is time-consuming and error-prone. Detection approaches provide an alternative by monitoring the system for signs of ongoing attacks. However, distinguishing between malicious and benign processes is complex, error-prone, and ineffective against sophisticated attacks.In this paper, we propose a novel approach, IRQGuard, which shifts the focus to proactive mitigation. IRQGuard enables the victim to monitor its own microarchitectural events resulting from microarchitectural state changes. Leveraging existing CPU features, IRQGuard uses interrupt requests (IRQs) triggered by victim-specific microarchitectural state changes within predefined code regions. This self-monitoring eliminates noise of unrelated applications, enabling immediate detection and response to potential attacks. Our proof-of-concept implementation demonstrates that IRQGuard stops information leakage in under 200 CPU cycles, outperforming current methods significantly. We evaluate IRQGuard on both cryptographic (OpenSSL) and non-cryptographic (toilet command-line utility) applications. We demonstrate IRQGuard’s real-world viability by protecting an OpenSSH server from cache attacks. IRQGuard offers a practical, low-overhead solution for mitigating a wide range of microarchitectural attacks on Intel, AMD, and Arm CPUs. Daniel Weber 0007, Leonard Niemann, Lukas Gerlach 0001, Jan Reineke 0001, Michael Schwarz 0001 |
ACSAC | 4 |
| 2024 | Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source ProcessorsabstractMicroarchitectural attacks compromise security by exploiting software-visible artifacts of microarchitectural optimizations such as caches and speculative execution. Defending against such attacks at the software level requires an appropriate abstraction at the instruction set architecture (ISA) level that captures microarchitectural leakage. Hardware-software leakage contracts have recently been proposed as such an abstraction. In this paper, we propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. For a given ISA, our approach relies on human experts to (a) capture the space of possible contracts in the form of contract templates and (b) devise a test-case generation strategy to explore a microarchitecture's potential leakage. For a given implementation of an ISA, these two ingredients are then used to automatically synthesize the most precise leakage contract that is satisfied by the microarchitecture. We have instantiated this methodology for the RISC- V ISA and applied it to the Ibex and CVA6 open-source processors. Our experiments demonstrate the practical applicability of the methodology and uncover subtle and unexpected leaks. Gideon Mohr, Marco Guarnieri, Jan Reineke 0001 |
DATE | 3 |
| 2023 | Specification and Verification of Side-channel Security for Open-source Processors via Leakage ContractsabstractLeakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Leakage contracts aim to capture the information that processors leak through their microarchitectural implementations. However, so far, we lack a methodology to verify that a processor actually satisfies a given leakage contract. Zilong Wang 0027, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke 0001, Marco Guarnieri |
CCS | 4 |
| 2023 | Leveraging LLVM's ScalarEvolution for Symbolic Data Cache AnalysisabstractWhile instruction cache analysis is essentially a solved problem, data cache analysis is more challenging. In contrast to instruction fetches, the data accesses generated by a memory instruction may vary with the program's inputs and across dynamic occurrences of the same instruction in loops. We observe that the plain control-flow graph (CFG) abstraction employed in classical cache analyses is inadequate to capture the dynamic behavior of memory instructions. On top of plain CFGs, accurate analysis of the underlying program's cache behavior is impossible. Thus, our first contribution is the definition of a more expressive program abstraction coined symbolic control-flow graphs, which can be obtained from LLVM's ScalarEvolution analysis. To exploit this richer abstraction, our main contribution is the development of symbolic data cache analysis, a smooth generalization of classical LRU must analysis from plain to symbolic control-flow graphs. The experimental evaluation demonstrates that symbolic data cache analysis consistently outperforms classical LRU must analysis both in terms of accuracy and analysis runtime. Valentin Touzeau, Jan Reineke 0001 |
RTSS | 2 |
| 2023 | Type-Aware Federated Scheduling for Typed DAG Tasks on Heterogeneous Multicore PlatformsabstractTo utilize the performance benefits of heterogeneous multicore platforms in real-time systems, we need task models that expose the parallelism and heterogeneity of the workload, such as typed DAG tasks, as well as scheduling algorithms that effectively exploit this information. In this paper, we introducetype-aware federated schedulingalgorithms for sporadic typed DAG tasks with implicit deadlines running on a heterogeneous multicore platform with two different types of cores. In type-aware federated scheduling, a task can be executed in one of the three strategies:Exclusive Allocation,Semi-Exclusive Allocation, andSequential and Share. InExclusive Allocation, clusters of cores of both core types are exclusively allocated to tasks, while cores of only one type are exclusively allocated to tasks inSemi-Exclusive Allocation. The workload of the other type from tasks inSemi-Exclusive Allocationand the workload from tasks inSequential and Shareshare the cores that are not exclusively allocated to any task. We prove that our type-aware federated scheduling algorithm has a capacity augmentation bound of 7.25. We also show that no constant capacity augmentation bound can be obtained withoutSemi-Exclusive Allocation. Compared to the state of the art, the type-aware federated scheduling algorithm achieves better schedulability, especially for task sets with skewed workload. Ching-Chi Lin, Niklas Ueter, Mario Günzel, Jan Reineke 0001, Jian-Jia Chen |
IEEE Trans. Computers | 5 |
| 2022 | uiCA: accurate throughput prediction of basic blocks on recent intel microarchitecturesabstractPerformance models that statically predict the steady-state throughput of basic blocks on particular microarchitectures, such as IACA, Ithemal, llvm-mca, OSACA, or CQA, can guide optimizing compilers and aid manual software optimization. However, their utility heavily depends on the accuracy of their predictions. The average error of existing models compared to measurements on the actual hardware has been shown to lie between 9% and 36%. But how good is this? To answer this question, we propose an extremely simple analytical throughput model that may serve as a baseline. Surprisingly, this model is already competitive with the state of the art, indicating that there is significant potential for improvement. Andreas Abel 0002, Jan Reineke 0001 |
ICS | 2 |
| 2022 | Warping cache simulation of polyhedral programsabstractTechniques to evaluate a program's cache performance fall into two camps: 1. Traditional trace-based cache simulators precisely account for sophisticated real-world cache models and support arbitrary workloads, but their runtime is proportional to the number of memory accesses performed by the program under analysis. 2. Relying on implicit workload characterizations such as the polyhedral model, analytical approaches often achieve problem-size-independent runtimes, but so far have been limited to idealized cache models. Canberk Morelli, Jan Reineke 0001 |
PLDI | 2 |
| 2022 | On the Trade-offs between Generalization and Specialization in Real-Time SystemsabstractWhile academia favours general research that is applicable to a large class of systems, this paper highlights the necessity of research into specific scenarios and aims to increase its acceptance in the real-time systems community. We argue that such research is not only motivated by greater applicability to industry, but that specialization can also provide valuable information from a purely academic perspective. In addition, the trade-offs between generalization and specialization are examined, considering not only theoretical performance, but also the impact on essential non-functional properties that are important for industry, namely composability, robustness, extensibility, and parametric simplicity. Georg von der Brüggen, Alan Burns 0001, Jian-Jia Chen, Robert I. Davis 0001, Jan Reineke 0001 |
RTCSA | 5 |
| 2021 | Hardware-Software Contracts for Secure SpeculationabstractSince the discovery of Spectre, a large number of hardware mechanisms for secure speculation has been proposed. Intuitively, more defensive mechanisms are less efficient but can securely execute a larger class of programs, while more permissive mechanisms may offer more performance but require more defensive programming. Unfortunately, there are no hardware-software contracts that would turn this intuition into a basis for principled co-design.In this paper, we put forward a framework for specifying such contracts, and we demonstrate its expressiveness and flexibility.On the hardware side, we use the framework to provide the first formalization and comparison of the security guarantees provided by a representative class of mechanisms for secure speculation.On the software side, we use the framework to characterize program properties that guarantee secure co-design in two scenarios traditionally investigated in isolation: (1) ensuring that a benign program does not leak information while computing on confidential data, and (2) ensuring that a potentially malicious program cannot read outside of its designated sandbox. Finally, we show how the properties corresponding to both scenarios can be checked based on existing tools for software verification, and we use them to validate our findings on executable code. Marco Guarnieri, Boris Köpf, Jan Reineke 0001, Pepe Vila |
SP | 3 |
| 2020 | nanoBench: A Low-Overhead Tool for Running Microbenchmarks on x86 SystemsabstractWe present nanoBench, a tool for evaluating small microbenchmarks using hardware performance counters on Intel and AMD x86 systems. Most existing tools and libraries are intended to either benchmark entire programs, or program segments in the context of their execution within a larger program. In contrast, nanoBench is specifically designed to evaluate small, isolated pieces of code. Such code is common in microbenchmark-based hardware analysis techniques. Unlike previous tools, nanoBench can execute microbenchmarks directly in kernel space. This allows to benchmark privileged instructions, and it enables more accurate measurements. The reading of the performance counters is implemented with minimal overhead avoiding functions calls and branches. As a consequence, nanoBench is precise enough to measure individual memory accesses. We illustrate the utility of nanoBench at the hand of two case studies. First, we briefly discuss how nanoBench has been used to determine the latency, throughput, and port usage of more than 13,000 instruction variants on recent x86 processors. Second, we show how to generate microbenchmarks to precisely characterize the cache architectures of eleven Intel Core microarchitectures. This includes the most comprehensive analysis of the employed cache replacement policies to date. Andreas Abel 0002, Jan Reineke 0001 |
ISPASS | 2 |
| 2020 | Spectector: Principled Detection of Speculative Information FlowsabstractSince the advent of Spectre, a number of counter-measures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now.In this paper (1) we put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and (2) we develop Spectector, an algorithm based on symbolic execution to automatically prove speculative non-interference, or to detect violations.We implement Spectector in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place Spectre countermeasures. A scalability analysis indicates that checking speculative non-interference does not exhibit fundamental bottlenecks beyond those inherited by symbolic execution. Marco Guarnieri, Boris Köpf, José F. Morales 0001, Jan Reineke 0001, Andrés Sánchez |
SP | 4 |
| 2020 | Design and analysis of SIC: a provably timing-predictable pipelined processor core
Sebastian Hahn 0001, Jan Reineke 0001 |
Real Time Syst. | 2 |
| 2019 | uops.info: Characterizing Latency, Throughput, and Port Usage of Instructions on Intel MicroarchitecturesabstractModern microarchitectures are some of the world's most complex man-made systems. As a consequence, it is increasingly difficult to predict, explain, let alone optimize the performance of software running on such microarchitectures. As a basis for performance predictions and optimizations, we would need faithful models of their behavior, which are, unfortunately, seldom available. Andreas Abel 0002, Jan Reineke 0001 |
ASPLOS | 2 |
| 2019 | Cache Persistence Analysis: Finally ExactabstractCache 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. Gregory Stock 0002, Sebastian Hahn 0001, Jan Reineke 0001 |
RTSS | 3 |
| 2019 | On the Incomparability of Cache Algorithms in Terms of Timing LeakageabstractModern computer architectures rely on caches to reduce the latency gap between the CPU and main memory. While indispensable for performance, caches pose a serious threat to security because they leak information about memory access patterns of programs via execution time. In this paper, we present a novel approach for reasoning about the security of cache algorithms with respect to timing leaks. The basis of our approach is the notion of leak competitiveness, which compares the leakage of two cache algorithms on every possible program. Based on this notion, we prove the following two results: First, we show that leak competitiveness is symmetric in the cache algorithms. This implies that no cache algorithm dominates another in terms of leakage via a program's total execution time. This is in contrast to performance, where it is known that such dominance relationships exist. Second, when restricted to caches with finite control, the leak-competitiveness relationship between two cache algorithms is either asymptotically linear or constant. No other shapes are possible. Pablo Cañones, Boris Köpf, Jan Reineke 0001 |
Log. Methods Comput. Sci. | 3 |
| 2019 | Fast and exact analysis for LRU cachesabstractFor applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that result in cache misses. Among cache replacement policies, the least recently used (LRU) policy has been studied the most and is considered to be the most predictable. The state-of-the-art in LRU cache analysis presents a tradeoff between precision and analysis efficiency: The classical approach to analyzing programs running on LRU caches, an abstract interpretation based on a range abstraction, is very fast but can be imprecise. An exact analysis was recently presented, but, as a last resort, it calls a model checker, which is expensive. In this paper, we develop an analysis based on abstract interpretation that comes close to the efficiency of the classical approach, while achieving exact classification of all memory accesses as the model-checking approach. Compared with the model-checking approach we observe speedups of several orders of magnitude. As a secondary contribution we show that LRU cache analysis problems are in general NP-complete. Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke 0001 |
Proc. ACM Program. Lang. | 4 |
| 2019 | Basic problems in multi-view modeling
Jan Reineke 0001, Christos Stergiou 0001, Stavros Tripakis |
Softw. Syst. Model. | 1 |
| 2018 | Design and Analysis of SIC: A Provably Timing-Predictable Pipelined Processor CoreabstractWe 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. Sebastian Hahn 0001, Jan Reineke 0001 |
RTSS | 2 |
| 2018 | On the Smoothness of Paging Algorithms
Jan Reineke 0001, Alejandro Salinger |
Theory Comput. Syst. | 1 |
| 2018 | An extensible framework for multicore response time analysisabstractIn this paper, we introduce a multicore response time analysis ( MRTA ) framework , which decouples response time analysis from a reliance on context-independent WCET values. Instead, the analysis formulates response times directly from the demands placed on different hardware resources. The MRTA framework is extensible to different multicore architectures, with a variety of arbitration policies for the common interconnects, and different types and arrangements of local memory. We instantiate the framework for single level local data and instruction memories (cache or scratchpads), for a variety of memory bus arbitration policies, including: Round-Robin, FIFO, Fixed-Priority, Processor-Priority, and TDMA, and account for DRAM refreshes. The MRTA framework provides a general approach to timing verification for multicore systems that is parametric in the hardware configuration and so can be used at the architectural design stage to compare the guaranteed levels of real-time performance that can be obtained with different hardware configurations. We use the framework in this way to evaluate the performance of multicore systems with a variety of different architectural components and policies. These results are then used to compose a predictable architecture, which is compared against a reference architecture designed for good average-case behaviour. This comparison shows that the predictable architecture has substantially better guaranteed real-time performance, with the precision of the analysis verified using cycle-accurate simulation. Robert I. Davis 0001, Sebastian Altmeyer, Leandro Soares Indrusiak, Claire Maïza, Vincent Nélis, Jan Reineke 0001 |
Real Time Syst. | 6 |
| 2018 | Response-time analysis for fixed-priority systems with a write-back cacheabstractThis paper introduces analyses of write-back caches integrated into response-time analysis for fixed-priority preemptive and non-preemptive scheduling. For each scheduling paradigm, we derive four different approaches to computing the additional costs incurred due to write backs. We show the dominance relationships between these different approaches and note how they can be combined to form a single state-of-the-art approach in each case. The evaluation explores the relative performance of the different methods using a set of benchmarks, as well as making comparisons with no cache and a write-through cache. We also explore the effect of write buffers used to hide the latency of write-through caches. We show that depending upon the depth of the buffer used and the policies employed, such buffers can result in domino effects. Our evaluation shows that even ignoring domino effects, a substantial write buffer is needed to match the guaranteed performance of write-back caches. Robert I. Davis 0001, Sebastian Altmeyer, Jan Reineke 0001 |
Real Time Syst. | 3 |
| 2018 | Checking multi-view consistency of discrete systems with respect to periodic sampling abstractions
Maria Pittou, Panagiotis Manolios, Jan Reineke 0001, Stavros Tripakis |
Sci. Comput. Program. | 3 |
| 2017 | Ascertaining Uncertainty for Efficient Exact Cache Analysis
Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke 0001 |
CAV (2) | 4 |
| 2017 | Write-Back Caches in WCET AnalysisabstractWrite-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. Tobias Stark, Sebastian Hahn 0001, Jan Reineke 0001 |
ECRTS | 3 |
| 2017 | Memory Bank Partitioning for Fixed-Priority Tasks in a Multi-core SystemabstractIn a multi-core platform, resources, such as memory banks and buses, are mostly shared among all cores for power, performance, and cost reasons. The access interference on the shared resources poses a major challenge on the analysis of real-time properties, but can be alleviated if task data partition onto memory banks is applied with care. In this paper, we consider to schedule RAS (resource access sporadic) tasks onto a platform consisting of homogeneous cores and capacity-limited memory banks. According to our observation, we should avoid internal data spreading among the memory banks for a task while advocate external data spreading among memory banks for a given task set. We propose a two-phase algorithm with (4 + ρ + 3(2γ+1)/γ) speedup factor and (γ + 1) memory augmentation factor, where ρ γ 0 and ρ ≥ 1. The derived adjustable resource augmentation factors can be useful in terms of system synthesis and schedulability. Moreover, under the premise that a given task set is feasible, we devise a bi-section approach that can derive a schedulable solution requiring the least amount of memory augmentation. According to our experiment results, the proposed algorithm significantly outperformed the state-of-the-art algorithm [15] in terms of schedulability test even when memory augmentation is prohibited. Sheng-Wei Cheng, Jian-Jia Chen, Jan Reineke 0001, Tei-Wei Kuo |
RTSS | 3 |
| 2017 | Abstract PRET MachinesabstractPrior work has shown that it is possible to design microarchitectures called PRET machines that deliver precise and repeatable timing of software execution without sacrificing performance. That prior work provides specific designs for PRET microarchitectures and compares them against conventional designs. This paper defines a class of microarchitectures called abstract PRET machines (APMs) that capture the essential temporal properties of PRET machines. We show that APMs deliver deterministic timing with no loss of performance for a family of real-time problems consisting of sporadic event streams with deadlines equal to periods. On the other hand, we observe a tradeoff between deterministic timing and the ability to meet deadlines for sporadic event streams with constrained deadlines. Edward A. Lee, Jan Reineke 0001, Michael Zimmer 0001 |
RTSS | 2 |
| 2016 | MIRROR: symmetric timing analysis for real-time tasks on multicore platforms with shared resourcesabstractThe emergence of multicore and manycore platforms poses a big challenge for the design of real-time embedded systems, especially for timing analysis. We observe in this paper that response-time analysis for multicore platforms with shared resources can be symmetrically approached from two perspectives: a core-centric and a shared-resource-centric perspective. The common "core-centric" perspective is that a task executes on a core until it suspends the execution due to shared resource accesses. The potentially less intuitive "shared-resource-centric" perspective is that a task performs requests on shared resources until suspending itself back to perform computation on its respective core. Wen-Hung Kevin Huang, Jian-Jia Chen, Jan Reineke 0001 |
DAC | 3 |
| 2015 | MeMin: SAT-based Exact Minimization of Incompletely Specified Mealy MachinesabstractIn this paper, we take a fresh look at a well-known NP-complete problem-the exact minimization of incompletely specified Mealy machines. Most existing exact techniques in this area are based on the enumeration of sets of compatible states, and the solution of a covering problem. We propose a different approach. In our approach, first, a polynomial-time algorithm is used to compute a partial solution. This partial solution is then extended to a minimum-size complete solution by solving a series of boolean satisfiability (SAT) problems. We evaluate our implementation on the same set of benchmarks used previously in the literature. On a number of hard benchmarks, our approach outperforms existing exact minimization techniques by several orders of magnitude; it is even competitive with state-of-the-art heuristic approaches on most benchmarks. Andreas Abel 0002, Jan Reineke 0001 |
ICCAD | 2 |
| 2015 | ASTRA: A Tool for Abstract Interpretation of Graph Transformation Systems
Peter Backes, Jan Reineke 0001 |
SPIN | 2 |
| 2015 | Analysis of Infinite-State Graph Transformation Systems by Cluster Abstraction
Peter Backes, Jan Reineke 0001 |
VMCAI | 2 |
| 2015 | On the Smoothness of Paging Algorithms
Jan Reineke 0001, Alejandro Salinger |
WAOA | 1 |
| 2015 | CacheAudit: A Tool for the Static Analysis of Cache Side ChannelsabstractWe present CacheAudit, a versatile framework for the automatic, static analysis of cache side channels. CacheAudit takes as input a program binary and a cache configuration and derives formal, quantitative security guarantees for a comprehensive set of side-channel adversaries, namely, those based on observing cache states, traces of hits and misses, and execution times. Our technical contributions include novel abstractions to efficiently compute precise overapproximations of the possible side-channel observations for each of these adversaries. These approximations then yield upper bounds on the amount of information that is revealed. In case studies, we apply CacheAudit to binary executables of algorithms for sorting and encryption, including the AES implementation from the PolarSSL library, and the reference implementations of the finalists of the eSTREAM stream cipher competition. The results we obtain exhibit the influence of cache size, line size, associativity, replacement policy, and coding style on the security of the executables and include the first formal proofs of security for implementations with countermeasures such as preloading and data-independent memory access patterns. Goran Doychev, Boris Köpf, Laurent Mauborgne, Jan Reineke 0001 |
ACM Trans. Inf. Syst. Secur. | 4 |
| 2014 | Impact of resource sharing on performance and performance predictionabstractMulti-core processors are increasingly considered as execution platforms for embedded systems because of their good performance/energy ratio. Many applications implemented on multi-core platforms are safety- and some also time-critical. A critical issue for these applications is the reduced predictability of such systems resulting from the interference of different applications on shared resources. These interferences can be at least of two kinds: Several applications may request a resource at the same time, but the resource can only admit one access at a time. As a consequence, an arbitration mechanism may delay the request of all but one application, thus slowing down the other applications. This is the case of resources like buses, typically called bandwidth resources. On the other hand, one application may also change the state of a shared resource such that another application using that resource will suffer from a slowdown. This is the case with shared memories, such as shared caches and shared dynamic random-access memories, which fall into the class of storage resources. Interference on shared resources makes worst-case execution time (WCET) analysis of applications more difficult since a task or a thread can no longer be analyzed for its timing behavior in isolation. All potential interferences slowing down (or speeding up) the task under analysis have to be considered. This leads to a combinatorial explosion of the analysis complexity, as all possible interleavings of different threads have to be analyzed. The survey [1] considers several aspects of the execution of sets of tasks on multi-core platforms that have to do with the interference of the tasks on shared resources. One question is how the actual performance of tasks is slowed down by other co-running tasks. Another is how to compute bounds on the slow-down in order to derive sound guarantees for the timing behavior. A major problem is the increased complexity of this task compared to the single-task single-core case. This has led to the situation that industry is developing embedded systems for multi-core platforms while there exist no timing-analysis methods and tools that are both sound and precise. Jan Reineke 0001, Reinhard Wilhelm |
DATE | 1 |
| 2014 | Reverse engineering of cache replacement policies in Intel microprocessors and their evaluationabstractPerformance modeling techniques need accurate cache models to produce useful estimates. However, properties required for building such models, like the replacement policy, are often not documented. In this paper, using a set of carefully designed microbenchmarks, we reverse engineer a precise model of caches found in recent Intel processors that enables accurate prediction of their cache performance by simulation. In particular, we identify two variants of pseudo-LRU that, unlike previously documented policies, employ randomization. We evaluate their performance and demonstrate that it differs significantly from known pseudo-LRU variants on some benchmarks. Andreas Abel 0002, Jan Reineke 0001 |
ISPASS | 2 |
| 2014 | Selfish-LRU: Preemption-aware caching for predictability and performanceabstractWe 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. Jan Reineke 0001, Sebastian Altmeyer, Daniel Grund, Sebastian Hahn 0001, Claire Maïza |
RTAS | 1 |
| 2014 | Architecture-parametric timing analysisabstractPlatforms are families of microarchitectures that implement the same instruction set architecture but that differ in architectural parameters, such as frequency, memory latencies, or memory sizes. The choice of these parameters influences execution time, implementation cost, and energy consumption. In this paper, we introduce the first general framework for architecture-parametric timing analysis (APTA). APTA computes an expression that bounds the worst-case execution time (WCET) of a program in terms of architectural parameters. This enables to configure a platform, at design or even at run time, in a way that is guaranteed to meet all deadlines, while minimizing implementation cost and/or energy consumption. We demonstrate the feasibility of our approach by implementing APTA for a precision-timed (PRET) platform and by evaluating our implementation on Mälardalen benchmarks. Jan Reineke 0001, Johannes Doerfert |
RTAS | 1 |
| 2014 | Basic Problems in Multi-View Modeling
Jan Reineke 0001, Stavros Tripakis |
TACAS | 1 |
| 2014 | Building timing predictable embedded systemsabstractA large class of embedded systems is distinguished from general-purpose computing systems by the need to satisfy strict requirements on timing, often under constraints on available resources. Predictable system design is concerned with the challenge of building systems for which timing requirements can be guaranteed a priori . Perhaps paradoxically, this problem has become more difficult by the introduction of performance-enhancing architectural elements, such as caches, pipelines, and multithreading, which introduce a large degree of uncertainty and make guarantees harder to provide. The intention of this article is to summarize the current state of the art in research concerning how to build predictable yet performant systems. We suggest precise definitions for the concept of “predictability”, and present predictability concerns at different abstraction levels in embedded system design. First, we consider timing predictability of processor instruction sets. Thereafter, we consider how programming languages can be equipped with predictable timing semantics, covering both a language-based approach using the synchronous programming paradigm, as well as an environment that provides timing semantics for a mainstream programming language (in this case C). We present techniques for achieving timing predictability on multicores. Finally, we discuss how to handle predictability at the level of networked embedded systems where randomly occurring errors must be considered. Philip Axer, Rolf Ernst, Heiko Falk, Alain Girault, Daniel Grund, Nan Guan, Bengt Jonsson 0001, Peter Marwedel, Jan Reineke 0001, Christine Rochange, Maurice Sebastian, Reinhard von Hanxleden, Reinhard Wilhelm, Wang Yi 0001 |
ACM Trans. Embed. Comput. Syst. | 9 |
| 2013 | Impact of Resource Sharing on Performance and Performance Prediction: A Survey
Andreas Abel 0002, Florian Benz, Johannes Doerfert, Barbara Dörr, Sebastian Hahn 0001, Florian Haupenthal, Michael Jacobs 0002, Armin Moin, Jan Reineke 0001, Bernhard Schommer, Reinhard Wilhelm |
CONCUR | 9 |
| 2013 | Precise timing analysis for direct-mapped cachesabstractSafety-critical systems require guarantees on their worst-case execution times. This requires modelling of speculative hardware features such as caches that are tailored to improve the average-case performance, while ignoring the worst case, which complicates the Worst Case Execution Time (WCET) analysis problem. Existing approaches that precisely compute WCET suffer from state-space explosion. In this paper, we present a novel cache analysis technique for direct-mapped instruction caches with the same precision as the most precise techniques, while improving analysis time by up to 240 times. This improvement is achieved by analysing individual control points separately, and carrying out optimisations that are not possible with existing techniques. Sidharta Andalam, Alain Girault, Roopak Sinha, Partha S. Roop, Jan Reineke 0001 |
DAC | 5 |
| 2013 | Measurement-based modeling of the cache replacement policyabstractModern microarchitectures employ memory hierarchies involving one or more levels of cache memory to hide the large latency gap between the processor and main memory. Cycle-accurate simulators, self-optimizing software systems, and platform-aware compilers need accurate models of the memory hierarchy to produce useful results. Similarly, worst-case execution time analyzers require faithful models, both for soundness and precision. Unfortunately, sufficiently precise documentation of the logical organization of the memory hierarchy is seldom available publicly. In this paper, we propose an algorithm to automatically model the cache replacement policy by measurements on the actual hardware. We have implemented and applied this algorithm to various popular microarchitectures, uncovering a previously undocumented cache replacement policy in the Intel Atom D525. Andreas Abel 0002, Jan Reineke 0001 |
IEEE Real-Time and Embedded Technology and Applications Symposium | 2 |
| 2013 | CacheAudit: A Tool for the Static Analysis of Cache Side Channels
Goran Doychev, Dominik Feld, Boris Köpf, Laurent Mauborgne, Jan Reineke 0001 |
USENIX Security Symposium | 5 |
| 2013 | Sensitivity of cache replacement policiesabstractThe sensitivity of a cache replacement policy expresses to what extent the execution history may influence the number of cache hits and misses during program execution. We present an algorithm to compute the sensitivity of a replacement policy. We have implemented this algorithm in a tool called R elacs that can handle a large class of replacement policies including LRU, FIFO, PLRU, and MRU. Sensitivity properties obtained with R elacs demonstrate that the execution history can have a strong impact on the number of cache hits and misses if FIFO, PLRU, or MRU is used. A simple model of execution time is used to evaluate the impact of cache sensitivity on measured execution times. The model shows that measured execution times may strongly underestimate the worst-case execution time for FIFO, PLRU, and MRU. Jan Reineke 0001, Daniel Grund |
ACM Trans. Embed. Comput. Syst. | 1 |
| 2012 | A PRET microarchitecture implementation with repeatable timing and competitive performanceabstractWe contend that repeatability of execution times is crucial to the validity of testing of real-time systems. However, computer architecture designs fail to deliver repeatable timing, a consequence of aggressive techniques that improve average-case performance. This paper introduces the Precision-Timed ARM (PTARM), a precision-timed (PRET) microarchitecture implementation that exhibits repeatable execution times without sacrificing performance. The PTARM employs a repeatable thread-interleaved pipeline with an exposed memory hierarchy, including a repeatable DRAM controller. Our benchmarks show an improved throughput compared to a single-threaded in-order five-stage pipeline, given sufficient parallelism in the software. Isaac Liu, Jan Reineke 0001, David Broman, Michael Zimmer 0001, Edward A. Lee |
ICCD | 2 |
| 2011 | Temporal isolation on multiprocessing architecturesabstractMultiprocessing architectures provide hardware for executing multiple tasks simultaneously via techniques such as simultaneous multithreading and symmetric multiprocessing. The problem addressed by this paper is that even when tasks that are executing concurrently do not communicate, they may interfere by affecting each others' timing. For cyber-physical system applications, such interference can nullify many of the advantages offered by parallel hardware and can enormously complicate synthesis of software from models. This paper examines what changes need to be made at lower levels of abstraction to support temporal isolation for effective software synthesis. We discuss techniques at the microarchitecture level, in the memory hierarchy, in on-chip communication, and in the instruction-set architecture that can facilitate temporal isolation. Dai N. Bui, Edward A. Lee, Isaac Liu, Hiren D. Patel, Jan Reineke 0001 |
DAC | 5 |
| 2011 | CAMA: A Predictable Cache-Aware Memory AllocatorabstractGeneral-purpose dynamic memory allocation algorithms strive for small memory fragmentation and good average-case response times. Hard real-time settings, in contrast, place different demands on dynamic memory allocators: worst-case response times are more important than average-case response times. Furthermore, predictable cache behavior is a prerequisite for timing analysis to derive tight bounds on a program's execution time. This paper proposes a novel algorithm that meets these demands. It guarantees constant response times, does not cause unpredictable cache pollution, and allocations are cache-set directed, i.e., allocated memory is guaranteed to be mapped to a given cache set. The latter two are necessary to enable a subsequent precise static cache analysis. Jörg Herter, Peter Backes, Florian Haupenthal, Jan Reineke 0001 |
ECRTS | 4 |
| 2011 | Branch target buffers: WCET analysis framework and timing predictability
Daniel Grund, Jan Reineke 0001, Gernot Gebhard |
J. Syst. Archit. | 2 |
| 2010 | Precise and Efficient FIFO-Replacement Analysis Based on Static Phase DetectionabstractSchedulability analysis for hard real-time systems requires bounds on the execution times of its tasks. To obtain useful bounds in the presence of caches, static timing analyses must predict cache hits and misses with high precision. For caches with least-recently-used (LRU) replacement policy, precise and efficient cache analyses exist. However, other widely used policies like first-in first-out (FIFO) are inherently harder to analyze. The main contributions of this paper are precise and efficient must- and may-analyses of FIFO based on the novel concept of static phase detection. The analyses statically partition sequences of memory accesses as they will occur during program execution into phases. If subsequent phases contain accesses to the same (similar) set of memory blocks, each phase contributes a bit to the overall goal of predicting hits (misses). The new must-analysis is significantly more precise than prior analyses. Both analyses can be implemented space-efficiently by sharing information using abstract LRU-stacks. Daniel Grund, Jan Reineke 0001 |
ECRTS | 2 |
| 2010 | Resilience analysis: tightening the CRPD bound for set-associative cachesabstractIn preemptive real-time systems, scheduling analyses need - in addition to the worst-case execution time - the context-switch cost. In case of preemption, the preempted and the preempting task may interfere on the cache memory.This interference leads to additional cache misses in the preempted task. The delay due to these cache misses is referred to as the cache-related preemption delay~(CRPD), which constitutes the major part of the context-switch cost.In this paper, we present a new approach to compute tight bounds on the CRPD for LRU set-associative caches, based on analyses of both the preempted and the preempting task. Previous approaches analyzing both the preempted and the preempting task were either imprecise or unsound.As the basis of our approach we introduce the notion of resilience: The resilience of a memory block of the preempted task is the maximal number of memory accesses a preempting task could perform without causing an additional miss to this block. By computing lower bounds on the resilience of blocks and an upper bound on the number of accesses by a preempting task, one can guarantee that some blocks may not contribute to the CRPD. The CRPD analysis based on resilience considerably outperforms previous approaches. Sebastian Altmeyer, Claire Maïza, Jan Reineke 0001 |
LCTES | 3 |
| 2010 | Static Timing Analysis for Hard Real-Time Systems
Reinhard Wilhelm, Sebastian Altmeyer, Claire Maïza, Daniel Grund, Jörg Herter, Jan Reineke 0001, Björn Wachter, Stephan Wilhelm |
VMCAI | 6 |
| 2009 | Branch Target Buffers: WCET Analysis Framework and Timing PredictabilityabstractOne step in the verification of hard real-time systems is to determine upper bounds on the worst-case execution times (WCET) of tasks. To obtain tight bounds, a WCET analysis has to consider microarchitectural features like caches, branch prediction, and branch target buffers (BTB). We propose a modular WCET analysis framework for branch target buffers (BTB), which allows for easy adaptability to different BTBs. As an example, we investigate the Motorola PowerPC 56x family MPC56x, which is used in automotive and avionic systems. On a set of avionic and compiler benchmarks, our analysis improves WCET bounds on average by 13% over no BTB analysis. Capitalizing on the modularity of our framework, we explore alternative hardware designs. We propose more predictable designs, which improve obtainable WCET bounds by up to 20%, reduce analysis time considerably, and simplify the analysis. We generalize our findings and give advice concerning hardware used in real-time systems. Daniel Grund, Jan Reineke 0001, Gernot Gebhard |
RTCSA | 2 |
| 2009 | Abstract Interpretation of FIFO Replacement
Daniel Grund, Jan Reineke 0001 |
SAS | 2 |
| 2009 | Memory Hierarchies, Pipelines, and Buses for Future Architectures in Time-Critical Embedded SystemsabstractEmbedded hard real-time systems need reliable guarantees for the satisfaction of their timing constraints. Experience with the use of static timing-analysis methods and the tools based on them in the automotive and the aeronautics industries is positive. However, both the precision of the results and the efficiency of the analysis methods are highly dependent on the predictability of the execution platform. In fact, the architecture determines whether a static timing analysis is practically feasible at all and whether the most precise obtainable results are precise enough. Results contained in this paper also show that measurement-based methods still used in industry are not useful for quite commonly used complex processors. This dependence on the architectural development is of growing concern to the developers of timing-analysis tools and their customers, the developers in industry. The problem reaches a new level of severity with the advent of multicore architectures in the embedded domain. This paper describes the architectural influence on static timing analysis and gives recommendations as to profitable and unacceptable architectural features. Reinhard Wilhelm, Daniel Grund, Jan Reineke 0001, Marc Schlickling, Markus Pister 0002, Christian Ferdinand |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2008 | Relative competitive analysis of cache replacement policiesabstractCaches are commonly employed to hide the latency gap between memory and the CPU by exploiting locality in memory accesses. On today's architectures a cache miss may cost several hundred CPU cycles. Jan Reineke 0001, Daniel Grund |
LCTES | 1 |
| 2008 | Estimating the Performance of Cache Replacement PoliciesabstractCaches are commonly employed to hide the latency gap between memory and the CPU by exploiting locality in memory accesses. The cache performance strongly influences a system's overall performance, as this gap is large and ever-increasing. The efficiency of a given cache architecture - usually measured by its miss ratio - varies greatly depending on the software being executed. We present an efficient method to estimate the miss ratio using a stochastic model. The model takes into account the parameters of the cache architecture and a concise characterization of the software's locality. In contrast to previous approaches, we consider the replacement policy as an important component of the cache architecture. To this end, we introduce policy tables as a concise representation of replacement policies. The software 's locality is characterized by stack histograms or our extension thereof: History stack histograms, which refine stack histograms by distinguishing contexts of accesses. Simulation results on the SPEC benchmarks demonstrate the strong influence of the replacement policy on the miss ratio and the precision of our estimates: average absolute errors between 0.18% and 2.92%. Daniel Grund, Jan Reineke 0001 |
MEMOCODE | 2 |
| 2008 | Relative competitiveness of cache replacement policiesabstractNo abstract available. Jan Reineke 0001, Daniel Grund |
SIGMETRICS | 1 |
| 2007 | Timing predictability of cache replacement policies
Jan Reineke 0001, Daniel Grund, Christoph Berg, Reinhard Wilhelm |
Real Time Syst. | 1 |