NNSmith: Generating Diverse and Valid Test Cases for Deep Learning Compilers

Jiawei Liu, Jinkun Lin, Fabian Ruffy, Cheng Tan, Jinyang Li, Aurojit Panda, Lingming Zhang

Introduction

Deep learning (DL) compilers such as TVM (Chen et al., 2018a), TensorRT (NVIDIA, 2022), and TensorFlow XLA (Abadi et al., 2016) are increasingly being used to deploy deep neural network (DNN) models in many different applications. These compilers optimize DL models to meet desired performance, energy, and resource requirements, allowing their use by interactive or safety-critical applications deployed on a variety of devices. However, as compiler implementations are complex, we must be vigilant about detecting bugs in these systems. Compiler bugs can result in crashes or generating an incorrect executable that produces different results than those intended by the user-specified input modelAs deep-learning models use floating-point operations, a correctly compiled executable model can have close but not identical results as those of the input model. We do not regard this case as a bug..

In this paper, we develop techniques to automatically find bugs in deep-learning compilers. Similar to prior work (Liu et al., 2022; Luo et al., 2021; Wang et al., 2020), we adopt a fuzzing and differential testing based approach: we generate random models, compile them using the compiler being tested, and then compare results obtained from the compiled model with those from a reference implementation. This basic approach faces two main challenges, which are not adequately addressed by prior work. First, how do we generate structurally diverse and valid models? Deep-learning compilers express a model as a computation graph of tensor operators. For better test coverage, we must ensure model diversity, which requires us to generate graphs by combining operators in different ways. However, connecting two arbitrary operators often produces invalid models, which are rejected by deep learning compilers. For example, a compiler will reject any computation graph containing a MatMul (matrix multiplication) operator for which the number of rows in the first input differs from the columns for the second. Therefore, for test efficiency, our graph generation method must also ensure the validity of generated models. Second, given a compiled model, what weights/inputs should we use to run it for differential testing? Naively testing generated models with random or default weights/inputs can easily lead to floating point (FP) exceptional values, i.e., NaNNaNs or infinities (InfInfs). In such cases, we cannot compare the compiled model with its reference implementation. Therefore, to enable equivalence checking, we must be able to generate computation inputs that can avoid FP exceptional values during model execution.

We develop NNSmith, a tester for deep-learning compilers including TVM (Chen et al., 2018a), ONNXRuntime (Microsoft, 2020), and TensorRT (NVIDIA, 2022), that addresses these two challenges. NNSmith adopts a three-step approach for finding bugs: 1 first, it automatically generates an arbitrary but valid computation graph expressing some model MIM_{I}; 2 it then uses the compiler being tested to produce a compiled model MOM_{O} from MIM_{I}, and a reference backend to produce an executable model MRM_{R}; and 3 finally it generates random inputs which it passes to MOM_{O} and MRM_{R}, and compares their outputs.

NNSmith addresses the model and input generation challenges as follows.

Generating diverse and valid computation graphs: The computation graph expressing a deep-learning model consists of tensor operators with attributes attached to both the operators and graph edges. Operator attributes specify parameters such as kernel sizes that impact the operator’s semantics, while edge attributes are used to specify input and output tensor typesA tensor’s type defines its shape and its elements’ data type.. Before proceeding with the actual compilation steps, deep-learning compilers check the validity of the input computation graph, e.g., whether an operator’s output tensor type matches the expected input tensor type of its downstream operators and whether an operator’s attributes are valid. In order to produce valid graphs, NNSmith aims to capture and ensure the type matching constraints of a computation graph during its generation. To do so, NNSmith requires that users provide a specification for each operator, which specifies the constraints that must be satisfied by the operator’s input tensors/attributes and also indicates the operator’s output tensor type, which NNSmith can use to check the validity of generated graphs. During NNSmith’s incremental graph generation, it inserts one candidate operator at a time by solving for the satisfiability of its type matching constraints given the existing graph. NNSmith uses an existing SMT solver (Moura and Bjørner, 2008) for constraint solving.

Executing compiled models without FP exceptional values. In order to meaningfully compare the outputs of a compiled computation graph with those from a reference implementation, NNSmith aims to select computation inputs (aka model weights and inputs) that do not result in NaNNaNs or InfInfs during execution. Instead of random search, NNSmith uses gradient-guided search to efficiently find viable model inputs/weights for 98% of the generated models with negligible overhead.

In addition to addressing the two main challenges above, we designed NNSmith so it can be easily extended to add support for new operators or to work with other deep-learning compilers. We do so by providing users with a framework for writing operator specifications that are needed to ensure graph validity, and by providing a library of common patterns. In our experience, using this framework and library, users can write new operator specifications in a few lines of code. We evaluated the efficacy of our approach by using NNSmith to identify bugs in TVM, ONNXRuntime, TensorRT, and PyTorch.

Over the last seven months, NNSmith found 72 new bugs in these frameworks. Developers have confirmed 58 and fixed 51 of these bugs. Our coverage evaluation also shows that NNSmith outperforms the state-of-the-art fuzzer by 1.8×\times for ONNXRuntime and 1.08×\times for TVM in total branch coverage, as well as 32.7×\times and 10.8×\times respectively in unique branches.

Background

DL frameworks represent a model’s underlying computation as a directed graph of tensor operators. In this work, we focus on DNN inference, where the graph captures the forward NN computation to generate predicted labels or outputs given the model weights and some inputs. For example, the model in Figure 1 is invoked by specifying its inputs (i.e., input variables %x0 and %x1) and the model weights (i.e., input variable %w0), and the DNN runtime computes the output tensor (%v2) from these inputs.

In what follows, we use the term tensor type to refer to both the shape and element type of a tensor. In the DNN computation graph, each edge is marked with the tensor type that corresponds to the output of the edge’s upstream operator, as shown in Figure 1. When instantiating an operator, model developers must specify certain additional attributes that dictate its output tensor type. For example, on line 4 in Figure 1, the Reshape operator takes %v1 as an input tensor and as an attribute indicating the output shape. Because each operator expects its input tensors to be of certain types, it is often invalid to connect two arbitrary operators together by an edge: e.g., the reshape operator on line 4 is valid if and only if its upstream operator’s output (%v1) has 76887688 elements (62×62×262\times 62\times 2). This is akin to a “type checking error” in traditional programs. We say that a DNN computation graph is valid if and only if all operators in the graph are valid.

2. DL Compilers

State-of-the-art DL compilers turn a user-specified model, expressed as a DNN computation graph, into an executable implementation. As shown in Figure 2, DL compilers process an input DNN model in two stages during its compilation.

First, DL compilers need to convert an input computation graph into their own internal formats. For interoperability, DL training frameworks typically export trained models to a standardized format such as ONNX (Bai et al., 2019). DL compilers take ONNX models as input and convert them to a compiler-specific Intermediate Representation (IR) that is easier for the compiler to ompimize.

