SOURCE ARCHIVE
EXTRACTED CONTENT
102,885 charsH ART B REAKER: Deterministic Fuzzing of Multi-Hart RISC-V CPUs with Non-Deterministic Programs
Quentin Bordier Tobias Kovats Flavien Solt Kaveh Razavi ETH Zurich ETH Zurich UC Berkeley ETH Zurich bordierq@ethz.ch tkovats@ethz.ch flavien.solt@berkeley.edu kaveh@ethz.ch
Abstract—Hardware bugs threaten the correctness and se- input, which is non-trivial to derive. Efforts to automate this curity of modern CPUs. Relying on a deterministic correct translation exist [24] but cannot yet handle complex CPUs baseline, pre-silicon fuzzing has proven to be an effective strategy with speculative execution or caches. Architectural test cases for discovering deviations from correct behavior (i.e., bugs) in single-core CPUs. Modern CPUs, however, often feature multiple address this scalability challenge by generating small multi- cores with complex interconnects that implement communication hart programs. For example, litmus tests [21] evaluate partic- channels such as inter-processor interrupts or shared memory. ular memory consistency scenarios with two major limitations. Is it possible to effectively fuzz multicore CPUs despite their First, memory consistency is not the only source of bugs in inherent non-deterministic operations? multi-hart CPUs [40]. Second, litmus tests execute under a We make a key observation that multi-hart interactions fixed microarchitectural state, limiting their ability to discover may result in non-deterministic data flows, control flows, or combinations thereof. An efficient fuzzing campaign needs to bugs occurring in complex scenarios such as orderings affected manage this non-determinism without limiting the exploration by specific out-of-order execution conditions. CPU fuzzers of the possible state space that may lead to bugs. Our new have recently gained momentum [5], [17], [26], [39], [43], multi-hart RISC-V fuzzer, called HARTBREAKER, achieves this [50], but they are all limited to single-threaded execution and with a judicious use of three determinism anchors: control- and extending them to multi-hart execution is non-trivial due to data-flow anchors enable non-deterministic control- and data- flow interactions between harts while ensuring a correct execution the inherent non-determinism. of multi-hart test programs, achieving high testing throughput Determinism anchors. We classify the non-determinism and simplified bug detection. Synchronization anchors bound the non-deterministic window across harts, enabling HARTBREAKER in multi-hart execution into data- and control-flow non- to detect bugs that do not contaminate the control flow. We determinism, affecting the predictability of data values (e.g., test HARTBREAKER on five multi-hart designs, namely Rocket, load reordering) or control transfers (e.g., interrupts), respec- BOOM, Toooba, NaxRiscv and XiangShan. HARTBREAKER tively. We introduce determinism anchors to manage these two discovers five new concurrency bugs in these designs. classes of non-determinism while fuzzing multi-hart CPUs. I. INTRODUCTION A determinism anchor is a mechanism that enables non- Hardware support for multi-threaded execution is a key deterministic behavior at instruction granularity, while guar- feature of modern general-purpose processors to improve anteeing program-level determinism. Data-flow determinism performance. Similar to other general-purpose architectures, anchors ensure that non-deterministic data values are cleared RISC-V achieves this with parallel execution units that are before they affect the control flow. Control-flow determinism referred to as harts (i.e., hardware threads). Harts execute anchors ensure that non-deterministic control flow decisions independently and feature communication channels such as return to deterministic targets before proceeding with the rest shared memory and interrupts. Implementing these commu- of execution. nication channels is complex and error-prone, yet we cur- Verifying correct behavior under non-determinism. To rently lack generic and scalable approaches for systematically build these determinism anchors, we must understand what is testing these implementations under diverse microarchitectural a legal outcome of non-determinism (e.g., what reorderings conditions. This paper introduces HARTBREAKER, a RISC-V are allowed): the anchors must restore legal outcomes of multi-hart fuzzer that addresses the challenges inherent to non- non-determinism to a known state, but not illegal ones. For determinism when generating multi-hart test programs and example, an incorrect reordering of loads resulting in a wrong detecting when they trigger a concurrency bug in the CPU. data value should not just be overwritten by a data-flow anchor, HARTBREAKER has discovered five new concurrency bugs in otherwise the bug would never be detected. Effective test four multi-hart RISC-V CPUs. programs, however, can be long [39] and the calculation of Testing multi-hart CPUs. Two general approaches have been legal outcomes scales exponentially with program length. To adopted for testing multi-hart CPUs. Formal methods ex- address this challenge, we propose to parition complex multi- haustively explore all possible microarchitectural states where hart test programs into (smaller) litmus tests and use estab- memory consistency bugs may occur [33], [35], [42]; however, lished techniques [15], [37] to calculate the legal outcomes such methods use an abstracted model of the hardware as an within each partition. To scope the non-deterministic state
1
to each partition, we rely on synchronization anchors when TABLE I: Store buffer litmus test.
moving from one partition to another. x = 0, y = 0
HARTBREAKER. Armed with determinism anchors, we build P0 P1
H ARTBREAKER , a multi-hart RISC-V CPU fuzzer that com- (1) x ← 1 (3) y ← 1
bines the microarchitectural complexity of fuzzing while han- (2) x1 ← y (4) x2 ← x
dling non-determinism introduced by multi-hart execution.
The test programs generated by HARTBREAKER randomly Hart 0 Global Memory Order Hart 1
exert non-determinism within and across harts in multi-hart W addr1 R addr2 W addr0
CPUs. Asynchronous inter- and intra-hart interrupts exert non- R addr2 W addr0 W addr1
deterministic control flows. Similarly, asynchronous inter- and W addr3 W addr1 R addr1
intra-hart load and store operations to exclusive or shared W addr3 * R addr1 W addr1
memory regions exert non-deterministic data flows. Such non- W addr3 W addr3 W addr3
deterministic data and control flows are also exerted simul- W addr3 W addr3 R addr2
taneously, e.g., when writing into another hart’s instruction R addr4 W addr1 W addr4
stream. These inter-hart interactions make the execution of a W addr4 W addr3 R addr5
HARTBREAKER test program non-deterministic at instruction R addr5 W addr3 W addr5
granularity. However, by construction, the programs determin- *Preserve Program Order Rule 1
istically complete on a correctly-implemented multi-hart CPU Fig. 1: RVWMO model overview. The hart columns represent
after executing all instructions they are composed of. the memory operations in order, from the point of view of
We tested HARTBREAKER on five multi-hart RISC-V the harts. The column at the center shows one possible global CPUs: Rocket, BOOM, Toooba, NaxRiscv and XiangShan. memory ordering. HARTBREAKER reveals five previously-unknown, inherently concurrent bugs, involving cases such as illegal memory reorderings and mishandling of state when receiving interrupts These relaxations over the SC model must be accounted for across harts. by concurrent software, and by hardware implementations. Contributions. We make the following contributions: Litmus tests. Litmus tests are small concurrent programs that • We introduce determinism anchors, a novel technique that illustrate the behaviors allowed or forbidden by a memory enables instruction-level non-determinism while main- model. For example, Table I shows a litmus test that demon- taining program-level determinism. strates the behavior of store buffering in a dual-hart system • Leveraging determinism anchors, we design and im- (P 0 plement HARTBREAKER, a multi-hart CPU fuzzer that & P 1). The outcome x1 = 0, x2 = 0 is forbidden systematically generates test cases exercising all types of by SC, as it would imply that both loads (2) and (4) were multicore communication patterns. performed before the stores (1) and (3). Note that unlike SC, the RISC-V Weak Memory Ordering (RVWMO) model allows • We evaluate HARTBREAKER on five well-tested open- this behavior. In the RVWMO, stores (1) and (3) may be source RISC-V CPUs and discover five previously- committed to local store buffers, then when loads (2) and (4) unknown concurrency bugs. execute, they might not yet observe the other hart’s buffered Open sourcing. HARTBREAKER, along with a user-friendly store, potentially returning the initial value 0 for both loads. setup and extensive documentation, is readily available at https://github.com/comsec-group/hartbreaker. B. RISC-V Multi-Hart Features II. BACKGROUND RISC-V is a free and open ISA, popular in both academia We provide background on memory consistency, RISC-V and industry. It consists of a base ISA, and a set of optional ex- multi-hart features, and hardware fuzzers. tensions that add more advanced or specialized functionalities A. Memory Consistency like floating-point or atomic instructions. In RISC-V, a hart (hardware thread) is an execution unit that can independently Consistency models. In multi-hart CPUs, load and store fetch and execute instructions. Inter-hart communication in operations from different harts access the same global memory RISC-V primarily occurs through shared memory and Inter- space. A Memory Consistency Model (MCM) puts order- Processor Interrupts (IPIs). ing constraints on memory operations to ensure predictable Shared memory. RISC-V relies on the RVWMO for memory concurrent behavior. For example, Sequential Consistency consistency, introduced earlier. RVWMO builds upon the load (SC) [32] enforces in-order execution of memory operations: value axiom which specifies the value that a load may return, a load must return the value from the most recent store defined through 13 Preserved Program Order (PPO) rules. committed in the whole system. In contrast, Weak Memory For instance, the first PPO rule forbids the reordering of two Models (WMMs) allow memory operations from one hart consecutive stores to the same address as shown in Figure 1. to be observed in a different order by other harts (to ac- Other rules preserve data and control dependencies, or enforce commodate microarchitectural mechanisms like store buffers). synchronization through fence instructions. We include an
2
Program Order
exhaustive list of all PPO rules, as well as the 2 other axioms TABLE II: Instruction coverage comparison between litmus
in the RISC-V manual, page 93 [8]. tests and Cascade.
Inter-processor interrupts. An interrupt is an asynchronous Test Type Litmus test [21] Cascade [39]
event typically generated by an external source such as a Shared Memory ✓
different hart or a peripheral. The interrupt requests the (re- Atomics ✓
ceiving) hart to suspend its current program execution and Fences ✓ ✓
transfer control to a designated interrupt handler. An IPI is a Interrupts
special interrupt triggered by software running in another hart, Inter Processor Interrupts
Exceptions ✓
setting the MSIP bit of the mip Control and Status Register Independent Memory ✓
(CSR) of the target hart to 1. IPIs are generally sent through Branches ✓ ✓
a memory-mapped peripheral, usually the RISC-V-specified ALU operations ✓ ✓
FPU operations ✓
Core Local INTerrupt controller (CLINT). Since RISC-V does Privilege switches ✓
not specify a delay in which an interrupt must be evaluated or
even liveness, the time between when an interrupt is sent and TABLE III: Comparison of fuzzing tools verification strate-
when it is evaluated is non-deterministic. gies. Tools marked with † means that the CHERI version [3],
C. Hardware Fuzzers [4] is also supported. Custom methods are methods proprietary
to the fuzzer, such as undisclosed golden models or differential
Hardware fuzzers [5], [7], [17], [23], [26], [31], [39], [41], testing with another CPU
[43], [46], [47], [50] generate randomized test cases to evaluate
the correctness of a design dynamically. These test cases Fuzzer name Spike [10] Sail [9] Whisper [13] Custom
are executed on the target design, and typically validated DifuzzRTL [26] ✓
against a reference implementation. While hardware fuzzing Cascade [39] ✓
has proven to be an effective strategy for finding RISC-V Trippel et al. [43] ✓
CPU bugs in single-hart settings, it so far remained unclear TestRIG [5] ✓† ✓†
how the inherent non-determinism of multi-hart systems can ProcessorFuzz [17] ✓
be effectively tackled. INSTILLER [50] ✓
TheHuzz [44] ✓
III. O BSERVATIONS AND CHALLENGES MorFuzz [48] ✓
RISCVuzz [41] ✓
We first quantitatively analyze existing single- and multi- RISCV-DV [7] ✓ ✓ ✓
hart testing approaches to expose the gap for effectively testing multi-hart CPUs. We then discuss the high-level design of HARTBREAKER to address this gap and introduce the question: can techniques from single-hart fuzzing be applied challenges that such a design introduces. to multi-hart systems? A. Testing Multi-Hart CPUs Methodology. We analyze the instruction diversity of all 5000 litmus tests from the non-mixed-size (same size memory We analyze existing single- and multi-hart testing methods accesses) RISC-V suite [21] and 1000 programs generated by on two aspects. First, previous work [20], [40] has shown Cascade [39], a state-of-the-art CPU fuzzer. that CPU bugs often appear under specific microarchitectural Results. Table II compares the capabilities of both tools, conditions, hence we are interested in the ability of testing and confirms that litmus tests have very restricted capabilities techniques to effectively explore the microarchitectural state compared to fuzzers. Litmus tests cannot generate exceptions, space. Second, we consider the expandability of existing floating point operations or privilege switches and only support single-hart testing techniques to multi-hart systems. a small subset of the instructions available in the other Litmus tests. Litmus tests highlight specific aspects of mem- exercised categories. This low instruction diversity implies that ory consistency models in multi-hart settings [14], [21]. They litmus tests are unlikely to trigger MCM violations associated focus on clearly expressing subtle tolerated and non-tolerated with very specific microarchitectural conditions as they fail non-deterministic interaction patterns. Due to their focus on to effectively explore the microarchitectural state space. To testing specific memory consistency scenarios, we raise the validate this hypothesis, we ran 1,314 bare-metal litmus tests question: is the distribution of instructions in litmus tests di- from the PULP group [6] and CHERI project [2] repositories verse enough to trigger complex microarchitectural scenarios? on all CPU designs in our study. These tests did not trigger any Hardware fuzzers. Conversely, state-of-the-art CPU of the bugs identified by HARTBREAKER since these bugs, as fuzzers [5], [17], [26], [39], [43], [48] can generate complex discussed in Section VII-E, require specific microarchitectural instruction streams with balanced instruction distributions, conditions that are not exercised by these tests. allowing them to reach arbitrary microarchitectural states. Cascade [39], a hardware fuzzer, on the other hand, gen- However, they are designed for single-hart scenarios and erates programs with more balanced instruction distributions, rely on deterministic program execution, raising another exercising the microarchitecture in diverse conditions. Hard-
3
ware fuzzers like Cascade, however, rely on deterministic
program execution for verification via differential testing using
either an instruction set simulator (ISS) or a reference hart,
as summarized by the evaluation of popular fuzzers shown Test case Simulation Timeout Memory trace
in Table III. Hence, current RTL fuzzers cannot verify non- generation detection validation
deterministic program execution which fundamentally limits Store bug-
their application to multi-hart CPUs where the execution is triggering
inherently non-deterministic. test case
B. HARTBREAKER Design Fig. 2: Overview of HARTBREAKER’s pipeline.
Ideally, we need a fuzzer that can exercise multi-hart interactions under diverse microarchitectural conditions which is currently missing. HARTBREAKER fills this gap by gen- non-determinism in multi-hart settings. This introduces our erating multi-hart test cases with high instruction diversity first challenge. and throughput while triggering non-deterministic behavior in multi-hart settings. Before diving into the challenges specific Challenge 1. Determine the root causes of non- to HARTBREAKER, we present our initial design decisions. determinism in multi-hart programs. Fuzzers, in general, are attractive testing tools due to their good performance in terms of instruction throughput. Insights from In Section IV, we analyze the sources and effects of non- previous work [7], [39] show that to maximize throughput, deterministic execution in multi-hart settings. We observe that every generated instruction should be executed. As such, the non-determinism can fundamentally only manifest in three generated test cases need a known execution path, from a ways: (1) control flow non-determinism, (2) data flow non- predetermined start to a predetermined end state. This test determinism, and combinations thereof. program construction strategy allows a straightforward detec- Given these observations of non-deterministic behaviors, tion of the occurrence of functional bugs that contaminate the we implement HARTBREAKER based on the design in Fig- control flow, revealed by deviations from the expected final state. ure 2. The next challenge concerns the first step of HART- Limiting dead code. Non-deterministic programs can be BREAKER: the efficient generation of test cases that exhibit modeled using non-deterministic finite automata, where each non-deterministic behavior, while allowing for high instruction executed instruction corresponds to a state transition. A de- diversity and throughput. terministic instruction has exactly one successor state, while Challenge 2. Efficiently generate effective non- a non-deterministic instruction can lead to multiple possible deterministic test cases. successor states. Each non-deterministic instruction therefore introduces multiple possible transitions, increasing the number of possible execution paths. As a result, the number of In Section V, we present the core of HARTBREAKER: reachable accepting states might grow exponentially with the control and data flow anchors. They bound non-deterministic number of non-deterministic instructions. One could, in princi- effects within selected program regions, prohibiting their prop- ple, enumerate the legal accepting states at test-generation time agation into control flow decisions. Within these regions, there and accept any of them at runtime. However, deciding whether is no restriction on the non-determinism that may occur during an observed trace is consistent with the memory consistency execution. As such, all possible behaviors can be observed model, i.e., the testing problem, is NP-complete [18], and while avoiding path explosion. Given efficient mechanisms to therefore intractable for programs of fuzzing-relevant length. generate effective multi-hart test cases, HARTBREAKER then Yet in a single instance of a program execution, only one path needs to verify that the observed program executions are valid. is taken, leading to an exponential amount of dead code in the This is our final challenge which addresses detecting bug- program. To avoid this path explosion problem resulting in triggering programs in the design of HARTBREAKER depicted prohibitive amounts of dead code, and thus low performance, in Figure 2. we will introduce techniques for generating programs with a well-defined accepting state. Challenge 3. Enable efficient verification of non- C. Overview of Challenges deterministic test cases. HARTBREAKER thus opts for generating random programs In Section VI, we introduce synchronization anchors. that exercise unconstrained non-determinism in bounded re- Synchronization anchors allow efficient verification of non- gions, but enforces that those regions return to a deterministic deterministic programs by periodically resetting parts of the state before exiting, thus connecting many non-deterministic architectural state that must be verified post-simulation. This regions using a deterministic path. To generate such programs, effectively bounds non-determinism in a controllable manner we must first understand the core mechanisms that introduce to avoid state explosion.
4
1 la x4, 0x80001000 1 # Load address in x4 and counter P C(s). The environmental state e is the remaining 2 li x5, 0x80000000 2 # jump to it architectural and microarchitectural components, including the 3 sw x5, 0(x4) 3 la x4, 0x80001000 CSR registers C(e) and the hart’s view of memory M (e). Let 45 addi x5, x5, 1 4 lw x5, 0(x4) S be the set of all possible observable states, E the set of all sw x5, 0(x4) 5 jalr x0, x5 environmental states, and I the set of all executable instruc- (a) Hart 0 instructions. (b) Hart 1 instructions. tions of a hart. Ereach(s) ⊆ E is the set of environmental Fig. 3: Example of data-flow non-determinism in multi-hart states reachable when the observable state is s. Informally, programs. Ereach(s) is the set of environmental states consistent with a valid execution history leading to s. We define the transition relation of the hart as a set of triples 1 # send an IPI to 1 add x2, x4, x8 δ ⊆ (S × E) × I × (S × E). A triple ((s, e), i, (s′, e′)) ∈ 2 # hart 1 2 sub x8, x3, x4 δ captures the transition from one architecturally committed 3 la x4, CLINT_BASE 3 final: 4 li x5, 1 4 csrr x2, MIP state (s, e) where s is fully determined even if e is not, to the 5 sw x5, 4(x4) 5 beq zero, x2, final next committed state (s′, e′) upon retirement of i, abstracting (a) Hart 0 instructions. (b) Hart 1 instructions. away all intermediate pipeline behavior. For ease of notation, we denote triples ((s, e), i, (s′, e′)) ∈ δ as transitions (s, e) → −i Fig. 4: Example of control-flow non-determinism in multi-hart (s′, e′). programs. Instruction-level non-determinism. An instruction i is IV. PROFILING MULTI-HART NON-DETERMINISM non-deterministic in the observable state s if there exist We formalize the sources of non-determinism in multi- distinct e0, e1 ∈ Ereach(s) and s′0, s′1 ∈ S such that (s, e0) →i − (s′ , e′ ), (s, e ) → hart systems. We then present a strategy for generating non- 0 0 1 −i (s′1, e′1) and s′0 = s′1. deterministic test cases that can be validated against a deter- Instruction-level non-determinism originates when execut- ministic model. ing an instruction i from a given observable state s may A. Root Causes of Non-determinism lead to multiple possible observable states s′, depending on To understand non-determinism in multi-hart programs, we the (unobservable) environmental state e, which captures the distinguish the root causes that lead to non-determinism. Data- sources of non-determinism such as memory interleavings, flow non-determinism occurs when concurrent interactions CSR values, or interrupt timing. This instruction-centric view produce non-deterministic values in registers or memory, while allows us to formally define control-flow and data-flow non- control-flow non-determinism occurs when inter-hart events determinism. affect the execution path. Both can produce similar observable Control-flow non-determinism occurs when different envi- effects, but require different handling strategies. ronmental states cause execution to diverge at an instruction Consider the code in Figure 3 executed on two different that is not itself the source of non-determinism. For example, harts. The value in x5 in hart 1 at the end of the execution when an interrupt arrives during an otherwise deterministic is non-deterministic. It may hold the value 0x80000000, instruction (see Figure 4b). 0x0, or 0x80000001, depending on the interleaving of the instructions, due to the absence of synchronization primitives. Control-flow non-determinism. Instruction i induces This is an example of data-flow non-determinism. control-flow non-determinism in the observable state s if In Figure 4, since there is no synchronization, hart 1 receives there exist e0, e1 ∈ Ereach(s) and sc0, sc1 ∈ S such that −i (sc0, e′ ), (s, e ) → the interrupt at an unknown location, causing a trap. Hart 1 (s, e0) → 0 1 −i (sc1, e′1), and P C(sc0) = could trap on any of the four lines of the program, leaving P C(sc1). the subsequent state of the system undetermined. This is an example of control-flow non-determinism. Data-flow non-determinism occurs when different environ- The following section formalizes both forms of non- mental states cause an instruction to produce different register determinism, allowing us to reason about both their individual values for the same observable state. For example, when a and conjunctive effects. load returns different values depending on the interleaving of B. Formalizing Non-determinism concurrent stores from another hart (see Figure 3b). We reason about non-determinism either on an instruction Data-flow non-determinism. Instruction i induces data- level (Section IV-B1) or on a program level (Section IV-B2). flow non-determinism in observable state s if there exist 1) Instruction-level non-determinism: We define a hart’s e , e1 ∈ Ereach(s) and sd0, sd1 ∈ S such that architectural state and its instruction-level transition relation. 0 (s, e0) → −i (sd0, e′ ), (s, e → States and transitions. We call s the observable state of a R(sd1). 0 1) −i (sd1, e′1), and R(sd0) = hart, including its general-purpose registers R(s) and program
5
Control and data-flow non-determinism can also occur si-
multaneously: control-flow non-determinism can induce data- sending send IPI
flow non-determinism, and vice versa. For example, consider a core
scenario where a program uses virtual addresses, and has just recieving confined landing zone
changed address space. If the Translation Lookaside Buffer core check MIP
(TLB) is not flushed, a subsequent load might either cause ΔPC time
a trap if the buffered virtual address is invalid, or load a
(non-deterministic) value and continue otherwise. As such, the Fig. 5: Interrupt transmission diagram. The sender sends an
load introduces both data- and control-flow non-determinism interrupt, which the receiver evaluates within a bounded, yet
simultaneously. non-deterministic number of cycles ∆P C. A branch at the
- Program-level non-determinism: We define a program tail of the confined landing zone evaluates the MIP register. P as a directed graph G whose nodes and edges are architec- Unless the interrupt has been processed, execution resumes at tural states and their transitions, respectively, expressed by δ the head of the landing zone. (see Section IV-B1). Let ϕ : S → {true, false} be a termina- tion predicate that determines when the execution halts. An The anchors do not impose restrictions on the non- execution Exec(P ) of a program P is the traversal of G from deterministic instructions. Instead, they allow the non- an initial state si until the first state sf for which ϕ(sf ) = true, determinism to occur naturally but ensure that its effects do called the final state of the execution. For a single program, not propagate beyond predetermined boundaries. there may be multiple valid executions resulting in different final states depending on non-deterministic behavior. V. GENERATING EFFECTIVE MULTI-HART PROGRAMS In the following, we present two core techniques for exerting Program-level non-determinism. A program P is said instruction-level non-determinism while preserving program- to be program-level non-deterministic if there exist two level determinism in multi-hart systems: control and data-flow executions Exec(P ) and Exec’(P ) with distinct final states anchors. sf = s′f . A. Control-Flow Anchors Conversely, a program is program-level deterministic if all Control-flow anchors (in short, cf-anchors) handle non- executions, regardless of the path taken through G, reach the deterministic control-flow variations that may arise from same final state sf . A program can be non-deterministic at the asynchronous events such as inter-processor interrupts (IPIs). instruction level, but deterministic on program level. Assume, Control-flow non-determinism can involve two harts that must for example, that a program is exposed to data-flow-, but not to be synchronized: aa sender, which triggers the event, and control-flow non-determinism. The program never conditions receiver, which observes the resulting non-determinism. its control flow on the non-deterministic data and overwrites Figure 5 shows the outline of the cf-anchor mechanism. all registers with fixed values just before terminating. The pro- Implementation. The set of instructions A that defines the gram is then instruction-level non-deterministic, but remains cf-anchor is composed as follows. The receiver executes an program-level deterministic. instruction that prepares the target address of the trap handler along with a subsequent store to an address shared with the
C. Determinism Anchors sending hart. This sequence signals the sender that the receiver
has entered the confined landing zone. Once the sending hart
Determinism anchors enable the generation of program- observes that the receiving hart has entered the landing zone, level deterministic test cases in the presence of control- it may initiate the interrupt by executing the respective non- or data-flow non-determinism at an instruction level. A deterministic instruction i. At initiation of the interrupt by the determinism anchor bounds a region of potentially non- sender, the receiver traps some (non-deterministic number of) deterministic instructions and provides a sequence that restores cycles later, resulting in control-flow non-determinism (i.e., a unique observable state. Let Π(i, s) = { s′ ∈ S | ∃e ∈ P C(sc0) = P C(sc1)). An interrupt handler subsequently Ereach(s), e′. (s, e) → −i (s′, e′) } be the set of the observable marks the interrupt as processed and returns execution to the states reachable by executing the non-deterministic instruction next instruction in the landing zone. The receiving hart may i in the observable state s. now exit the landing zone when executing the concluding branch at its boundary. Within the landing zone, the receiving Determinism Anchors. A sequence of instructions A = hart performs random computations that regenerate the same (i1, . . . , in) is a determinism anchor for i at s if, for every data throughout an arbitrary number of iterations. Therefore, s′ ∈ Π(i, s) and every e ∈ Ereach(s′), executing A from independent of the (valid) arrival time of the interrupt, the (s′, e) yields the same observable state; that is, there exists architectural state remains identical upon the exit from the a unique sd ∈ S such that all such executions terminate in confined zone. (sd, ·). Preserving bug detection capabilities. Because of the archi- tectural invariance after the execution of confined landing zone
6
with respect to the arrival time of the interrupt, we can exploit Generation Simulation Validation
program-level determinism for bug detection. As explained
in Section II-C, prior work [7], [39] exploits the fact that Collect PPO Collect load Generate litmus
hardware bugs invalidate the data flow, which subsequently edges and return values test and
breaks the control flow when executing a valid program stored values Verify existence
on faulty hardware. An architectural bug that occurs during
interrupt handling thus breaks the architectural invariance upon Fig. 6: MCM load return value computation flow.
exiting from the landing zone. The invalid data can therefore
propagate into the control flow and cause the hart to jump gather the data returned by all loads, and validate the observed
into arbitrary memory regions, causing a hang and eventually execution using a memory consistency solver presented in
timing out which HARTBREAKER detects. Section VI.
B. Data-Flow Anchors VI. DETECTING BUGS IN NON- DETERMINISTIC
Data-flow anchors (in short, df-anchors) prevent non- EXECUTION
deterministic data from contaminating control-flow decisions,
while maintaining instruction-level data variability to expose Having established mechanisms to maintain program-level
hardware memory-consistency bugs. They isolate and reset determinism, we now address the third and last challenge:
ambiguous data values only, hence have minimal impact on verifying the execution of non-deterministic programs. The
the overall program structure. verification of control- and data-flow non-determinism requires
Implementation. Contrary to control-flow non-determinism, orthogonal approaches.
data-flow non-determinism does not rely on a timely sender- Control-flow non-determinism. Control-flow non-
receiver setting. A hart can issue load and store operation determinism is bounded within the landing zones. However, with no synchronization without affecting the control-flow, and resulting faulty computations may leak into the data flow. As thus the validity of programs. Hence, exerting data-flow non- such, invalid forms of control-flow non-determinism likely determinism does not require any cross-hart synchronization. break program-level validity, resulting in trivially detectable Executing the respective instruction ind that initiates non- timeouts during RTL simulation. determinism has no preconditions and can execute from any Data-flow non-determinism. However, df-anchors block data- state s. After ind’s execution, its effects become observable flow non-determinism from affecting program-level validity. and its destination register r holds an ambiguous value that is Hence, we follow an alternative approach to verify that some only determined at runtime, producing multiple possible states instance of a non-deterministic data-flow execution trace does {s′0, s′1, . . . } during program generation. not violate memory ordering rules. The following details our The register r is flagged as non-deterministic within the approach. program generation algorithm. Flagged registers are isolated: they cannot be used as explicit sources for control-flow deci- A. Validating Non-Deterministic Data Flows sions until the determinism anchor resets them to a predictable We verify the realized ordering of memory operations ob- state. In this case, the set of instructions A corresponding to served during execution against the RVWMO model. Figure 6 the df-anchor contains only a single instruction that restores provides an overview of our approach. In the first two steps, determinism by overwriting r with a predictable value, either we extract relevant properties from the generated test case by assigning zero to r or by using it as a destination for an and its execution trace to construct an equivalent litmus operation with a deterministic output. test. Subsequently, we generate the minimal litmus test and This restoration step is local to the hart and requires no inter- leverage it for verification accordingly. A key insight is that we hart synchronization. We apply this method to the registers can construct an equivalent litmus test from any generated test used as output registers for load operations, and to the mepc case following this method, allowing us to leverage existing CSR register after an interrupt has been received. high-performance verification tools [14], [37] in the backend Preserving bug detection capabilities. Resetting registers of HARTBREAKER. does not imply breaking the syntactic dependencies that de- Transforming programs into litmus tests. Existing weak- termine re-ordering of memory operations. Instead, we can memory model analysis tools [14], [37] input litmus tests that enable arbitrary dependencies by zeroing out registers using express some instance of memory orderings. To leverage these instructions such as xor or sub. Such operations neutralize tools, the derived litmus test must preserve equivalency in the dependency carrier, while maintaining the syntactic de- terms of the RVWMO model (as formally specified in [8]) pendency relations. This allows safe usage of the registers to with respect to the original test case. However, litmus tests create dependencies. support only a restricted set of instructions, preventing direct Because non-deterministic data is isolated and the set of translation of our complex test cases into litmus assembly. behaviors is unconstrained, we can observe and verify the All properties relevant to the verification of the litmus test, outcomes of a test case from the execution traces obtained dur- with the exception of syntactic dependencies, are fully defined ing simulation. HARTBREAKER isolates memory operations, by the memory operations alone. By expressing syntactic
7
syntactic address dependency
x1 = addr2; x4 = addr1 dependent registers operations. First, they synchronize the cores, such that each
section of a test case has a single corresponding section in
1 lw x2, 0(x4) x2 = *addr1 all harts. Second, they fence loads and stores between these
2 xor x2, x2, x2 x2 = 0 sections to ensure the re-orderings remain local within the
respective sections. Contrary to control- and data-flow an-
3 or x1, x2, x1 x1 = addr2, x2=0 chors that ensure program-level determinism, synchronization
4 sw x5, 0(x1) x1 = addr2, x2=0 anchors reset non-determinism to keep verification tractable.
Fig. 7: Example of the method we use to create arbitrairy syn- VII. EVALUATION
tactic address dependencies between two memory operations. We evaluate HARTBREAKER by first investigating whether
In step 1 , x2 picks up a dependency on the load. In step 2 the generated test programs can sufficiently exercise multi-hart , x2 is zeroed but the dependency survives. In step 3 , the communication channels in Section VII-A. We then evaluate dependency is transferred from x2 onto x1. Finally, in step 4 the fuzzing performance of HARTBREAKER, with respect , the store reads x1, giving its address a syntactic dependency to its instruction throughput in Section VII-B and achieved on the load. coverage when compared with the industry standard RISCV- DV [7] in Section VII-C. We finally look at the concurrency bugs that HARTBREAKER has discovered in Section VII-D. dependencies using the method introduced in Figure 7, we Testbed and targets. The evaluation is performed on a can fully express the RVWMO relations in a litmus test, machine equipped with two AMD EPYC 7H12 processors at guaranteeing equivalency with respect to the original program. 2.6 GHz containing 256 logical cores and 1 TB of DRAM. Given this insight, we exploit three key properties to We use Verilator [12] to simulate designs, and Spike [10] concretely translate arbitrary HARTBREAKER programs into as a golden model. We adapt the Verilator version based equivalent litmus tests. First, data-flow anchors ensure deter- on the design’s requirements if necessary. The experiments ministic data flows with respect to store operations, allowing involving RISCV-DV [7] were run using the UVM framework us to obtain store values from a deterministic ISS. Second, the with a commercial simulator. We tested HARTBREAKER on test cases statically define all syntactic dependencies between Rocket [16], a simple, in-order CPU, and four out-of-order, memory operations, which we can extract during generation. superscalar CPUs: BOOM [51], Toooba [1], NaxRiscv [11] Third, the traces reveal the concrete load return values, which and XiangShan [49]. we gather after simulation. We thus iterate through all memory operations of a test A. Multi-Hart Feature Coverage case as follows. Because we already know the store values, To evaluate how well HARTB we generate each store with an associated instruction that REAKER can exercise multi- ensures the store instruction in the litmus test commits the hart functionalities, we analyze 10’000 generated test pro- same value as the original program to memory. Furthermore, grams. We use a default set of parameters that allow a rea- when an instruction initiates a syntactic dependency, we carry sonable number of shared memory operations and interrupts, the dependency in a temporary register. We then zero out the while leaving space for other instructions for maximizing the temporary register, while keeping the dependency active, as exploration of microarchitectural states. in step 2 in Figure 7. And for each instruction that has a Interrupts. We first test the interrupt capabilities of HART- dependency to a previous instruction, we transmit the depen- BREAKER. We look for a high frequency of interrupts such dency, mirroring step 3 of Figure 7 to propagate the respective that we put the subsystems under stress. We found that relation. This way, the solver observes relations between the interrupts are used in 100% of the generated test cases, with memory operations in the litmus test that are identical to an average of 12.1 IPIs per test case, each consisting of 1600 the memory operations of the original test case. Finally, we instructions on average. construct an exists statement using the load return values Shared memory. We further investigate the PPO rule cover- for the verification by the solver in the HARTBREAKER’s age to ensure we can detect all possible forbidden re-orderings. backend to check if this outcome exists given the memory Since the bugs we aim to discover are violations of these rules, consistency model. it is also critical to cover all of them to avoid masking bugs. B. Synchronization Anchors We plot the probability that a memory instruction is subject to a given rule in Figure 8. We observe that all rules are To ensure that the complexity of validating the data flow covered, meaning we can discover bugs related to all rules. of test cases remains bounded, we must control the number Notice that PPO rule number 8 is not included in the plot. This of memory operations the solver must process. Instead of rule enforces the ordering of load-reserve (LR) with respect bounding the number of instructions in a test case, we bound to its paired store-conditional (SC). LR/SC ordering could be the number of instructions that can be re-ordered, allowing us treated as standard loads and stores, with the MCM solver to verify large test cases in smaller sections. To reset the state verifying their ordering. We exclude them by choice, as the of the shared memory, synchronization anchors perform two ISA permits spurious SC failures, making it impossible to
8
0.4 600.0 Verification
Disabled
0.2 400.0 Enabled
0.0 200.0
1 2 3 4 5 6 7 9 10 11 12 13
PPO Rules 0.0
Fig. 8: Probability that a memory instruction exercises a given 1k 2k 4k 8k
PPO rule. The x axis is the index of a PPO rule as defined in Program Size (instructions)
the RISC-V manual [8]. Fig. 10: HARTBREAKER instruction throughput of the triple-
hart Rocket CPU with verification enabled and disabled.
0.2
NaxRiscv Boom XiangShan
0.1 Toooba Rocket
60
0.0 0 5 10 15 20 25 40
Memory Operations Distance (instructions) 20
Fig. 9: Distance between memory operations accessing shared 0
memory. 1k 2k 4k 8k
Program Size (instruction)
distinguish legal behavior from liveness bugs without design- Fig. 11: HARTBREAKER instruction throughput for each sup-
specific knowledge. ported CPU, across program sizes. Each CPU uses three harts.
An additional important factor in exercising the underlying
memory consistency implementations is memory operation
frequency since CPUs have a bounded re-ordering window Figure 11 shows the end-to-end instruction throughput with
depending on the size of hardware structures such as store verification enabled across all supported CPUs, for different
buffers and queues. Because we want to maximize the amount program sizes. With the exception of NaxRiscv, we observe
of re-orderings of memory operations we observe, it is crucial that the throughput does in fact stay fairly constant, with only
to have a high density of memory operations such that in- a very slow increase in throughput over the program size. The
structions are not too far apart to be re-ordered. Figure 9 plots sharp increase in throughput for the NaxRiscv CPU is due
the distance between memory operations that access addresses to NaxRiscv’s simulator. All CPUs use Verilator [12] as a
used at least once by both harts in a test case. We observe a simulator, producing a compiled RTL binary with very short
good density of memory operations, with reasonable distances startup time. In contrast, NaxRiscv simulations run through
between memory operations, enabling many possibilities for Scala and bind to a Verilator binary via the Java Native
the re-ordering of memory operations. Interface, which leads to significantly longer startup times
B. Fuzzing Throughput since the simulator must be rebuilt from cached artifacts.
As a result, generating longer programs helps amortize this
We first investigate what impact the verification of the data- startup cost. Furthermore, we observe that the size of the
flow has on throughput using the triple-hart Rocket CPU CPU impacts the throughput, as larger CPUs tend to have
shown in Figure 10. We observe that without verification, much slower simulation performance, as depicted in Figure 12.
the throughput converges to a stable value for larger program XiangShan [49] takes multiple minutes to perform a single
sizes, creating an optimal program size for fuzzing. However, simulation, with larger programs increasing simulation times
verification of valid data flows is comparably slow and has even further. All CPUs we tested followed a similar trend at
a significant impact on the end-to-end throughput when con- different scales, e.g., Rocket [16] simulation time is measured
sidering both verification and simulation, resulting in a rather in seconds.
stable throughput across all program sizes. The optimal size To further understand the performance impact of each of the
is therefore a program that is as long as possible to maximize components of HARTBREAKER, we evaluate their individual
throughput, while keeping the simulation time of the program runtime contribution in Figure 13. The first step is the genera-
reasonable for detecting bugs. tion stage, where the assembly programs are generated. After
9
Probability Probability
Throughput (instr/s) Throughput (instr/s)
30 XiangShan 34
32
20 30
10 28 HartBreaker no verification
HartBreaker with verification
26 RISCV-DV
1k 2k 4k 8k 0 200 400 600 800
Instruction Count (instructions) Fuzzing Time (core hours)
Fig. 12: XiangShan simulation time in minutes. Fig. 14: Multiplexer select coverage achieved by HART-
BREAKER vs. RISCV-DV on triple-hart Boom v3. 15,872
Generation ISS MCM Verification RTL Simulation coverage points.
1.0 TABLE IV: Summary of discovered bugs.
CPU name Bug Type Bug Alias
0.5 NaxRiscv [11] Illegal Load-Load re-ordering N1
CLINT access size N2
Toooba [1] IPI evaluation timing bug T1
0.0 BOOM (v4) [51] Illegal Load-Load re-ordering B1
Rocket [16] None
XiangShan [49] Out-of-order MIP read X1
1000 2000 4000 8000
Program size (instruction) RISCV-DV uses pre-defined test scenarios, which guide
Fig. 13: Fraction of time spent in each step of the testing random programs towards specific features of a CPU. We ran
pipeline. RISCV-DV using its default multi-hart target, configured for
64-bit designs with three harts. We evaluated coverage on the
triple-hart BOOM CPU.
the generation, we run the binaries on the Spike ISS [10] to To ensure a fair comparison, we included RISCV-DV test
gather some values unknown at generation time, such as the cases that timed out (we use a five-minute timeout) in the values that the stores will commit to memory. The binary is coverage calculation, but excluded their execution time from then executed on the RTL simulator of the design under test. the core-hour count. We ran RISCV-DV and HARTBREAKER Finally, if MCM verification is enabled, we gather the values with verification for a total of 858 core-hours, and then ran returned by concurrent loads from the simulator’s commit logs, HARTBREAKER without verification until we reached similar translate the trace into a litmus test that expresses the exact coverage. Figure 14 shows that HARTBREAKER achieved behavior observed, and verify if there exists a valid execution similar coverage to RISCV-DV, while additionally provid- that returns the same values for all loads. We observe that ing multi-hart verification capabilities including IPI support, verification makes up the bulk of the runtime overhead across memory model checking, and deterministic interrupt injection all program sizes, and its share slightly increases for larger that RISCV-DV lacks. Without verification, HARTBREAKER programs. However, with verification disabled, we observe that reached the same coverage as RISCV-DV in a significantly ISS and RTL simulation have the largest remaining impact shorter time. on performance for smaller programs. For large programs, D. Discovered Bugs the bottleneck shifts to RTL simulation alone, showcasing the amortizing effects of larger programs which we have HARTBREAKER has found five bugs dealing exclusively previously observed in Figure 10. with shared memory and interrupts across the tested CPUs, summarized in Table IV. HARTBREAKER triggers some of C. Coverage Comparison these bugs within minutes, while others require very spe- cific microarchitectural conditions and only surface after sev- We compare HARTBREAKER against RISCV-DV [7], a eral core hours of fuzzing. Figure 15 displays the Time-to- widely-used random instruction generator for RISC-V verifica- Exposure (TTE) statistics for each bug accordingly, collected tion. To the best of our knowledge, RISCV-DV is the only tool over 20 fuzzing runs each. The NaxRiscv and XiangShan bugs capable of automated generation of multi-hart test programs. (N1, N2, X1) have been confirmed and fixed by the respective
10
Fraction of total time Simulation Time (min)
Coverage (%)
no-verif verif no-verif verif no-verif verif no-verif verif
TABLE V: Outcome x1=0, x2=1, x3=0 is forbidden.
50
Address x initialized to 0
P0 P1 40
(2) x1 ← x
(1) x ← 1 (3) x2 ← x 30
(4) x3 ← x
20
developers. The other bugs (B1, T1) have been reported to 10
their respective project platforms. Furthermore, the absence of 0
multi-hart bugs in Rocket is not surprising. Rocket implements
an in-order pipeline with only limited optimizations in its B1 N1 N2 T1 X1
memory subsystems. The following provides an overview of Fig. 15: Time to exposure statistics over 20 runs for each bug.
the individual bugs discovered by HARTBREAKER. NaxRiscv INT is the measurement for the NaxRiscv interrupt
Illegal load-load re-ordering (B1, N1). The B1 and N1 bugs bug, and NaxRiscv MCM for the memory consistency bug.
are very similar in nature. Both bugs violate the Coherence of
Read-Read (CoRR) ordering, a fundamental memory consis-
tency requirement. 1 1 lw s7,0(sp) # Load(x) id=0
In the example presented in Table V, the outcome (x1 = 2 # Write(x) 2 ...
0, x2 = 1, x3 = 0) implies that the second and third loads of x 3 sd s1, 0(a1) 3 lwu t1,0(s2) # Load(x) id=1
on P1 returned values written by different stores, even though 4 4 ...
5 ... 5 lwu s0,0(tp) # Load(x) id=2
there was no intervening store to x between them in program
order. Under RVWMO, this case falls under the same-address (a) Hart 0 instructions. (b) Hart 1 instructions.
load–load preserved program order (PPO) rule [8]: Fig. 16: B1 test case excerpt. Hart 0 performs a store to
If two loads to the same byte return values written an address and hart 1 concurrently reads from it with three
by different stores and no store to that byte occurs consecutive loads. The resolution of load 1’s address is delayed
between them, the first load must precede the second by complex computations, creating a race condition that results
in the global memory order (GMO). in load 2 reading a stale value.
Since the younger load (x3) observes an older value than the earlier load (x2), this PPO ordering is not preserved. As a result, the execution violates the load value axiom, which as processor to miss newly-arrived interrupts that should have we discussed in Section II, mandates that each load returns been visible, violating the expected ordering between interrupt the value of the most recent store that precedes it in both updates and their observation. program order and the GMO. Hence, the observed outcome CLINT access size restriction (N2). To send an IPI, a represents a violation of Coherence of Read–Read (CoRR): hart cannot directly modify another hart’s interrupt registers. the hart observes memory that “goes backward in time”, i.e., Instead, it must write to a memory-mapped register managed a younger load returns a value older than a previous load from by the CLINT using a regular memory store instruction. The the same address. RISC-V specification requires the CLINT to support store IPI evaluation timing bug (T1). T1 is an interrupt handling operations of any size (byte, halfword, or word). However, we bug in Toooba’s implementation of the mret instruction. The found that NaxRiscv’s CLINT implementation only accepts bug occurs when a hart has a pending interrupt while interrupts full-word stores, incorrectly raising an exception when a are currently disabled, but were previously enabled before program attempts to use a store-byte instruction. entering the trap handler. When returning from a trap using mret, the processor should restore the previous interrupt- E. Microarchitectural root cause analysis enabled state and immediately check if any interrupts are In the following, we discuss the specific microarchitectural pending. According to the RISC-V specification, if an interrupt root causes for two particularly interesting bugs discovered is pending after re-enabling interrupts, the processor must by HARTBREAKER. Notably, triggering them requires com- handle it immediately. However, Toooba incorrectly proceeds plex structural and computational dependencies, as well as to fetch the next instruction from an invalid address (stored in exercising the involved microarchitectural components. HART- the exception program counter) before checking for pending BREAKER is capable of generating such programs for the interrupts. This causes the processor to trap due to the invalid first time, revealing edge cases that could not be detected address instead of the pending interrupt, writing the wrong by existing tooling. Figure 16 and Figure 17 show simplified cause into the trap cause register. versions of the test cases, where interleaving instructions have Out-of-order MIP read (X1). XiangShan allows out-of- been removed for clarity. A complete version can be found in order reads of the interrupt pending register. This causes the the Appendix Figure 19 and Figure 18.
11
Time to Exposure (core-hours)
1 1 sd a0, 0(a1) # Write(x) times. We initially thought that the number of memory op- 2 2 ... erations between two solving steps was a limiting factor of 3 3 lb s2, 0(a1) # Load(x) id=0 our implementation, and modified our approach to translate 45 #swrite(x) 4 ... execution traces to litmus tests so we could benefit from the x2, 0(a1) 5 lbu s5, 0(a1) # Load(x) id=1 6 6 ... capacities of the state-of-the-art memory consistency solvers. 7 ... 7 lwu sp, 0(a1) # Load(x) id=2 When using Dartagnan [37], we could scale HARTBREAKER (a) Hart 0 instructions. (b) Hart 1 instructions. to about 100 memory operations between synchronization an- chors. However, we did not find any new bugs, and could only Fig. 17: N1 test case excerpt. Hart 1 is writing to an address x reproduce the ones found with our custom implementation. and subsequently reads from it using three consecutive loads This suggests that further increasing the number of memory of different widths. Hart 0 concurrently writes to that address. operations between synchronization anchors is unlikely to The last load returns a stale value. trigger more bugs since 100 memory operations already go beyond the size of most on-core data structures. Bug B1. The bug manifests when a hart stores to an address, Program reduction. The non-deterministic nature of our test and another hart has three concurrent in-flight loads, see Fig- cases presents a challenge for debugging and analysis. When ure 16. Because load 1’s address computation is delayed a test case triggers a bug, it cannot be reduced, as any (e.g., by a multi-cycle instruction), load 2 succeeds before- modifications to the instruction stream might fail to reproduce hand, ahead of load 1. Simultaneously, a concurrent store the bug, even if the test case is far from minimal. Still, even from hart 0 triggers a coherency probe. This invalidates without reduction, the memory consistency solvers used as the cache line, but no corrective action is taken on load backends offer visualization capabilities that we can use to 2, which has already succeeded. Load 1, however, returns pinpoint the incorrect instruction more easily. the newer data, as it has not yet succeeded. When the older Scaling to more harts. Our methodology uses two harts, as load’s address is unresolved, the younger load can bypass the described in the examples. We added a third hart that generates coherency check and succeed with a stale value. independent memory operations to introduce additional noise Bug N1. This bug involves a same-hart store followed by three into the system. We evaluated both configurations: the third loads to the same address, while another hart concurrently hart yielded modest coverage improvement but did not uncover stores to that address, see Figure 17. A size mismatch between additional bugs. Scaling program generation beyond two harts the same-hart store and the subsequent loads on hart 1 would require engineering effort to extend the barrier’s lock prevents store-to-load forwarding, forcing the loads to wait mechanism. until the store’s entry is freed from the store queue. Intervening Size of re-ordering windows. The upper bound on the number instructions between the loads spread their dispatch across of instructions between synchronization anchors is set by multiple cycles, such that the store queue entry is freed after the capabilities of the backend we use. The bugs are not load 0 and load 1 check for pending stores but before very sensitive to the window size; we discovered them with load 2. Load 0 and load 1 are therefore scheduled to windows ranging from 10 to 100 memory operations. Larger replay, while load 2 is marked as succeeded and has no windows may become relevant in future CPUs that may adopt more replay path. Before load 1 replays, the store on hart wider store buffers and other memory-related optimizations. 0 becomes available and sends a probe to invalidate the cache IX. RELATED WORK line. When load 1 then replays, it will use the updated cache line. However, the load-store unit provides no mechanism to Hardware fuzzing and memory consistency solvers are invalidate already-completed loads when a coherency event popular areas of research. We first discuss related hardware changes the underlying cache line. Load 2 is therefore never fuzzing research before discussing formal approaches to veri- replayed and commits with the stale value. fying memory consistency. VIII. DISCUSSION Hardware fuzzers. To the best of our knowledge, HART- BREAKER is the first general hardware fuzzer that is capable We now discuss the scalability of data-flow verification and of generating multi-hart assembly programs and verifying their the challenges involved in reducing test cases. correctness. Some hardware fuzzers, such as INSTILLER [50], Verification scalability. HARTBREAKER scales well due to DifuzzRTL [26] and ProcessorFuzz [17] support interrupt the determinism anchors, enabling large program lengths. fuzzing, but unlike HARTBREAKER, they do not support Yet, the number of memory operations that may be executed IPIs or multi-hart capabilities. The most relevant fuzzer for between two synchronization anchors remains bounded by multi-hart testing is RISCV-DV [7], which cannot verify the the capacity of the memory consistency solver. Initially, we correctness of test program execution. AXE [36] is a tool implemented our own custom memory consistency solver. This for testing and validating the memory subsystem of shared- solver was inefficient for our verification scenario, and could memory multiprocessors. It records memory request/response only handle around ten memory operations before having to traces, then checks those traces against a consistency model. use a synchronization anchor due to extremely long solving Still, it only supports an older version of the RVWMO model,
12
and requires a custom RTL-level generator such as Rocket’s 1 1 la x1, ADDR_A
GroundTest. 2 2 sd a0, 0(a1) # Write(x)
Formal approaches. Formal approaches are not general, and 3 3 bltu a0, a4, ...
mostly focus on memory consistency models, and struggle 4 4 lb s2, 0(a1) # Load(x) id=0
5 # Write(x) 5 xor s2, s2, s2
when scaling to larger CPU designs. There has been research 6 sw x2, 0(a1) 6 lbu s5, 0(a1) # Load(x) id=1
on the interaction of interrupts with memory consistency 7 7 mulhu s5, s5, zero
models, but such work aims at defining a better model rather 8 8 bne s2, s2, ...
9 9 sd s0, 0(a7)
than testing hardware’s correctness [38]. Other formal ap- 10 ... 10 lwu sp, 0(a1) # Load(x) id=2
proaches formalize the microarchitecture of CPUs, and verify
this model against different memory models [33], [35], [42]. (a) Hart 0 instructions. (b) Hart 1 instructions.
Yet, unlike HARTBREAKER, the microarchitecture of these Fig. 18: Complete N1 test case excerpt.
CPUs must be manually translated. Automatic translation of
RTL into microarchitectural specifications is possible, but
scaling to complex CPUs with speculation or caches remains 1 1 lw s7,0(sp) # Load(x) id=0
a challenge [24]. Recent efforts to bridge this gap [25] cannot 2 2 sraiw zero,t1,0x0
yet verify memory consistency models. Other formal tools aim 3 3 remw s7,s7,s7
4 4 and s2,s2,t5
to synthesize litmus test suites from axiomatic memory model 5 5 and s7,s7,t5
formalizations [34], but they suffer from the same limitation 6 6 xor s2,s2,s7
as standard litmus tests: they are not complex enough to exert 7 7 lui tp,0x1cc5a
8 8 lwu t1,0(s2) # Load(x) id=1
meaningful pressure on bare-metal hardware. 9 9 addi tp,tp,-764
Software concurrency fuzzing. Previous work applies 10 10 and tp,tp,t5
11 11 and a7,a7,t5
fuzzing techniques to detect concurrency bugs in multithreaded 12 12 xor tp,tp,a7
software, using strategies such as thread-aware input prioriti- 13 # Write(x) 13 lui a7,0x80005
zation, automatic control of thread interleavings, and context- 14 sd s1, 0(a1) 14 mul t1,t1,zero
15 15 addi a7,a7,1496
sensitive race detection [19], [22], [27]–[30], [45]. While 16 16 and a7,a7,t5
effective at finding concurrency bugs at the software level, 17 17 and s7,s7,t5
these approaches operate on compiled binaries or source code 18 18 xor a7,a7,s7
19 19 lui a5,0xd3f4d
and rely on software-level oracles such as crash detection, 20 20 addi a5,a5,-368
sanitizers, or assertion violations. Even if such a tool hap- 21 21 and a5,a5,t5
pened to trigger a hardware memory ordering bug, it would 22 22 and t1,t1,t5
23 23 xor a5,a5,t1
lack the oracle to detect it: the observed outcomes are not 24 24 lui t1,0x80005
checked against a formal memory model specification, and 25 ... 25 lwu s0,0(tp) # Load(x) id=2
the microarchitectural state is not visible to the fuzzer. In (a) Hart 0 instructions. (b) Hart 1 instructions.
contrast, our work generates bare-metal litmus tests and checks
their outcomes against the RISC-V memory model, enabling Fig. 19: Complete B1 test case excerpt.
the detection of hardware-level ordering violations that are
invisible to software-level tools.
ACKNOWLEDGMENTS
X. CONCLUSION The authors would like to thank all reviewers for their
We presented HARTBREAKER, the first RISC-V fuzzer valuable feedback and guidance during the review process. capable of systematically testing communication channels This work was supported in part by the Swiss State Secretariat such as shared memory or inter-processor interrupts on multi- for Education, Research and Innovation under contract number hart CPUs. To make this possible, HARTBREAKER needs MB22.00057 (ERC-StG PROMISE). to address the fundamental challenge of validating correct behavior in the presence of inherent non-determinism in APPENDIX A multi-hart execution. HARTBREAKER achieves this through TEST CASES a mechanism that we call determinism anchor. Determinism anchors enable HARTBREAKER to generate test programs Figure 18 and Figure 19 show the entire assembly snippets that exhibit arbitrary yet bounded non-deterministic behavior, relevant to the bugs described in Section VII-E. The instruc- enabling efficient program execution and scalable validation tions prior to the snippets play an important role in priming of correct CPU behavior. Our evaluation on five well-tested the microarchitectural structures before these critical sections RISC-V designs discovered five previously unknown concur- execute. The sections only show the memory operations rel- rency bugs, demonstrating that critical multi-hart interactions evant to the bugs, and their interleaving instructions, which remain under-tested in practice. play a crucial role in triggering the correct timings.
13
APPENDIX B F. Experiment Workflow
ARTIFACT APPENDIX All experiments are orchestrated by per-figure Bash scripts
A. Abstract in artifact_reproduction/. Each script runs inside
the appropriate Docker container and produces a PDF in
This artifact contains the HartBreaker fuzzing framework figures/.
for RISC-V processor verification, together with pre-built 1) Collect shared benchmark data (required for Fig-
simulator binaries, Docker containers, and scripts to reproduce ures 10–13):
all figures (Figures 8-14) from the paper. The artifact runs ./artifact_reproduction/collect_data.sh
inside Docker containers to ensure a consistent environment. 2) Generate individual figures:
Reviewers can reproduce each figure independently using the ./artifact_reproduction/figure_8.sh
provided scripts, which handle data collection, processing, and ./artifact_reproduction/figure_9.sh
PDF figure generation. A Zenodo archive provides a persistent, ./artifact_reproduction/figure_10.sh
citable snapshot of the full artifact. ./artifact_reproduction/figure_11.sh
./artifact_reproduction/figure_12.sh
B. How to Access ./artifact_reproduction/figure_13.sh
./artifact_reproduction/figure_14.sh
The artifact is archived on Zenodo at https://doi.org/ Figures 8, 9, and 14 collect their own data and can be run in- 10.5281/zenodo.19417381. We also make the source code dependently of step 1. Figure 14 supports a --quick flag for available on GitHub at https://github.com/comsec-group/ faster evaluation. We provide a script to run everything in one hartbreaker. We recommend using the GitHub version, as it command: ./artifact_reproduction/run_all.sh will provide potential bugfixes, if any are found. G. Evaluation and Expected Results C. Hardware Dependencies Each script produces a PDF figure in figures/ that should match the corresponding figure in the paper: To just run the fuzzer, a user will need a processor with at • Figure 8 (PPO Rule Usage Probabilities): Distribution of least 8 cores (more cores speed up parallel benchmark runs), at rule usage should show similar relative proportions. least 16 GB of RAM and 50 GB of free disk space. Note that • Figure 9 (Memory Operations Distance Distribution): the requirements may change depending on the requirements Histogram shape should match the paper. of the design under test. For full reproduction of the figures • Figure 10 (Verification Throughput Overhead): Overhead on the paper, a processor with 256 cores, 64GiB of RAM and ratios should be within ±10% of reported values. 1TB of free disk space is recommended. • Figure 11 (Instruction Throughput): Throughput values may vary by ±15% depending on the host machine, but D. Software Dependencies • relative ordering across designs should be preserved. Figure 12 (Simulation Time): Absolute times are All dependencies are encapsulated in the provided Docker machine-dependent; trends across instruction sizes should images. Locally, the following tools will be needed: match. • Linux operating system (tested on Ubuntu 22.04). • Figure 13 (ISS and Simulation Time Breakdown): Rela- • Docker (version ≥20.10). tive proportions between ISS and simulation time should • ModelSim to re-generate the Riscv-DV test corpus. (op- match. tional) • Figure 14 (Coverage Comparison): Coverage curves should show the same relative ranking (HartBreaker with verification > HartBreaker without > RISCV-DV). E. Installation Absolute performance numbers are expected to vary across 1) Download and extract the artifact from Zenodo. machines; the key claims are about relative comparisons and 2) Build the Docker images: trends. ./scripts/build_docker.sh run REFERENCES ./scripts/build_docker.sh covcollect [1] Bluespec/Toooba. [Online]. Available: https://github.com/bluespec/ ./scripts/build_docker.sh naxriscv [2] Toooba 3) Pre-built simulator binaries are included in Cheri litmus tests. [Online]. Available: https://github.com/CTSRD- CHERI/CHERI-Litmus simulators/. To optionally rebuild from source [3] Cheri-risc-v model written in sail. [Online]. Available: https://github. (several hours): [4] com/CTSRD-CHERI/sail-cheri-riscv Cheri spike. [Online]. Available: https://github.com/marnovandermaas/ ./scripts/build_chipyard.sh cheri-riscv-isa-sim ./scripts/build_toooba.sh [5] CTSRD-CHERI/TestRIG: Testing processors with Random Instruction ./scripts/build_xs.sh Generation. [Online]. Available: https://github.com/CTSRD-CHERI/ TestRIG
14
[6] cva6-litmus. [Online]. Available: https://github.com/Michelangelo98/ fuzzing,” in 2023 IEEE Symposium on Security and Privacy (SP). IEEE, cva6-litmus 2023, pp. 2104–2121. [7] riscv-dv. Google. [Online]. Available: https://github.com/chipsalliance/ [29] Z.-M. Jiang, J.-J. Bai, K. Lu, and S.-M. Hu, “Context-sensitive and riscv-dv directional concurrency fuzzing for data-race detection,” in Network and [8] Riscv-unprivileged.pdf. Google Docs. [Online]. Available: Distributed Systems Security (NDSS) Symposium 2022, 2022. https://drive.google.com/file/d/1uviu1nH-tScFfgrovvFCrj7Omv8tFtkp/ [30] Y. Ko, B. Zhu, and J. Kim, “Fuzzing with automatically controlled view?usp=drive link&usp=embed facebook interleavings to detect concurrency bugs,” Journal of Systems and [9] Sail risc-v model. [Online]. Available: https://github.com/riscv/sail-riscv Software, vol. 191, p. 111379, 2022. [10] Spike, a risc-v isa simulator. [Online]. Available: https://github.com/ [31] K. Laeufer, J. Koenig, D. Kim, J. Bachrach, and K. Sen, “Rfuzz: [11] riscv-software-src/riscv-isa-sim Coverage-directed fuzz testing of rtl on fpgas,” in 2018 IEEE/ACM SpinalHDL/NaxRiscv. [Online]. Available: https://github.com/ International Conference on Computer-Aided Design (ICCAD). IEEE, [12] SpinalHDL/NaxRiscv/tree/main 2018, pp. 1–8. [13] Verilator. [Online]. Available: https://github.com/verilator/verilator [32] L. Lamport, “How to Make a Multiprocessor Computer That [14] Whisper. [Online]. Available: https://github.com/tenstorrent/whisper Correctly Executes Multiprocess Programs,” IEEE Transactions J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, “Litmus: Running tests on Computers C-28, vol. 9, pp. 690–691, Sep. 1979. [Online]. against hardware,” in International Conference on Tools and Algorithms Available: https://www.microsoft.com/en-us/research/publication/make- for the Construction and Analysis of Systems. Springer, 2011, pp. multiprocessor-computer-correctly-executes-multiprocess-programs/ [15] 41–44. [33] D. Lustig, M. Pellauer, and M. Martonosi, “Pipecheck: Specifying J. Alglave, L. Maranget, and M. Tautschnig, “Herding cats: Modelling, and verifying microarchitectural enforcement of memory consistency simulation, testing, and data mining for weak memory,” ACM Trans- models,” in 2014 47th Annual IEEE/ACM International Symposium on actions on Programming Languages and Systems (TOPLAS), vol. 36, Microarchitecture. IEEE, 2014, pp. 635–646. [16] no. 2, pp. 1–74, 2014. [34] D. Lustig, A. Wright, A. Papakonstantinou, and O. Giroux, “Automated K. Asanovi´c, R. Avizienis, J. Bachrach, S. Beamer, D. Biancolin, synthesis of comprehensive memory model litmus test suites,” ACM C. Celio, H. Cook, D. Dabbelt, J. Hauser, A. Izraelevitz, S. Karandikar, SIGPLAN Notices, vol. 52, no. 4, pp. 661–675, 2017. B. Keller, D. Kim, J. Koenig, Y. Lee, E. Love, M. Maas, A. Magyar, [35] Y. A. Manerkar, D. Lustig, M. Martonosi, and M. Pellauer, “Rtlcheck: H. Mao, M. Moreto, A. Ou, D. A. Patterson, B. Richards, C. Schmidt, Verifying the memory consistency of rtl designs,” in Proceedings of the S. Twigg, H. Vo, and A. Waterman, “The rocket chip generator,” 50th Annual IEEE/ACM International Symposium on Microarchitecture, Tech. Rep. UCB/EECS-2016-17, Apr 2016. [Online]. Available: http: 2017, pp. 463–476. [17] //www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-17.html [36] M. Naylor, S. Moore, and A. Mujumdar, “A consistency checker S. Canakci, C. Rajapaksha, L. Delshadtehrani, A. Nataraja, M. B. Taylor, for memory subsystem traces,” 2016. [Online]. Available: https: M. Egele, and A. Joshi, “Processorfuzz: Processor fuzzing with control //www.repository.cam.ac.uk/handle/1810/260225 and status registers guidance,” in 2023 IEEE International Symposium [37] H. Ponce-de Le´on, F. Furbach, K. Heljanko, and R. Meyer, “Portability on Hardware Oriented Security and Trust (HOST). IEEE, 2023, pp. analysis for weak memory models porthos: One tool for all models,” in [18] 1–12. International Static Analysis Symposium. Springer, 2017, pp. 299–320. J. F. Cantin, M. H. Lipasti, and J. E. Smith, “The complexity of verifying [38] B. Simner, A. Armstrong, T. Bauereiss, B. Campbell, O. Kammar, memory coherence and consistency,” IEEE Transactions on Parallel and J. Pichon-Pharabod, and P. Sewell, “Precise exceptions in relaxed Distributed Systems, vol. 16, no. 7, pp. 663–671, 2005. architectures,” in Proceedings of the 52nd Annual International [19] H. Chen, S. Guo, Y. Xue, Y. Sui, C. Zhang, Y. Li, H. Wang, and Y. Liu, Symposium on Computer Architecture, ser. ISCA ’25. New York, “{MUZZ}: Thread-aware grey-box fuzzing for effective bug hunting in NY, USA: Association for Computing Machinery, 2025, p. 211–224. multithreaded programs,” in 29th USENIX Security Symposium (USENIX [Online]. Available: https://doi.org/10.1145/3695053.3731102 Security 20), 2020, pp. 2325–2342. [39] F. Solt, K. Ceesay-Seitz, and K. Razavi, “Cascade: CPU Fuzzing via [20] G. Dessouky, D. Gens, P. Haney, G. Persyn, A. Kanuparthi, H. Khattri, Intricate Program Generation.” J. M. Fung, A.-R. Sadeghi, and J. Rajendran, “{HardFails}: insights into {software-exploitable} hardware bugs,” in 28th USENIX Security [40] F. Solt, P. Jattke, and K. Razavi, “Rememberr: Leveraging microproces- Symposium (USENIX Security 19), 2019, pp. 213–230. sor errata for design testing and validation,” in 2022 55th IEEE/ACM [21] S. Flur and L. Maranget. litmus-tests-riscv. riscv. [Online]. Available: International Symposium on Microarchitecture (MICRO). IEEE, 2022, https://github.com/litmus-tests/litmus-tests-riscv pp. 1126–1143. [22] S. Gong, D. Altinb¨uken, P. Fonseca, and P. Maniatis, “Snowboard: Find- [41] F. Thomas, L. Hetterich, R. Zhang, D. Weber, L. Gerlach, and ing kernel concurrency bugs through systematic inter-thread communi- M. Schwarz, “Riscvuzz: Discovering architectural cpu vulnerabilities cation analysis,” in Proceedings of the ACM SIGOPS 28th Symposium via differential hardware fuzzing,” https://ghostwriteattack. com/, 2024. on Operating Systems Principles, 2021, pp. 66–83. [42] C. Trippel, Y. A. Manerkar, D. Lustig, M. Pellauer, and M. Martonosi, [23] R. G¨otz, C. Sendner, N. Ruck, M. Rostami, A. Dmitrienko, and A.-R. “Tricheck: Memory model verification at the trisection of software, Sadeghi, “Rlfuzz: Accelerating hardware fuzzing with deep reinforce- hardware, and isa,” ACM SIGPLAN Notices, vol. 52, no. 4, pp. 119– ment learning,” in 2025 IEEE International Symposium on Hardware 133, 2017. Oriented Security and Trust (HOST). IEEE, 2025, pp. 358–369. [43] T. Trippel, K. G. Shin, G. Kelly, D. Rizzo, M. Hicks, and V. Tech, [24] Y. Hsiao, D. P. Mulligan, N. Nikoleris, G. Petri, and C. Trippel, “Fuzzing Hardware Like Software.” “Synthesizing formal models of hardware from rtl for efficient verifica- [44] A. Tyagi, A. Crump, A.-R. Sadeghi, G. Persyn, J. Rajendran, P. Jauernig, tion of memory model implementations,” in MICRO-54: 54th annual and R. Kande, “Thehuzz: Instruction fuzzing of processors using golden- IEEE/ACM international symposium on microarchitecture, 2021, pp. reference models for finding software-exploitable vulnerabilities,” arXiv 679–694. preprint arXiv:2201.09941, 2022. [25] Y. Hsiao, N. Nikoleris, A. Khyzha, D. P. Mulligan, G. Petri, C. W. [45] D. Wolff, Z. Shi, G. J. Duck, U. Mathur, and A. Roychoudhury, “Grey- Fletcher, and C. Trippel, “Rtl2mμpath: Multi-μpath synthesis with box fuzzing for concurrency testing,” in Proceedings of the 29th ACM applications to hardware security verification,” in 2024 57th IEEE/ACM International Conference on Architectural Support for Programming International Symposium on Microarchitecture (MICRO). IEEE, 2024, Languages and Operating Systems, Volume 2, 2024, pp. 482–498. pp. 507–524. [46] L. Wu, M. Rostami, H. Li, J. Rajendran, and A.-R. Sadeghi, [26] J. Hur, S. Song, D. Kwon, E. Baek, J. Kim, and B. Lee, “DifuzzRTL: “{GenHuzz}: An efficient generative hardware fuzzer,” in 34th USENIX Differential Fuzz Testing to Find CPU Bugs,” in 2021 IEEE Symposium Security Symposium (USENIX Security 25), 2025, pp. 1787–1805. on Security and Privacy (SP), pp. 1286–1303. [Online]. Available: [47] L. Wu, M. Rostami, H. Li, and A.-R. Sadeghi, “Hfl: Hardware fuzzing https://ieeexplore.ieee.org/document/9519470/ loop with reinforcement learning,” in 2025 Design, Automation & Test [27] D. R. Jeong, K. Kim, B. Shivakumar, B. Lee, and I. Shin, “Razzer: in Europe Conference (DATE). IEEE, 2025, pp. 1–7. Finding kernel race bugs through fuzzing,” in 2019 IEEE Symposium [48] J. Xu, Y. Liu, S. He, H. Lin, Y. Zhou, and C. Wang, “{MorFuzz}: on Security and Privacy (SP). IEEE, 2019, pp. 754–768. Fuzzing processor via runtime instruction morphing enhanced synchro- [28] D. R. Jeong, B. Lee, I. Shin, and Y. Kwon, “Segfuzz: Segmentiz- nizable co-simulation,” in 32nd USENIX Security Symposium (USENIX ing thread interleaving to discover kernel concurrency bugs through Security 23), 2023, pp. 1307–1324.
15
[49] Y. Xu, Z. Yu, D. Tang, G. Chen, L. Chen, L. Gou, Y. Jin, Q. Li, X. Li, Z. Li et al., “Towards developing high performance risc-v processors using agile methodology,” in 2022 55th IEEE/ACM International Sym- posium on Microarchitecture (MICRO). IEEE, 2022, pp. 1178–1199. [50] G. Zhang, P. Wang, T. Yue, D. Liu, Y. Guo, and K. Lu, “Instiller: Toward efficient and realistic rtl fuzzing,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 43, no. 7, pp. 2177–2190, 2024. [51] J. Zhao, B. Korpan, A. Gonzalez, and K. Asanovic, “Sonicboom: The 3rd generation berkeley out-of-order machine,” May 2020.
16