Automated Machine Learning (AutoML) is an upcoming field in machine learning (ML) that searches the candidate model space for a given task, dataset and an evaluation metric and returns the best performing model on the supplied dataset as per the given metric. AutoML not only reduces the man-power and expertise needed to develop ML models but also decreases the time-to-market for ML models substantially. In Walmart, we have designed an enterprise-scale AutoML frame-work called WALTS to meet the rising demand of employing ML in the retail business, and thus help democratize ML within our organization. In this work, we delve into the design of WALTS from both algorithmic and architectural perspectives. Specfiically, we elaborate on how we explore models from a pool of candidates along with describing our choice of technology stack to make the whole process scalable and robust. We illustrate the process with the help of a business use-case, and finally underline how WALTS has impacted our business so far.

Reducing the number of failures in a production system is one of the most challenging problems in technology driven industries, such as, the online retail industry. To address this challenge, change management has emerged as a promising sub-field in operations that manages and reviews the changes to be deployed in production in a systematic manner. However, it is practically impossible to manually review a large number of changes on a daily basis and assess the risk associated with them. This warrants the development of an automated system to assess the risk associated with a large number of changes. There are a few commercial solutions available to address this problem but those solutions lack the ability to incorporate domain knowledge and continuous feedback from domain experts into the risk assessment process. As part of this work, we aim to bridge the gap between model-driven risk assessment of change requests and the assessment of domain experts by building a continuous feedback loop into the risk assessment process. Here we present our work to build an end-to-end machine learning system along with the discussion of some of practical challenges we faced related to extreme skewness in class distribution, concept drift, estimation of the uncertainty associated with the model's prediction and the overall scalability of the system.

Extracting texts of various shapes, sizes, and orientations from images containing multiple objects is an important problem in many contexts, especially, in connection to E-commerce. In the context of the scale at which Walmart operates, the text from an image can be a richer and more accurate source of data than human inputs and can be used in several applications such as Attribute Extraction, Offensive Text Classification, Product Matching among others. The motivation of this particular work has come from different business requirements such as flagging products whose images contain words that are non-compliant with organizational policies and building an efficient automated system to identify similar products by comparing the information contained in their respective product images and many others. Existing methods fail to address domain specific challenges like high entropy, different orientations, and small texts in product images adequately. In this work, we provide a solution that not only addresses these challenges but is also proven to work at a million image scale for various retail business units within Walmart. Extensive experimentation revealed that our proposed solution has been able to save around 30% computational cost in both the training and the inference stages.

Deep learning (DL) is one of the most prominent branches of machine learning. Due to the immense computational cost of DL workloads, industry and academia have developed DL libraries with highly-specialized kernels for each workload/architecture, leading to numerous, complex code-bases that strive for performance, yet they are hard to maintain and do not generalize. In this work, we introduce the batch-reduce GEMM kernel and show how the most popular DL algorithms can be formulated with this kernel as the basic building-block. Consequently, the DL library-development degenerates to mere (potentially automatic) tuning of loops around this sole optimized kernel. By exploiting our new kernel we implement Recurrent Neural Networks, Convolution Neural Networks and Multilayer Perceptron training and inference primitives in just 3K lines of high-level code. Our primitives outperform vendor-optimized libraries on multi-node CPU clusters, and we also provide proof-of-concept CNN kernels targeting GPUs. Finally, we demonstrate that the batch-reduce GEMM kernel within a tensor compiler yields high-performance CNN primitives, further amplifying the viability of our approach.

Google's neural machine translation (GNMT) is state-of-the-art recurrent neural network (RNN/LSTM) based language translation application. It is computationally more demanding than well-studied convolutional neural networks (CNNs). Also, in contrast to CNNs, RNNs heavily mix compute and memory bound layers which requires careful tuning on a latency machine to optimally use fast on-die memories for best single processor performance. Additionally, due to massive compute demand, it is essential to distribute the entire workload among several processors and even compute nodes. To the best of our knowledge, this is the first work which attempts to scale this application on an Intel CPU cluster. Our CPU-based GNMT optimization, the first of its kind, achieves this by the following steps: (i) we choose a monolithic long short-term memory (LSTM) cell implementation from LIBXSMM library (specifically tuned for CPUs) and integrate it into TensorFlow, (ii) we modify GNMT code to use fused time step LSTM op for the encoding stage, (iii) we combine Horovod and Intel MLSL scaling libraries for improved performance on multiple nodes, and (iv) we extend the bucketing logic for grouping similar length sentences together to multiple nodes for achieving load balance across multiple ranks. In summary, we demonstrate that due to these changes we are able to outperform Google's stock CPU-based GNMT implementation by ~2x on single node and potentially enable more than 25x speedup using 16 node CPU cluster.