Next, DL compilers invoke various transformation passes which rewrite the input IR into a more efficient version. These passes include: graph-optimization passes that simplify the graph (e.g., constant folding) or fuse operators (merge Add and Softmax into BiasSoftmax) (ONNXRuntime, 2022a); low-level passes that optimize computation using arithmetic simplification and loop tiling/fusion, to reduce computational overheads.

Compiler bugs can occur in both the conversion and transformation phases, but bugs in the later phase are generally harder to identify and debug. To comprehensively detect both kinds of bugs, we need to test using models with a diverse graph structure and tensor operators.

3. Challenges in Finding DL Compiler Bugs

Differential testing and fuzzing (McKeeman, 1998) is a promising approach for finding DL compiler bugs. As shown in the right part of Figure 2, this approach requires synthesizing random models for compilation, then running the compiled models with random inputs, and finally comparing the generated results with those from a reference implementation.

There are several challenges facing the basic approach of fuzzing and differential testing, which are not addressed by prior work (Luo et al., 2021; Wang et al., 2020; Wei et al., 2022). Next, we illustrate these challenges using concrete examples.

Challenge #1: Generating graphs with diverse patterns. Finding DL compiler bugs requires generating input graphs that contain a variety of operators and connections. Some prior fuzzers (Wei et al., 2022) test only using single-operators and thus are too limiting. LEMON (Wang et al., 2020) and GraphFuzzer (Luo et al., 2021) generate multi-operator computation graphs, but they are restricted to certain types of operators and connections in order to avoid “type check” errors on the generated graphs (detailed in §6.1). These restrictions limit graph diversity, and compromise test coverage.

Listing 1 shows an example model (M0) generated by NNSmith which has triggered a layout analysis bug in TVM. LEMON cannot generate this model because M0 contains non-shape-preserving operators (e.g., Conv2d) and connections (e.g., broadcasting) which are not supported by LEMON for ensuring graph validity. GraphFuzzer uses a different strategy to guarantee graph validity. Specifically, GraphFuzzer tries to “fix” mismatched tensor shapes in generated graphs through slicing and padding, as illustrated by line 1 in model M1. Unfortunately, doing so biases the generated graphs to include many slicing/padding nodes. In our example, the slice operation in M1 would silence the layout bug found in M0.

Challenge #2: Exploring diverse attributes for operators and edges. When generating graphs, it is tempting to ignore the need to explore the operator/edge attribute space and rely on some default values. For example, M2 of Listing 1 uses trivial attributes (e.g., always 1) to initialize operator Ones(1,1,1) (line 1). Unfortunately, the bug found by M0 will not be triggered by M2. Since exploring different attribute values results in diverse output tensor types on edges, it further complicates the task to ensure the validity of generated graphs.

Challenge #3: Running compiled models to produce numerically valid output. Using arbitrary inputs and model weights to test a compiled model can result in FP exceptional values (i.e., NaNNaNs and InfInfs) during execution for differential testing. Such cases occur when the given inputs to some operator are outside of its expected domain, e.g., feeding Sqrt negative values results in NaNNaNs, and feeding Pow large base or exponents results in InfInfs. Larger graphs are particularly prone to encountering FP exceptional values. For example, we have found that NaNNaN/InfInf occurs in 56.8% of 20-node models generated by NNSmith when using PyTorch’s default weight initializer. Previous testing frameworks did not consider these issues, and consequently up to 41% of their bug reports can be false-alarms because of the undefined/non-deterministic behaviors arising from the NaNNaN/InfInf (gbftdlie, 2020).

Clearly we should not compare the output of a compiled model to those of the reference implementation if the results themselves contain NaNNaN/InfInf. What about those scenarios with normal final results (aka without any NaNNaN/InfInf) where some internal operator has produced FP exceptional values during graph execution? For example, operator ArgMax can output a normal FP value even though one of its upstream operators gives it NaNNaN as input. It is a subtle requirement that we must also exclude these results from differential testing or risk incurring false positives in bug detection. This is because when handling FP exceptional values, otherwise semantically equivalent operators could produce different results. Therefore, to be able to test effectively, we must generate model inputs/weights that avoid FP exceptional values for all operators in the graph. Only then we refer to the model’s output as numerically valid. Otherwise, we might miss detecting bugs. As an example, Listing 1’s model M3 can trigger a semantic bug. However, this bug is not exposed because the execution results in InfInf values which are not used for comparison.

NNSmith’s Design

Figure 3 shows an overview of NNSmith’s workflow. NNSmith generates random models that are valid, which are then compiled and executed. NNSmith takes as input a compiler’s type checking requirements in the form of operator specifications (§3.1), and then uses an SMT solver to generate graphs and operator attributes that meet these constraints (§3.2). Next, when running a compiled model, NNSmith uses a gradient guided search procedure to find benign weights/inputs so that no FP exceptional values are produced at any step of the execution (§3.3). Finally, NNSmith compares the results obtained from multiple deep learning libraries and compilers to those from a reference implementation to identify bugs.

1. Modeling DNN Operators

NNSmith generates random DNN models expressed as computational graphs by connecting together different operators. We aim to generate valid graphs that “type check”, i.e., graphs where each operator’s attributes and input tensor type meet requirements imposed by the compiler.

In order to generate valid graphs, we require users to provide operator specifications that explicitly state the compiler’s requirements for each operator and guarantees about its output. An operator’s specification codifies rules for checking validity and depends on its inputs and attributes: For example, the 2-D convolution operator (Conv2d) has several attributes, including a kernel, and takes an image as input. A model that uses a Conv2d operator is valid if the input image is a rank-4 tensor that is larger than the kernel’s size.

While our implementation includes specifications for common operators (detailed in §4), we designed NNSmith so that it is easy for users to write specification for additional operators. NNSmith specifications are written using symbolic integers and abstract tensors. An abstract tensor is specified by its data type, rank and shape. In our implementation we specify an abstrat tensor’s data type and rank using concrete values, and use symbolic integers to specify its shape. As we will see later in §3.2, NNSmith uses an SMT solver to assign concrete integers to each symbolic integer during graph generation. NNSmith operator specifications provide input and output types (specified using abstract tensors), constraints on inputs and attributes, as well as transfer rules for each operator. Listing 2 shows the operator specification for a 2-D pooling operator (Pool2d), and we describe each of part below:

Inputs and outputs. An operator’s attributes are inferred from the inputs to its __init__ function. The class variables input_type and output_type describe the input and output tensor types respectively (Lines 2 and 2). Programmers specify a list of tuples, each tuple says what data types can be used for an input (or provided as output). In the listing, the Pool2d operator accepts a single rank 4 tensor of 32-bit or 64-bit floats.

