Internet-of-Things (IoT) edge devices have limited resources in terms of area and power. Machine Learning based intelligent filtering can be effective in reducing the data footprint. In this work, we report a feasibility study of using decision trees (DTs) on the edge. The main contribution of this work is to demonstrate that decision trees are equally effective compared to popular neural networks (multi-layer perceptrons). We trained four datasets (Iris, Heart Disease, Breast Cancer, and Credit Card) with supervised decision tree-based learning with accuracy comparable to that of MLPs. We synthesized the DTs to gate-level implementation with the Synopsys Design Compiler in 32 nm CMOS technology node. Compared to MLP implementations, DTs can save approximately 97-98% in both area and power.

For memristive crossbar arrays, currently, no high-level design validation and early space exploration tools exist in the literature. Such tools are essential to quickly verify the design functionality as well as compare design alternatives in terms of power and performance. In this work, we propose a VHDL-based framework that enables us to quickly perform behavioral simulation as well as estimate dynamic energy consumption and speed of any large memristive crossbar array. We propose a high-level (VHDL) model of a memristor based on which crossbar architectures can be modeled. The individual memristor model is embedded with power and delay numbers obtained from a detailed memristor model. We demonstrate the framework for MAGIC-style memristive crossbars. We validate the framework against detailed Verilog-A based model on fifteen combinational benchmarks. For the single row model, we obtained 153x simulation speedup over HSPICE, average estimation errors of 6.64% and 0% for dynamic energy consumption and cycle-time, respectively. For the transpose model, we obtained average estimation errors of 5.51% and 10.90% for dynamic energy consumption and cycle-time, respectively. We also extend our framework to support another prominent logic style and validate through a case study. The proposed framework can be easily extended to other emerging technologies.

This paper reports our experience applying lightweight formal methods to validate the correctness of ShardStore, a new key-value storage node implementation for the Amazon S3 cloud object storage service. By "lightweight formal methods" we mean a pragmatic approach to verifying the correctness of a production storage node that is under ongoing feature development by a full-time engineering team. We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure correctness as both software and its specification evolve over time. Our approach decomposes correctness into independent properties, each checked by the most appropriate tool, and develops executable reference models as specifications to be checked against the implementation. Our work has prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems, and has been extended by non-formal-methods experts to check new features and properties as ShardStore has evolved.

The range of verification problems that can be solved with logic model checking tools has increased significantly in the last few decades. This increase in capability is based on algorithmic advances and new theoretical insights, but it has also benefitted from the steady increase in processing speeds and main memory sizes on standard computers. The steady increase in processing speeds, though, ended when chip-makers started redirecting their efforts to the development of multicore systems. For the near-term future, we can anticipate the appearance of systems with large numbers of CPU cores, but without matching increases in clock-speeds. We will describe a model checking strategy that can allow us to leverage this trend and that allows us to tackle significantly larger problem sizes than before.

Reportedly, supercomputer designer Seymour Cray once said that he would sooner use two strong oxen to plow afield than a thousand chickens. Although this is undoubtedly wise when it comes to plowing afield, it is not so clear for other types of tasks. Model checking problems are of the proverbial "search the needle in a haystack" type. Such problems can often be parallelized easily. Alas, none of the usual divide and conquer methods can be used to parallelize the working of a model checker. Given that it has become easier than ever to gain access to large numbers of computers to perform even routine tasks it is becoming more and more attractive to find alternate ways to use these resources to speed up model checking tasks. This paper describes one such method, called swarm verification.

Most flight software testing at the Jet Propulsion Laboratory relies on the use of hand-produced test scenarios and is executed on systems as similar as possible to actual mission hardware. We report on a flight software development effort incorporating large-scale (biased) randomized testing on commodity desktop hardware. The results show that use of a reference implementation, hardware simulation with fault injection, a testable design, and test minimization enabled a high degree of automation in fault detection and correction. Our experience will be of particular interest to developers working in domains where on-time delivery of software is critical (a strong argument for randomized automated testing) but not at the expense of correctness and reliability (a strong argument for model checking, theorem proving, and other heavyweight techniques). The effort spent in randomized testing can prepare the way for generating more complete confidence using heavyweight techniques.