Path‐based equivalence checkers (PBECs) have been successfully applied for verification of programmes from diverse domains and from various stages of high‐level synthesis. In the case of non‐equivalence, PBEC provides very little information which is not sufficient for further investigation of the two programmes being compared by some human expert. In this work, the authors show how a counter‐trace ( cTrace ) can be generated in the case of non‐equivalence reported by the PBEC. Using this cTrace , they also present a procedure to find suitable initialisation values for input variables which reveal the non‐equivalence (i.e. counter‐example) by using off‐the‐shelf satisfiability modulo theories (SMT) solvers. To aid the human expert, they also show that how they can visualise this cTrace in the control and data‐flow graph of the programmes using the graph visualisation software – Graphviz. This counter‐example and visual representation of the corresponding cTrace will be helpful in debugging the root cause of the non‐equivalence. The experimental results are encouraging.

Abstract Translation validation is an undecidable problem. Bisimulation relation based approaches, nevertheless, have been widely successful in translation validation of programs albeit with some drawbacks. These drawbacks include non-termination of the verification methodology and significant restrictions on the structures of programs to be checked for equivalence. We have developed a path based equivalence checker which propagates mismatched values over consecutive paths to alleviate these drawbacks. In this work, we show how a bisimulation relation between a program and its translated version can be constructed from the outputs of such a value propagation based equivalence checker. Moreover, none of the earlier methods that establish equivalence through construction of bisimulation relations has been shown to tackle code motions across loops; the present work demonstrates, for the first time, the existence of a bisimulation relation under such a situation.

Constructing bisimulation relations between programs as a means of translation validation has been an active field of study. The problem is in general undecidable. Currently available mechanisms suffer from drawbacks such as non-termination and significant restrictions on the structures of programs to be checked. We have developed a path extension based equivalence checking method as an alternative translation validation technique to alleviate these drawbacks. In this work, path extension based equivalence checking of programs (flowcharts) is leveraged to establish a bisimulation relation between a program and its translated version by constructing the relation from the outputs of the equivalence checker.

Compiler optimization of array-intensive programs involves extensive application of loop transformations and arithmetic transformations. Hence, translation validation of array-intensive programs requires manipulation of intervals of integers (representing domains of array indices) and relations over such intervals to account for loop transformations and simplification of arithmetic expressions to handle arithmetic transformations. A major obstacle for verification of such programs is posed by the presence of recurrences, whereby an element of an array gets defined in a statement S inside a loop in terms of some other element(s) of the same array which have been previously defined through the same statement S. Recurrences lead to cycles in the data-dependence graph of a program which make dependence analyses and simplifications (through closed-form representations) of the data transformations difficult. Another technique which works better for recurrences does not handle arithmetic transformations. In this work, array data-dependence graphs (ADDGs) are used to represent both the original and the optimized versions of the program and a validation scheme is proposed where the cycles due to recurrences in the ADDGs are suitably abstracted as acyclic subgraphs. Thus, this work provides a unified equivalence checking framework to handle loop and arithmetic transformations along with most of the recurrences -- this combination of features had not been achieved by a single verification technique earlier.

A compiler is a computer program which translates a source code into a target code, often with an objective to reduce the execution time and/or save critical resources. However, an error in the design or in the implementation of a compiler may result in software bugs in the target code obtained from that compiler. Translation validation is a formal verification approach for compilers whereby, each individual translation is followed by a validation phase which verifies that the target code produced correctly implements the source code. In this paper, we present a tool for translation validation of optimizing transformations of programs; the original and the transformed programs are modeled as Finite State Machines with Datapath having Arrays (FSMDAs) and a symbolic value propagation (SVP) based equivalence checking strategy is applied over this model to determine the correctness of the applied transformations. The tool has been demonstrated to handle uniform and non-uniform code motions, including code motions across loops, along with transformations which result in modification of control structures of programs. Moreover, arithmetic transformations such as, associative, commutative, distributive transformations, expression simplification, constant folding, etc., are also supported.