Constraints. The operator’s requires function (Line 2) returns constraints that its inputs and attributes must satisfy as a list of logical predicates. For example, among other constraints, the Pool2d operator requires that the kernel size should be greater than 0 (Line 2).

Type transfer function. The operator uses a type transfer function (Line 2) to specify how its output tensor relates to its inputs. For example, on Line 2, Pool2d’s type transfer function relates the shape of the operator’s output tensor to its kernel size (self.kw and self.kh) and its input shapes. Observe that the constraints output by the type transfer function become the input constraints on a downstream operator. These constraints are used to to combine constraints from connected operators in a computation graph, thereby allowing NNSmith to generate valid models.

2. Model Generation

Given a set of operator specifications, NNSmith generates models that are topologically diverse and whose operators use diverse attributes. Below we first detail our approach for generating diverse model topologies and then present our binning based approach to assigning diverse attributes.

Generating computation graphs. Our model generation algorithm is designed to ensure that generated computation graphs are fully connected, as is the case with most real-world models. Additionally, it is also designed so that it can generate a rich variety of models, including ones similar to existing multi-modal and multi-task models (He et al., 2017; Baltrušaitis et al., 2018; Radford et al., 2021; Ngiam et al., 2011) that can accept multiple inputs and/or produce multiple outputs.

NNSmith generates connected computation graph by extending an existing graph while maintaining connectivity. It does so by starting with a graph that contains a single placeholder node, and extending it by either (a) adding a new node whose input edges are connected to the output of an existing node (we refer to this as a forward insertion) or (b) replacing an existing placeholder node with an operator node whose input edges are connected to one or more placeholder nodes (we refer to this as backward insertion). In both cases, the node added by NNSmith is picked at random from the set of symbolic operator specifications (op) it is provided. Placeholder nodes have one output, and at the end of the graph generation process they are replaced by input nodes or by weights (which are constant inputs). Algorithm 1 shows our graph generation algorithm. We detail the steps taken when inserting a randomly selected operator (op) into an existing compute graph below:

Type matching: To insert op, NNSmith must first find a feasible insertion point in the current graph. When using forward insertion, this means finding an output edge in the graph whose constraints (as provided by the operator that node represents) satisfy op’s input constraints. Similarly, when using backward insertion, this means finding a placeholder node whose output is connected to node(s) whose input constraints are satisfied by op’s output constraints. To do so we need to check constraint satisfaction, and we use a SMT solver for this. Rather than invoking an SMT solver for all possible insertion points, we use a simple type matching heuristic to filter out nodes that are obviously infeasible because of incompatible data types or ranks. For example, when using forward insertion for Where(cond, T, F), type matching (Lines 1) will filter out any output edges which are not boolean.

Constraint solving: Next, NNSmith generates constraints for any feasible insertion points that have not been filtered out by its type matching heuristic, and uses an SMT solver to check their satisfiability. NNSmith caches constraints for the current model (in M.M.solver) to reduce constraint generation overheads, and uses incremental solving (Bjørner et al., 2018) to reduce time taken for checking constraints (Line 1).

Node insertion: As we stated previously, we use one of two approaches to insert nodes into the graph: forward insertion and backward insertion:

Forward insertion (Line 1) selects one group of plausible tensors (vv) as the inputs of op (Line 1) and inserts op as their consumer (Line 1) if the insertion constraints are satisfiable (Line 1).

Backward insertion (Line 1) replaces an existing placeholder node with op. To do so it first determines a placeholder candidate (vv) by matching op’s output type and the candidate’s type (Line 1—1). Next, it infers op’s input type from vv. If op’s input type constraints can be satisfied for the candidate, NNSmith replaces the candidate with op and creates new placeholder nodes (of the inferred types) to act as op’s inputs (Lines 1 and 1).

Attribute binning. In addition to topological diversity, attribute diversity is also crucial as discussed in §2.3. We use the solution (model) generated by an SMT solver (Z3 (Moura and Bjørner, 2008) in our implementation) when checking satisfiability for the graph’s constraints to determine attributes. However, we found that the models produced by SMT solvers tend to pick boundary values for integer constraints. For example, when a tensor shape DD is constrained so that {di≥1;di∈D}\{d_{i}\geq 1;d_{i}\in D\}, the Z3 SMT solver always returns models where {di=1;di∈D}\{d_{i}=1;d_{i}\in D\}, limiting the diversity of attributes in generated DNNs.

We address this problem by adding extra constraints (which we call binning constraints) that limit each attribute to a randomly chosen range. Algorithm 2 shows how we generate these binning constraints: We start from an empty set of binning constraints (CbC_{b} in Line 2), and iterate over each attribute α\alpha of each operator op (Line 2-2) in the graph (MM). Note that this algorithm also considers placeholders as operators, and uses placeholder tensor shape as attributes for these operators. The binning constraints for each attribute are generated by randomly choosing from one of kk bins, where the ithi^{th} bin represents the range [2i−1,2i)[2^{i-1},2^{i}) (when i<ki<k, the last bin represents the range [2k−1,∞)[2^{k-1},\infty)), and limiting the attribute to a subset of the bin’s range. To do so, we randomly pick a bin (Line 2) for each (op,α)(\textit{op},\alpha), and sample two integers (i.e., ll and rr) from it (Line 2). We then add l≤α≤rl\leq\alpha\leq r as the binning constraints for the (op,α)(\textit{op},\alpha) pair. We use bins with exponential ranges (Line 2) because, in practice, systems are more sensitive to changes in smaller values, e.g., changing a variable from 0 to 1 generally has larger effect on the output than changes from 30 to 31. Our approach of dividing ranges in exponential buckets is inspired by how AFL (Zalewski, 2018) coarsely records the hit counts for execution tuples (Google, 2019). We allow operators to provide a different, more specialized strategy, for attribute binning, and in this case we simply use the provided constraints (C∗C^{*} in Line 2) instead (details in §4).

Adding extra binning constraints to the graph’s constraints can produce an unsatisfiable constraint system, leading to a situation where we can find no attributes for a valid graph. We avoid this situation by adding constraints only after a graph has been generated (Paragraph 2 in §3.2) and only when doing so does not impact satisfiability. Specifically, if the solver fails to find a satisfiable assignment after adding CbC_{b} to the graph’s constraints, we randomly drop half of the constraints and retry, until it succeeds (Line 2).

3. Improving Numeric Validity with Gradients

Next, NNSmith generates inputs and weights that can be used to test the generated models. We initially considered using randomly selected numbers. However, we found that the generated graphs produce FP exceptional values, including NaN (not a number) and Inf (infinite number). For example, when generating 20-operator graphs, FP exceptional values occur in 56.8% of generated graphs if we use random weights and inputs.