Abstract We propose tackling a “mini challenge” problem: a nontrivial verification effort that can be completed in 2–3 years, and will help establish notational standards, common formats, and libraries of benchmarks that will be essential in order for the verification community to collaborate on meeting Hoare’s 15-year verification grand challenge. We believe that a suitable candidate for such a mini challenge is the development of a filesystem that is verifiably reliable and secure. The paper argues why we believe a filesystem is the right candidate for a mini challenge and describes a project in which we are building a small embedded filesystem for use with flash memory.

This article presents a design for the Denali-2 superoptimizer, which will generate minimum-instruction-length machine code for realistic machine architectures using automatic theorem-proving technology: specifically, using E-graph matching (a technique for pattern matching in the presence of equality information) and Boolean satisfiability solving.This article presents a precise definition of the underlying automatic programming problem solved by the Denali-2 superoptimizer. It sketches the E-graph matching phase and presents a detailed exposition and proof of soundness of the reduction of the automatic programming problem to the Boolean satisfiability problem.

A utility environment is dynamic in nature. It has to deal with a large number of resources of varied types, as well as multiple combinations of those resources. By embedding operator and user level policies in resource models, specifications of composite resources may be automatically generated to meet these multiple and varied requirements. The paper describes a model for automated policy-based construction of complex environments. We pose the policy problem as a goal satisfaction problem that can be addressed using a constraint satisfaction formulation. We show how a variety of construction policies can be accommodated by the resource models during resource composition. We are implementing this model in a prototype that uses CIM as the underlying resource model and exploring issues that arise as a result of that implementation.

This paper provides a preliminary report on a new research project that aims to construct a code generator that uses an automatic theorem prover to produce very high-quality (in fact, nearly mathematically optimal) machine code for modern architectures. The code generator is not intended for use in an ordinary compiler, but is intended to be used for inner loops and critical subroutines in those cases where peak performance is required, no available compiler generates adequately efficient code, and where current engineering practice is to use hand-coded machine language. The paper describes the design of the superoptimizer, and presents some encouraging preliminary results.

Typically, program design involves constructing a program P that implements a given specification S; that is, the set P of executions of P is a subset of the set S of executions satisfying S. In many cases, we seek a program P that not only implements S, but for which P = S. Then, every execution satisfying the specification is a possible execution of the program; we then call P maximal for the specification S. We argue that maximality is an important criterion in the context of designing concurrent programs because it disallows implementations that do not exhibit enough concurrency. In addition, a maximal solution can serve as a basis for deriving a variety of implementations, each appropriate for execution on a specific computing platform.This paper also describes a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs, there is no need to appeal to branching time logics; we employ a fragment of linear temporal logic for our proofs. The method results in concise proofs of maximality for several non-trivial examples. The method may also serve as a guide in constructing maximal programs.

Abstract. Typically, program design involves constructing a program P that implements a given specification S ; that is, the set ${\overline P}$ of executions of P is a subset of the set ${\overline S}$ of executions satisfying S . In many cases, we seek a program P that not only implements S , but for which ${\overline P}$ = ${\overline S}$ . Then, every execution satisfying the specification is a possible execution of the program; we then call P maximal for the specification S . We argue that maximality is an important criterion in the context of designing concurrent programs because it disallows implementations that do not exhibit enough concurrency. In addition, a maximal solution can serve as a basis for deriving a variety of implementations, each appropriate for execution on a specific computing platform. This paper also describes a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs, there is no need to appeal to branching time logics; we employ a fragment of linear temporal logic for our proofs. The method results in concise proofs of maximality for several non-trivial examples. The method may also serve as a guide in constructing maximal programs.

A large fraction of scientific and engineering computations involve sparse matrices. While dense matrix computations can be parallelized relatively easily, sparse matrices with arbitrary or irregular structure pose a real challenge to designers of highly parallel machines. A recent paper by N.K. Karmarkar (1991) proposed a new parallel architecture for sparse matrix computations based on finite projective geometries. Mathematical structure of these geometries plays an important role in defining the interconnections between the processors and memories in this architecture, and also aids in efficiently solving several difficult problems (such as load balancing, data-routing, memory-access conflicts, etc.) that are encountered in the design of parallel systems. The authors discuss some of the key issues in the system design of such a machine, and show how exploiting the structure of the geometry results in an efficient hardware implementation of the machine. They also present circuit designs and simulation results for key elements of the system: a 200 MHz pipelined memory; a pipelined multiplier based on an adder unit with a delay of 2 ns; and a 500 Mbit/s CMOS input/output buffer.>