Execution of cryptographic algorithm in hardware or software usually leaves power/current traces that are dependent on the data being processed. Power analysis attacks (PAAs) have been found to be extremely effective on such systems to derive the cryptographic secrets from these traces. Therefore, countering PAAs is of great importance. In this work, a Binary Decision Diagram (BDD) based dual-rail logic circuit scheme has been developed to counter PAAs. This circuit scheme features novel pre-charge generation, voltage scaling with leakage power minimization and early propagation effect resistance mechanism. A simple synthesis algorithm for mapping given Boolean functions to such BDD based circuits is also presented. The synthesized circuits feature low power circuitry and extremely low peak power variation. Experimental results for elementary gates such as AND, OR, NOT, XOR, NAND, NOR and the Lucifer and the Present S-boxes highlight the advantages of circuits based on this scheme with respect to peak power variance, average power and average current when compared with two other techniques - DP-BDD and SDMLp. Resistance of our S-box implementations to strong differential power analysis and correlation power analysis attacks have also been experimentally demonstrated. All results have been obtained using 65nm technology.

An equivalence checking method of finite state machines with datapath based on value propagation over model paths is presented here for validation of code motion transformations commonly applied during the scheduling phase of high-level synthesis. Unlike many other reported techniques, the method is able to handle code motions across loop bodies. It consists in propagating the variable values over a path to the subsequent paths on discovery of mismatch in the values for some live variable, until the values match or the final path segments are accounted for without finding a match. Checking loop invariance of the values being propagated beyond the loops has been identified to play an important role. Along with uniform and nonuniform code motions, the method is capable of handling control structure modifications as well. The complexity analysis depicts identical worst case performance as that of a related earlier method of path extension which fails to handle code motion across loops. The method has been implemented and satisfactorily tested on the outputs of a basic block-based scheduler, a path-based scheduler, and the high-level synthesis tool SPARK for some benchmark examples.

The finite state machine with datapath (FSMD) models provide a formalism to represent any sequential behavior. Literature has many examples where this model has been successfully applied for behavioral verification of programs. All these methods, however, cannot handle an important class of programs, namely those involving arrays. This limitation is now overcome with finite state machine with datapath having arrays (FSMDA) models which are an extension of FSMD models; the corresponding equivalence checking algorithm has also been enhanced so that code motions of array-intensive behaviors can be validated. The new mechanism has been successfully tested with several examples.

Differential power analysis (DPA) attacks are the most powerful side channel attacks against cryptographic systems. In this work, a reduced ordered binary decision diagram (ROBDD) based dual rail circuit for a basic DPA resistant cell has been designed. The specialty of this cell is that the overall input current of the cell is invariant to the input combinations of data bits applied to the cell. For the first time, bottom pre-charge logic is used in the design of such a cell. The ROBDD based design minimizes both area and early propagation effect. A number of logic functions including AND, OR, XOR, NOT, NAND, NOR and also an adder, all based on the basic cell, have then been designed in a hierarchical manner. Experimental results demonstrate DPA resistance of the circuits (for example an adder) developed using this cell, outperforming other competing design with respect to peak power variance.

Loop transformation techniques along with arithmetic transformations are applied extensively on array and loop intensive behaviors in design of area/energy efficient systems in the domain of multimedia and signal processing applications. Ensuring correctness of such transformations is crucial for the reliability of the designed systems. In this paper, array data dependence graphs (ADDGs) are used to represent both the input and the transformed behaviors and the correctness of the transformations is ensured by proving equivalence of the two ADDGs. A slice-based equivalence checking method of ADDGs is proposed for this purpose. The method relies on the normalization of arithmetic expressions and some simplification rules to handle arithmetic transformations. Unlike many other reported techniques, our method is strong enough to handle several arithmetic transformations along with all kinds of loop transformations. Correctness and complexity of the method have been dealt with. Experimental results on several test cases demonstrate the effectiveness of the method.