This is because some operators, which we refer to as vulnerable operators (Yan et al., 2021), produce real (e.g., x\sqrt{x} returns NaNNaN if x<0x<0) or stable (e.g., xyx^{y} returns InfInf for large xx and yy) results only for a subset of their input domain. If a vulnerable operator’s input lies outside of this domain, the operator outputs an FP exceptional value, which propagates through the model and impacts the model’s output, preventing us from comparing model outputs during differential testing. Table 1 lists examples of vulnerable operators we encountered in our evaluation.

One way to address this problem is to use additional heuristics to extend and fix vulnerable operators. For example, changing Div(x, y) to Div(x, —y—+ϵ\epsilon) ensures that the Div operator is safe. However, this requires changing operator inputs, which limits graph diversity as discussed in §2.3. We thus propose an alternate approach, where we use a gradient-search algorithm to find inputs that ensure that the model’s output is numerically valid. Our approach is inspired by GRIST (Yan et al., 2021), though that work has the opposite goal: it aims to find inputs that result in FP exceptional values.

At a high-level, our approach associates a set of loss functions with each operator. When selecting inputs, NNSmith starts with random inputs, and then iteratively refines these inputs so that no operator in the graph produces an FP exceptional value. In each iteration, NNSmith identifies the first operator in the model that produces an FP exceptional value. It then uses the set of loss functions associated with the operators to compute new model inputs and uses these for the next iteration. The algorithm terminates when no FP exceptional values are found. We provide details below:

Loss functions for avoiding FP exceptional values. NNSmith associates a set of loss functions with each operator, which our input search algorithm (Algorithm 3) uses to update inputs to avoid FP exceptional values. Users can specify loss functions for each operator, and below we describe our approach to producing loss functions.

As we noted above, vulnerable operators produce valid outputs (i.e., outputs that are not FP exceptional values) when inputs are drawn from a particular domain, and this domain can be expressed (or approximated) by the conjunction of a few (usually one or two) inequality predicates on the operator’s input. We refer to this conjunction of inequality predicates as the operator’s tensor inequalities. For example, the Sqrt(X)Sqrt(X) operator takes a tensor XX as input, and is numerically valid if and only if X≥0X\geq 0 (i.e., all elements of XX are positive). Similarly, the Pow(X,Y)Pow(X,Y) operator’s numerically valid domain can be under-approximated as X≥0∧Ylog⁡(X)≤40X\geq 0\wedge Y\log(X)\leq 40, which requires that all elements of XX be positive to avoid NaNNaNs (since YY might contain fractional elements) and bounds Ylog⁡(X)Y\log(X) to avoid outputs that are too large (and would be represented by infinity) We constrain the logarithm instead of directly using the power function to ensure that the loss function does not generate a FP exceptional value.. We associate a loss function with each predicate in an operator’s tensor inequality. We do so by first rewriting each predicate so that it is either of the form f(X)<0f(X)<0 or f(X)≤0f(X)\leq 0, and then use the formulas in Table 2 to convert this cannonical form to a scalar loss. We show examples of the loss functions produced in this manner in Table 1. When an operator produces invalid outputs, the search algorithm picks which loss function to use by finding a predicate that is violated by the operator’s current input and using the loss function associated with it. For simplicity, our design assumes that a loss function is positive if and only if its associated predicate is violated by the operator’s input, allowing us to use any positive loss function associated with the operator (Line 3) without evaluating its associated predicate.

Proxy derivative. Given a vulnerable operator’s loss, NNSmith uses gradient propagation to compute changes to the model inputs and weights. Doing so requires computing gradients (derivatives) for each operator in the graph (Line 3). However, some operators are either undifferentiable for some inputs (e.g., Floor, Ceil, and other operators cannot be differentiated at integers) or have zero gradient in some region (e.g., ReLU has gradient 0 for all negative inputs), and this prevents backward propagation. For these functions, we use Proxy Derivative Functions (Bengio et al., 2013) instead of actual derivatives during gradient propagation.

Search process. The overall input search algorithm (Algorithm 3) proceeds as follows: Given a model MM and time budget TT, we first randomly initialize inputs and weights ⟨X,W⟩\langle X,W\rangle (Line 3) used by the first iteration of the search algorithm (Line 3). In each iteration, we find the first operator (in topological order, Line 3) that produces an FP exceptional value (Line 3). We use its loss function as an optimization objective (Line 3) to tune ⟨X,W⟩\langle X,W\rangle. If the gradient is neither zero nor a FP exceptional values then we move on to the next iteration (Line 3), otherwise we restart the search with a different initial value (Line 3 and 3). The algorithm throws an exception (Line 3) if it does not terminate within the time budget.

Because loss functions can vary by orders-of-magnitude across operators, we use Adam (Kingma and Ba, 2014), an adaptive learning rate scheduling algorithm, to set the learning rate. We also reset the learning rate whenever we switch the loss functions used for optimization (as would be the case when an iteration finds a different operator). While this design can lead to a scenario where optimizing for one operator leads to another producing invalid outputs and vice-versa, we found that this to be rare in practice (it occurred less than 1% of the time). We found that the most common reason for the search algorithm failing was that the model has no valid inputs.

Implementation

NNSmith is implemented in 5157 lines of Python code. Consistent with Algorithm 1, NNSmith outputs a symbolic graph and its SMT solution for being valid with the help of the Z3 (Moura and Bjørner, 2008) solver. We then concretize the symbolic graph by invoking the materialized PyTorch functors in the topological order, and export the model to the deployment-friendly ONNX (Bai et al., 2019) format using PyTorch’s exporter. We also use PyTorch to implement our algorithm for finding model inputs/weights that result in numerically valid output (§3.3).

Since DL compilers vary in operator and data type support, we infer the set of operators supported by the compiler being tested by trying to compile single-operator models with different data types. We use this information when generating graphs, so as to avoid “Not-Implemented” errors.

When verifying outputs from the compiled model, we regard PyTorch’s results as the oracle. We use PyTorch as the reference backend over compiler cross-checking because: 1) Obtaining results from PyTorch is a “free” lunch which is a by-product of gradient-based value searching; 2) Current DL compilers support different operator sets or data types, implying that cross-checking is limited to the common set of their support matrices; and 3) PyTorch’s results are more trustworthy for being a better-tested interpreter, which has been used to produce oracles in many downstream compilers. In rare cases value inconsistency (1 out of 72 in our bug finding) can happen in PyTorch’s converter which makes it unclear whether the bug comes from the converter or the compiler. Therefore, for better fault localization, if the compiler and PyTorch disagree on the model outputs, we further compare it with the compiler “O0” mode at an extra cost of re-compilation. If the “O0” mode also disagrees with the optimized model, we then are confident the compiler’s optimization must be wrong.

We wrote operator specifications in NNSmith using information obtained from framework documentation (PyTorch, 2021) and source code (ONNXRuntime, 2022b). To simplify this task, we implemented several meta types including, unary/binary, reduce and broadcast that further reduce the amount of code needed to specify an operator. Using these, we found that we could implement 59 (out of 73) operator specification within 4 lines of code. Furthermore, even for the most complex specification, which was for Conv2d, the requires function has 9 inequalities and the type_transfer function is only 7 lines of code (formatted by PEP8 (Rossum et al., 2013)) that can be quickly implemented in a few minutes. Furthermore, these specifications can be written once and then shared by all compilers that can accept ONNX models as input.

Regarding the C∗C^{*} in attribute binning (Line 2 in Algorithm 2), our current implementation uses the following default settings: 1) we add one extra bin that contains only one integer “0” for the “padding” attribute in Conv2d, for that padding can also be 0; 2) similarly, for the “padding” attribute in ConstPad, ReplicatePad, and ReflectPad, we add both the 0-bin and negative bins that for supporting zero and negative padding; 3) we specifically handle for the indexing ranges (i.e., “start” and “end” attributes) in Slice to make sure the range is valid to its input tensor shape.

Evaluation

Metrics. We mainly target the following metrics for evaluation:

Code coverage: Following prior fuzzing work (Böhme et al., 2022, 2017; Wei et al., 2022), we trace source-level branch coverage for both the entire systems and their pass-only components, measuring 1) total coverage counts all hit branches; and 2) unique coverage counts unique branches (“hard” branches) that other baselines cannot cover.

Bug counting: Following prior work (Weimer, 2006; Wei et al., 2022; Liu et al., 2022), we use the number of independent patches as the number of detected bugs, except that we directly count the number of bug reports for closed-source systems (i.e., TensorRT) and unfixed ones.

Baselines. We compare NNSmith with both the state-of-the-art general DNN model generators (LEMON and GraphFuzzer) and fuzzer specifically designed for TVM (i.e., Tzer).

LEMON (Wang et al., 2020) is a mutation-based model generator that mutates pre-trained Keras (Google, 2015) models (Wang et al., 2021). We convert Keras models into ONNX, to reuse the same differential testing and evaluation framework of NNSmith for fair comparison;

GraphFuzzer (Luo et al., 2021) generates models by randomly connecting nodes from a block corpus. While LEMON is limited to shape-preserving unary operators, GraphFuzzer also supports non-unary operators by aligning input tensor shapes with slicing/padding and uses specific attributes to create shape-preserving instances for a few non-shape-preserving operators such as Conv2d. As its implementation is not open-sourced, for a fair comparison, we reimplemented its main design, e.g., stitching operators via padding/slicing, by replacing NNSmith’s specification-based node insertion.

Tzer (Liu et al., 2022) is a coverage-guided and mutation-based fuzzer targeting TVM’s low-level IR. As DNNs generated by NNSmith can also be lowered to low-level IR, we compare Tzer with NNSmith to see if NNSmith can well cover low-level optimizations as Tzer.

Systems under test. NNSmith finds bugs in the following commonly used compilers:

ONNXRuntime (ONNXRuntime, 2022a) (by Microsoft) is a graph-optimized DNN library for ONNX models, with over 130 source files on various graph optimizations. Like many runtime-based frameworks (e.g., PyTorch), though ONNXRuntime enables optimizations, the optimized graph will still be directly mapped into pre-compiled kernel functions (i.e., no code generation). To evaluate pass-only coverage, only files under onnxruntime/core/optimizer are instrumented;

TVM (Chen et al., 2018a) is an end-to-end compiler for deploying DNNs on various platforms. In addition to 61 graph-level passes, TVM also performs up to 58 low-level optimizations to generate highly optimized target code. As a front end, ONNX models will be converted into TVM’s graph-level IR to perform further optimization. TVM also has a much higher coverage upper limit (i.e., 116k) than ONNXRuntime (i.e., 65k) given its higher capability/complexity. For pass-only instrumentation, we consider files in all transfroms folders.

TensorRT (NVIDIA, 2021) is a compiler and runtime highly optimized for NVIDIA GPUs and has been used by more than 350k developers across 27.5k companies. Since TensorRT is closed-sourced, we exclude it for coverage evaluation.

Experimental configuration. The testbed hardware configurations include: 1) Intel 10700k CPU (16 threads); 2) 64 GB memory (3200 Mhz); and 3) 2TB NVMe SSD. The operating system is Ubuntu 20.04 and targeted DL systems are compiled by Clang 14 under release mode. Except that we performed bug findings on various latest compiler versions over the last tenvspace months, the default software versions used in evaluation are: ONNXRuntime v1.12 (c556f5), TVM v0.8 (9ab3a1), TensorRT v8.4 and PyTorch v1.13 (dev20220615).

When evaluating NNSmith, for Algorithm 1 we choose between forward and backward at every insertion randomly with equal probability. For the binning approach we use k=7k=7 bins (§3.2) to ensure a decent amount of attribute diversity while keeping the models small for fuzzing efficiency. For the gradient search, the initial learning rate is set to be 0.5, ϵ\epsilon in the tensor inequality loss function is set to 10−1010^{-10}. While LEMON does not explicitly control the graph sizes (since it mutates existing models), we set the default generated graph size of NNSmith and GraphFuzzer to be 10. For coverage evaluation, we run fuzzers for 4 hours by default (following Tzer (Liu et al., 2022)) as we observe that code coverage curves generally converge before that point (e.g., as shown in Figure 4).

2. End-to-end Coverage Efficiency

We first compare NNSmith with our graph-level baselines (i.e., GraphFuzzer and LEMON) in terms of code coverage on TVM and ONNXRuntime (since TensorRT is closed-sourced). Figure 4 shows the coverage growth (y axis) over four hours (x axis). As is shown in the Figure, NNSmith beats the 2nd-best baseline (i.e., GraphFuzzer) by 1.8×\times on ONNXRuntime and by 1.08×\times on TVM. NNSmith also achieves a decent percentage of total coverage, i.e., 17.9% on ONNXRuntime and 18.6% on TVM Note that it is unlikely for NNSmith to achieve perfect overall coverage as there are many other irrelevant components related to debugging, auto-tuning (Zheng et al., 2020; Chen et al., 2018b), etc. For instance, existing Linux kernel fuzzers (Kim et al., 2020) can only achieve 0.8-10.5% coverage.. Figure 5 further shows the number of generated test cases (x axis) within 4 hours and their accumulated total coverage (y axis, consistent to Figure 4). We can observe that with fewer test cases generated within the same time limit (mainly due to the overhead incurred by constraint solving), NNSmith can still achieve higher coverage than the 2nd-best baseline (i.e., GraphFuzzer), indicating that NNSmith can generate higher-quality test cases. It is also worth noting that LEMON is the slowest technique (e.g., up to 103×\times slower than NNSmith). The reason is that LEMON mutates real-world models which can be very costly to run. We also have similar observations on the pass-only coverage. For example, as shown in Figure 6, NNSmith outperforms GraphFuzzer by 1.85×\times on ONNXRuntime and 1.09×\times on TVM, showing its effectiveness for testing compiler transformation passes.

Another interesting observation is that NNSmith’s coverage improvement on TVM is relatively smaller than that on ONNXRuntime (1.08×\times v.s. 1.8×\times). This can be inferred by the difference in their fundamental designs. While ONNXRuntime implements over 130 optimization files targeting various specific graph patterns, TVM’s graph-level optimization is more general. For example, TVM’s operator fusion does not check specific operator types, but high-level operator properties such as injective, reduce, etc. Therefore, TVM’s coverage is less sensitive to the diversity of generated graph patterns.

To show the unique coverage for each studied technique, Figure 7 further breaks down the coverage sets of different fuzzers through Venn diagrams (Wikipedia contributors, 2022). It shows that NNSmith can achieve much higher unique coverage than the 2nd-best baseline (i.e., LEMON), e.g., 32.7×\times higher on ONNXRuntime and 10.8×\times higher on TVM. Despite that GraphFuzzer beats LEMON in total coverage, LEMON contrastingly outperforms GraphFuzzer in unique coverage. This is because LEMON has a different design from NNSmith and GraphFuzzer: it mutates existing real-world models rather than generating new models from scratch, creating different model patterns. Please note that we omitted the unique coverage distribution analysis for pass-only files as it follows a similar pattern as Figure 7.

Figure 8 also compares NNSmith against Tzer on TVM (as Tzer is specifically designed for TVM). On all TVM files, NNSmith as a general graph-level fuzzer, can outperform state-of-the-art IR-level TVM-specific fuzzer by 1.4×\times in total coverage and 13×\times in unique coverage. Interestingly, while other graph-level baselines can at most exclusively cover 117 branches (i.e., LEMON in Figure 7(b)), Tzer has an unique coverage of 461. This is because Tzer directly manipulates low-level IR and some low-level operations are not exposed at the graph level. Moreover, in terms of pass-only coverage, NNSmith outperforms Tzer even more, e.g., by 123×\times in unique coverage, demonstrating the superiority of graph-level fuzzing.

3. Ablation Study

Attribute binning. Figure 9 evaluates the effectiveness of attribute binning from the perspective of redundancy. Note that for implementation convenience we use the type system from TVM’s Relay IR (parsed from ONNX models) to distinguish operators.It shows that within 4 hours, our binning approach achieves 2.07×\times unique operator instances, which are distinguished by input types and operator attributes.

Turning to system coverage, as shown in Figure 10, attribute binning improves the unique branch coverage by 2.2×\times for ONNXRuntime (Figure 10(a)) and 1.8×\times for TVM (Figure 10(b)). The total coverage improvement is relatively subtle (up to 2.3%) as the binning approach aims at covering the hard-to-hit branches whose proportion is expected to be minor. For example, simply importing TVM’s libraries with “import tvm” can hit 4015 branches but those branches are unlikely to have bugs.

Gradient guidance. Figure 11 evaluates the effectiveness of three input/weight searching methods: 1) Sampling: randomly initializing test case values; 2) Gradient (Proxy Deriv.): searching values via the full gradient-based approach; and 3) Gradient: method two without proxy derivatives. The experiment is conducted on three model groups, each of which contains 512 models of 10, 20 and 30 nodes respectively. Every model has at least one vulnerable operator. The Sampling baseline randomly samples values from the range of $whichisempiricallyobtainedselectingthebestonefromvarioustestedranges.Forfairness,allmethodsrunonthesamegroupsofmodelswiththesameinitialweights/inputsgeneratedbytheSamplingbaseline.Weassigndifferentper−modelsearchingtimeouts(i.e.,which is empirically obtained selecting the best one from various tested ranges. For fairness, all methods run on the same groups of models with the same initial weights/inputs generated by the Sampling baseline. We assign different per-model searching timeouts (i.e.,i\times 8mswherems wherei\in)toeachmethodandobservetheratioofmodelswithnumeric−validinputs/weights(y−axis)overgroup−wideaveragesearchingtime(x−axis).Figure11showsthatourfullgradientsearchimprovesthenumericalvalidityofSamplingby1.16−1.34) to each method and observe the ratio of models with numeric-valid inputs/weights (y-axis) over group-wide average searching time (x-axis). Figure 11 shows that our full gradient search improves the numerical validity of Sampling by 1.16-1.34\times$ as the node size/difficulty grows. Also, the proxy derivative mechanism consistently helps our gradient search achieve higher success rate within shorter amount of time.

We also observe that searching time is negligible compared with model generation time, e.g., generating a 10-node model costs 83ms on average while our gradient-based searching only takes 3.5ms (4.2%) to achieve a success rate of 98%.

4. Bug Study

To date, NNSmith has uncovered 72 new bugs as shown in Table 3, where 58 have been confirmed and 51 have been fixed. Others are awaiting developer responses. Interestingly, in addition to compiler bugs, since NNSmith generates models through PyTorch ONNX exporter (§4), it also found 10 conversion bugs in PyTorch as a by-product. Among the bugs we found, 17 are semantic bugs (result inconsistencies with PyTorch) and 55 are crash bugs (segmentation faults or exceptions). In total, there are 43 transformation bugs in ONNXRuntime (10), TVM (29) and TensorRT (4), accounting for the majority of the detected bugs We classify bugs first based on code inspection (when possible); otherwise, we classify a bug as transformation bug if its individual operators cannot reproduce the issue separately.. We found that most of these were optimization bugs: of the 27 fixed transformation bugs we found, 21 are optimization bugs (and the remaining one is an unclassified bug in TensorRT whose code is not available).

Of the 72 bugs we found, 49 bugs cannot be triggered using the algorithms implemented by LEMON or GraphFuzzer. Of these 31 are transformation bugs and 14 are conversion bugs. LEMON’s algorithms can trigger at most 17 of all bugs we found, while GraphFuzzer’s algorithms can trigger at most 23 of these. The core difference is that these prior approaches limit how non-shape preserving operators are connected in the graph, thus limiting graph diversity. In addition to this theoretical analysis, we also evaluated all tools by running them for four hours under the same setting (e.g., all on the default compiler versions as shown in § 5.1), NNSmith triggers 38 unique crashes (by error messages) for ONNXRuntime and 13 for TVM, while LEMON triggers none and GraphFuzzer only triggers 1 crash for each of ONNXRuntime and TVM. For instance, the only ONNXRuntime bug detected by GraphFuzzer is the wrong fusion to a double-precision ReLU-Clip connection (element-wise and thus shape-preserving).

We next describe transformation and conversion bugs we found by illustrating prominent bug patterns with examples. We use ★\bigstar to denote bugs exclusively found by NNSmith.

Wrong layout analysis: Memory layout optimizations in TVM first rewrite layouts of the most beneficial operators (e.g., Conv2d) to efficient ones and then let remaining operators adapt changed layouts. We found 7 layout transformation bugs★ in TVM, related to non-shape-preserving operators including broadcasting, reduce and slicing, which cannot be handled by prior work. For example, TVM can rewrite NCHW Conv2d to the SIMD-friendly NC4\frac{C}{4}HW4c layout (NCHW4c for short), by packing every 4 elements on C to the new sub-dimension (4c). However, using this optimization when the Conv2d is followed by a Slice operator whose stride for C is greater than one causes TVM to crash. GraphFuzzer cannot find this bug because to ensure shape alignment it always uses a stride of 1.

Integer type mismatch: DL compilers, like traditional compilers (e.g., LLVM (Lattner, 2002)), leverage IRs to simplify optimization. IR type mismatch can happen if one pass makes wrong assumption for the IR being transformed. This is especially a pain for TVM: we found 9 bugs★ stopping the compilation due to int32-int64 mismatch and one core TVM developer also admits that “TVM has a pretty fragile system of using i32 vs i64; I personally experienced it a few times before…”.int64 is often introduced by shape-related operators (e.g., shape attributes of Reshape and BroadcastTo), which are not supported by prior work as they cannot handle those complicated shape constraints. Since our first bug report on such issues, there have been 12 fixes (7 from us and 5 from followers) within 5 months to resolve similar issues, one of which even blocked models in production. Interestingly, a bug we found also helped the developers find another bug that had previously been diagnosed as the outcome of a flaky test (Luo et al., 2014).

Conversion bugs. Wrong scalar handling: We found 6 crash bugs★ triggered when TVM imports reduce-like operators with a scalar input. Since these operators are not shape-preserving, prior work cannot trigger such bugs. Similarly in PyTorch, when exporting Log2 with a scalar input, the exporter mistakenly sets its output to a rank-1 tensor instead of a scalar, causing a semantic issue. A few days after our report, developers identified 37 other similar bugs. Concurrently, NNSmith also identified a subset of these bugs, but in our evaluation we only treat the first bug (Log2) as one found by NNSmith.

Wrong broadcasting: Given a 3-way broadcasting operationWhere(C1×1,T3×1,F2)(C_{1\times 1},T_{3\times 1},F_{2}), a TVM bug★ causes the lower-ranked tensor F2F_{2} being ignored during shape inference, resulting in the wrongly inferred shape 3×13\times 1, which should be 3×23\times 2. This incurs a compiler failure in later phases. Another TVM bug★ causes an import failure to MatMul with single-rank broadcasting (one input is a vector) and notably, one month after our bug report, real-world TVM users also encountered such issues and pushed for its fix, showing that NNSmith can synthesize real-world model patterns. Prior work cannot detect them since their design are incompatible with broadcasting operations.

Data type mismatch: Operators’ data type supports vary by ONNX versions, which are often mishandled. For example, PyTorch can mistakenly (and silently) export Clip whose data type is int32 which is not supported by ONNX version 11. Such ill-formed models will be rejected by most compilers; however, it can also be mistakenly compiled by TensorRT, producing unexpected model outputs (i.e., semantic bugs in TensorRT), due to the wrongly interpreted attributes.

False alarms. As we discussed in the introduction, floating point semantics (Priest, 1992; Overton, 2001) mean that even correct optimizations can lead to scenarios where an optimized model’s output differs from the reference output. Consequently, we check output equivalence by checking that the distance between model outputs,when scaled by their overall magnitude is small. However, in some cases valid optimizations can lead to a large relative change in outputs and produce false alarms. For example, when feeding the Sigmoid with a large value, the optimized output can be 1 whereas the reference one is less than (though very close to) 11. When it provides the input to a Floor operator, the optimized output will differ from the reference output by 11, To reduce false alarms, we use a high error tolerance in comparison. In addition, false positives share similar structural patterns (e.g., Sigmoid followed by Floor and Equal for float-pointing inputs) that we can easily filter. Thus it did not cause large trouble for us.

Related Work

Since the first proposal of fuzzing (Miller et al., 1990), various techniques have been proposed for fuzzing systems of different application domains (Boehme et al., 2021; Li et al., 2018; Manès et al., 2019; Zou et al., 2021; Trippel et al., 2021; Dewey et al., 2014; Luo and Demsky, 2021; Liu et al., 2021; Neal et al., 2021; Theodoridis et al., 2022). In this section, we mainly talk about the most closely related work in DL system fuzzing and compiler fuzzing.

In recent years, a number of techniques have been proposed to test DL libraries and compilers. As one of the first techniques in this direction, CRADLE (Marcozzi et al., 2019) directly runs existing DNN models on different DL libraries to detect potential inconsistencies via differential testing.Later on, AUDEE (Guo et al., 2020) and LEMON (Wang et al., 2020) further extend CRADLE by applying search-based mutation strategies on the DNN models and their inputs to cover more library code. While AUDEE mainly focuses on mutating layer parameters and weight/input tensors, LEMON further applies more advanced mutation rules, including layer deletions/additions. Meanwhile, to ensure correctness of generated models, LEMON (Wang et al., 2020) only mutates type-preserving operators (or blocks of operators) from the real-world models, to avoid handling type constraints.However, there are many non-shape-preserving operator types, e.g., even the commonly used Conv2d cannot be completely handled by LEMON. More recently, GraphFuzzer (Luo et al., 2021) allows a slightly larger operator search space using padding/slicing to align unmatched tensor shapes and also specifically controls the attributes of shape-changing operator types to create shape-preserving instances (e.g., Conv2d with kernel size/stride of 1). However, this design still substantially limits model diversity (as demonstrated in §2.3). The very recent (and concurrent) Muffin work (Gu et al., 2022) shares a similar limitation as GraphFuzzer: it uses “reshaping” layers to align tensor shapes during model generation; in addition, Muffin focuses on finding bugs in traditional DL libraries rather than DL compiler bugs. In this work, we aim to support more diverse/valid model generation for DL compiler fuzzing via a fundamentally different design powered by symbolic constraint solving (Cadar and Sen, 2013) and gradient-driven search.

To complete DL system testing at the model level, researchers have also proposed DL system fuzzing techniques focusing on directly generating or manipulating the low-level model IRs (Pankratz, 2020; Liu et al., 2022). TVMFuzz (Pankratz, 2020) aims to automatically generate arbitrary low-level IRs based on a set of predefined grammar rules for fuzzing the popular TVM compiler (Chen et al., 2018a). The more recent Tzer work (Liu et al., 2022) leverages coverage feedback to perform joint mutation of both the low-level IR and optimization passes for TVM. While Tzer has shown promising results over TVMFuzz, the low-level IR mutation adopted by Tzer can hardly test the graph-level optimizations widely adopted by various DL compilers (as shown in §5.2).

In recent years, researchers have also investigated techniques to fuzz each DL library API in isolation. Since DL APIs are usually exposed in Python, a dynamically typed language, prior techniques, such as Predoo (Zhang et al., 2021), require users to manually set up the function arguments, and can only be evaluated on a limited number of APIs. To address this challenge, FreeFuzz (Wei et al., 2022) dynamically traces API executions from various sources (including documents, developer tests, and model zoos), and generates new tests by mutating traced inputs. More recently, DeepREL (Deng et al., 2022) aims to automatically infer relational APIs (e.g., APIs that return the same values/statuses when given the same inputs), and then leverages such API relations as test oracle for catching more bugs than FreeFuzz.While such API-level testing techniques are adequate for testing first-generation DL libraries (§2.1), they can hardly find bugs in graph-level optimizations (e.g., 86% of the transformation bugs detected by NNSmith require multiple operators to trigger).

2. Compiler Fuzzing

As one of the most widely studied compiler fuzzing approaches in the literature (Marcozzi et al., 2019), grammar-based techniques (such as Csmith (Yang et al., 2011), jsfunfuzz (Security, 2007), and LangFuzz (Holler et al., 2012)) aim to generate syntactically valid input programs acceptable by the underlying compilers. While effective, it is hard for grammar-based techniques to ensure the semantic correctness of the generated programs to cover deep code paths, and highly specialized analyses have to be employed for specific languages. Therefore, various mutation-based techniques (Le et al., 2014; Donaldson et al., 2017; Sun et al., 2016; Le et al., 2015; Zhang et al., 2017) have also been proposed for fuzzing compilers via mutating existing seed input programs.Moreover, given the advances in DL, researchers have also proposed learning-based techniques for compiler fuzzing. DeepSmith (Cummins et al., 2018) and DeepFuzz (Liu et al., 2019) directly leverage recurrent neural networks (RNNs) to generate test programs from scratch, while Montage (Lee et al., 2020) performs mutation-based fuzzing, and replaces code snippets of the seed programs with new code fragments generated by RNNs. More recently, researchers have also leveraged the advanced pre-trained language models (e.g., GPT (Brown et al., 2020)) for more powerful test program generation for compiler fuzzing (Ye et al., 2021). Such existing compiler fuzzing techniques can be potentially applied to the low-level IRs (C-like) for fuzzing DL compilers (Liu et al., 2022). However, they can be hardly directly applied for graph-level DL compiler fuzzing, and our study has also shown the superiority of NNSmith over state-of-the-art IR-level DL compiler fuzzer.

Conclusion

NNSmith is a tool for generating diverse and valid test cases for deep learning compilers. It creates abstract operator models to ensure the validity of the generated models, and further utilizes incremental graph generation and attribute binning to ensure its diversity. To avoid false alarms and bug escapes, NNSmith leverages gradient search to find inputs that do not introduce NaN/Inf in the computation. NNSmith is easily extensible to support new operators with few lines of code. Lastly, NNSmith is implemented to generate models in the popular format ONNX and is readily applicable to any systems with ONNX support. To date NNSmith has found 72 new bugs in TVM, TensorRT, ONNXRuntime, and PyTorch, 58 of which have been confirmed or fixed, demonstrating its effectiveness.

Acknowledgments

We thank the ASPLOS reviewers for their insightful comments. We also thank Yuanyi Zhong, Lingfan Yu and Leyuan Wang for insightful discussions in the early stages of the project, Jinjun Peng for helping open-source the project, and the the NYU IT High Performance Computing group for providing computing resources. This work was partially supported by the National Science Foundation grants CCF-2131943 and CCF-2141474, a Google research award, a Meta research award, an AMD research award, and a gift from Microsoft Corporation.

Appendix A Artifact Appendix

The artifact contains evidence of bug finding, source code of NNSmith’s prototype, and user-friendly HTML documentation for re-generating the results. Specifically, it includes (1) links to bugs reported by the authors as real-world bug finding evidence, and (2) scripts and code to re-generate main results in § 5. To make artifact evaluation as simple as possible, our artifact is packaged into a pre-built docker image, along with a detailed and friendly HTML documentation. To fully evaluate the artifact, a X86-CPU platform with docker access is needed, with approximately 21 hours of machine time and 1 hour of manual inspection time.

A.2. Artifact check-list (meta-information)

Metrics: C++ source-level branch coverage.

How much disk space required (approximately)?: 256GB.

How much time is needed to prepare workflow (approximately)?: A few minutes to install and import the docker container image.

How much time is needed to complete experiments (approximately)?: About 21 hours of machine time and 1 hour of manual inspection time.

Code licenses (if publicly available)?: Apache-2.

Archived (provide DOI)?: 10.5281/zenodo.7222132

A.3. Description

The artifact can be downloaded from https://zenodo.org/record/7222132.

A.3.2. Hardware dependencies.

A computer with X86 CPU and disk space of over 256 gigabytes.

A.3.3. Software dependencies.

A.4. Installation

There are two common ways to install the docker image:

To directly install the docker image from the Docker Hub (https://hub.docker.com/repository/docker/ganler/nnsmith-asplos23-ae)repository: docker pull ganler/nnsmith-asplos23-ae

To import the image locally from the Zenodo repository (https://zenodo.org/record/7222132):

export IMG=ganler/nnsmith-asplos23-ae:latest

cat nnsmith-ae.tar | docker import - $IMG

A.5. Experiment workflow

Please open html/index.html in your browser or use the online documentation (http://nnsmith-asplos.rtfd.io/) for detailed installation and evaluation steps.

The overall logical workflow of experiments includes:

Running NNSmith and baselines on instrumented TVM and ONNXRuntime for 4 hours each to get code coverage reports.

Visualize coverage in coverage trends and Venn diagram.

A.6. Evaluation and expected results

All instructions and steps to reproduce our experimental results are in the artifact documentation (html/index.html or http://nnsmith-asplos.rtfd.io/).

The steps for main experiments are included in the “Evaluating artifact” chapter which re-generates results in § 5.2 and § 5.4. We also include instructions to re-generate non-main experiments (i.e., ablation study in § 5.3) in the “Read more” chapter.

References