Theorem proving demonstrates promising potential for verifying problems beyond the capabilities of SMT-solver-based verification tools. We explore and showcase the capability of Lean, an increasingly popular theorem-proving tool, in deriving the error bounds of table-based Logarithmic Number Systems (LNS). LNS reduces the number of bits needed to represent a high dynamic range of real numbers with finite precision and efficiently performs multiplication and division. However, in LNS, addition and subtraction become non-linear functions that must be approximated–typically using precomputed look-up tables. We provide the first rigorous analysis of LNS that covers first-order Taylor approximation, cotransformation techniques in-spired by European Logarithmic Microprocessor, and the errors introduced by fixed-point arithmetic involved in LNS implementations. By analyzing all error sources and deriving symbolic error bounds for each, then accumulating these to obtain the final error bound, we prove the correctness of these bounds using Lean and its Mathlib library. We empirically validate our analysis using an exhaustive Python implementation, demonstrating that our analytical interpolation bounds are tight, and our analytical cotransformation bounds overestimate between one and two bits.

Abstract Recent advances in satisfiability modulo theories have brought practical software verification within reach. The advent of the LLVM project presents a common representation which allows verification between programs written in different languages such as C and Rust. New programming languages such as Rust often have less complete standard libraries. In this work, we explore using the SMACK software verifier to check the equivalence of math library routines from the libm library and their translations into native Rust programs.

NVIDIA Tensor Cores and AMD Matrix Cores (together called Matrix Accelerators) are of growing interest in high-performance computing and machine learning owing to their high performance. Unfortunately, some of their crucial numerical attributes pertaining to departures from full IEEE floating-point compatibility are not documented. This makes it impossible to reliably port codes across these differing accelerators. This paper contributes a collection of Feature Targeted Tests for Numerical Properties that that help determine these features across five floating-point formats, four rounding modes and additional that highlight the rounding behaviors and preservation of extra precision bits. To show the practical relevance of FTTN, we design a simple matrix-multiplication test designed with insights gathered from our feature-tests. We executed this very simple test on five platforms, producing different answers: V100, A100, and MI250X produced 0, MI100 produced 255.875, and Hopper H100 produced 191.875. Our matrix multiplication tests employ patterns found in iterative refinement-based algorithms, highlighting the need to check for significant result variability when porting code across GPUs.

Porting high-performance computing (HPC) applications to lower or mixed-precision formats offers potential benefits, such as reduced computation and power consumption. However, this process presents challenges, including higher rounding errors, poor convergence, floating-point exceptions, and incurs considerable effort, particularly when leveraging low-precision hardware. Current precision-tuning approaches fail to comprehensively address these challenges and do not effectively utilize low-precision hardware.While not as accurate as converting the code to lower precision, this is a very effective tradeoff in terms of design-space search, as many precision settings may need to be explored during precision tuning.FBTuner empowers designers to confidently implement mixed precision in their projects while addressing the key challenges of porting HPC programs to lower or mixed-precision formats. We plan to demonstrate FBTuner on HPC proxy applications and demonstrate that the porting does not result in significant loss of accuracy or increase the number of iterations to attain convergence.

NVIDIA and AMD GPUs are fundamental components in contemporary high-performance systems, boosting computational capabilities in the HPC and AI fields.However, a clear understanding of the nuances in floating-point operations between these GPU variants is crucial to avoid introducing errors during software development or porting, and such clarity is currently insufficient.The complexity of this issue is amplified when considering the variety of floating-point precision options (such as FP16, FP32, etc.), floating-point formats (like standard floats, bfloats, etc.), and the different execution units (elementary units, matrix/tensor cores, etc.).As it stands, much of this information is either not well-known or is difficult to obtain. Our work aims to shed light on these areas through a pioneering testing-guided methodology that seeks to unravel many of these uncertainties.We are in the process of developing a series of tests that uncover the numerical discrepancies in elementary computing units, the built-in math libraries, and the numerical properties of matrix accelerators present in both NVIDIA (tensor cores) and AMD GPUs (matrix cores).The significance of this testing approach extends beyond current GPU models; it is designed to be forward-compatible with upcoming GPU technologies. We have already identified discrepancies as significant as 7 ulps for trigonometric functions at FP32 precision and 3 ulps at FP64 precision between NVIDIA and AMD GPUs. Additionally, our comprehensive examination has documented the behaviors of matrix cores (NVIDIA) and tensor cores (AMD), including their rounding modes (such as truncation and round-to-nearest), the extent of extra internal bits maintained (specifically, whether an additional 3 bits are retained), the handling of subnormal numbers in inputs and outputs and the FMA features in these units. This analysis spans four distinct floating-point formats and multiple GPU models, including NVIDIA’s V100, A100, H100 and AMD’s MI100 and MI250X.We believe that the information now being disclosed will reduce the risk of porting errors when codes are adapted across these different hardware platforms.

Emerging deep learning workloads urgently need fast general matrix multiplication (GEMM). Thus, one of the critical features of machine-learning-specific accelerators such as NVIDIA Tensor Cores, AMD Matrix Cores, and Google TPUs is the support of mixed-precision enabled GEMM. For DNN models, lower-precision FP data formats and computation offer acceptable correctness but significant performance, area, and memory footprint improvement. While promising, the mixed-precision computation on error resilience remains unexplored. To this end, we develop a fault injection framework that systematically injects fault into the mixed-precision computation results. We investigate how the faults affect the accuracy of machine learning applications. Based on error resilience characteristics, we offer lightweight error detection and correction solutions that significantly improve the overall model accuracy by 75% if the models experience hardware faults. The solutions can be efficiently integrated into the accelerator's pipelines.

Numerical programs that generate floating-point exceptions, such as NaNs, are inherently unreliable, as these programs can produce meaningless outputs or affect control flow. When these programs run on GPUs, one cannot rely on hardware traps to handle the exceptions, as most GPUs do not support them. Unfortunately, we must also employ black-box testing for many such GPU programs, as they are supplied as binary code only. While previous work has shown that black-box testing for triggering floating-point exceptions can be approached using Bayesian Optimization, their approach cannot handle programs with more than three inputs. We contribute a new tool, FPBOXer, which pushes up the capabilities of BO to handle over 20 inputs---this makes our contribution capable of handling realistic HPC program functions. In addition to delivering an overall 90x speedup over the previous methods, FPBOXer does not suffer from "self-inflicted" exceptions that are caused by the BO algorithm itself---something that previous tools did. This is achieved through parallel deployments of asynchronous BO searches, which has the beneficial side-effect of improving the GPU-utilization. By using FPBOXer, developers can, for the first time, find exception-causing inputs in realistic HPC programs, as we demonstrate when we apply FPBOXer to NAS, Lampps, CFD, ExaMiniMD, HPCCG, MiniFE, and BDCSVD.

Data races are egregious concurrency bugs that are especially problematic in performance-oriented GPU codes where large thread counts and multiple shared memory regions tend to exacerbate them. In this work, we present a new dynamic data-race checker called HiRace, whose key novelty is an innovative state machine designed to capitalize on the bulk-synchronous hierarchical GPU programming model. This state machine condenses an arbitrarily long access history into a constant-size state. We evaluate HiRace on a large, calibrated data-race benchmark suite. In over 3,500 studied executions of 580 CUDA kernels, 346 of which contain data races, we found HiRace to detect races missed by other tools without raising false alarms and to be more than 10 times faster on average than the current state of the art with half the memory overhead.

Floating-point exceptions occurring during numerical computations can be a serious threat to the validity of the computed results if they are not caught and diagnosed Unfortunately, on NVIDIA GPUs-today's most widely used types and which do not have hardware exception traps-this task must be carried out in software. Given the prevalence of closed-source kernels, efficient binary-level exception tracking is essential. It is also important to know how exceptions flow through the code, whether they alter the code behavior and additionally whether these exceptions can be detected at the program outputs or are killed inside program flow-paths.

Abstract Recent demand for distributed software had led to a surge in popularity in actor‐based frameworks. However, even with the stylized message passing model of actors, writing correct distributed software is still difficult. We present our work on linearizability checking in DS2, an integrated framework for specifying, synthesizing, and testing distributed actor systems. The key insight of our approach is that often subcomponents of distributed actor systems represent common algorithms or data structures (e.g., a distributed hash table or tree) that can be validated against a simple sequential model of the system. This makes it easy for developers to validate their concurrent actor systems without complex specifications. DS2 automatically explores the concurrent schedules that system could arrive at, and it compares observed output of the system to ensure it is equivalent to what the sequential implementation could have produced. We describe DS2's linearizability checking and test it on several concurrent replication algorithms from the literature. We explore in detail how different algorithms for enumerating the model schedule space fare in finding bugs in actor systems, and we present our own refinements on algorithms for exploring actor system schedules that we show are effective in finding bugs.

Coarse-grained reconfigurable accelerators (CGRAs) are a promising accelerator design choice that strikes a balance between performance and adaptability to different computing patterns across various applications domains. Designing a CGRA for a specific application domain involves enormous software/hardware engineering effort. Recent research works explore loop transformations, functional unit types, network topology, and memory size to identify optimal CGRA designs given a set of kernels from a specific application domain. Unfortunately, the impact of functional units with different precision support has rarely been investigated. To address this gap, we propose ASAP - a hardware/software co-design framework that automatically identifies and synthesizes optimal precision-aware CGRA for a set of applications of interest. Our evaluation shows that ASAP generates specialized designs 3.2X, 4.21X, and 5.8X more efficient (in terms of performance per unit of energy or area) than non-specialized homogeneous CGRAs, for the scientific computing, embedded, and edge machine learning domains, respectively, with limited accuracy loss. Moreover, ASAP provides more efficient designs than other state-of-the-art synthesis frameworks for specialized CGRAs.

Testing code for floating-point exceptions is crucial as exceptions can quickly propagate and produce unreliable numerical answers. The state-of-the-art to test for floating-point exceptions in GPUs is quite limited and solutions require the ap-plication's source code, which precludes their use in accelerated libraries where the source is not publicly available. We present an approach to find inputs that trigger floating-point exceptions in black-box GPU functions, i.e., functions where the source code and information about input bounds are unavailable. Our approach is the first to use Bayesian optimization (BO) to identify such inputs and uses novel strategies to overcome the challenges that arise in applying BO to this problem. We implement our approach in the XSCOPE framework and demonstrate it on 58 functions from the CUDA Math Library and functions from ten HPC programs. XSCOPE is able to identify inputs that trigger exceptions in about 72% of the tested functions.

Automated techniques for analyzing floating-point code for roundoff error as well as control-flow instability are of growing importance. It is important to compute rigorous estimates of roundoff error, as well as determine the extent of control-flow instability due to roundoff error flowing into conditional statements. Currently available analysis techniques are either non-rigorous or do not produce tight roundoff error bounds in many practical situations. Our approach embodied in a new tool called SEESAW employs symbolic reverse-mode automatic differentiation, smoothly handling conditionals, and offering tight error bounds. Key steps in SEESAW include weakening conditionals to accommodate roundoff error, computing a symbolic error function that depends on program paths taken, and optimizing this function whose domain may be non-rectangular by paving it with a rectangle-based cover. Our benchmarks cover many practical examples for which such rigorous analysis has hitherto not been applied, or has yielded inferior results.

This demo presents Jove, a new framework that brings the hands-on experience of teaching Automata and Computability through the popular medium of Jupyter notebooks. Jove requires no installation: it can be run straight out of its site https://github.com/ganeshutah/Jove.git by launching a chosen notebook on Google's Colab service. Students can create machines (DFA, Turing machines, etc.) in a simple markdown language, which are then translated into well-laid-out diagrams and animated for the provided user inputs. Jove's extensible animation controls build on Jupyter widgets and include interactive demos of NFA Epsilon-closure, Turing machines that perform tape updates, colored state transitions, etc. Composable commands easily achieve the construction of large machines, allowing the conversion of Regular Expressions to NFA, DFA, and minimal DFA. Python loops can administer tests on student-built machines; more advanced commands help establish formal equivalences of machines. Jove helps introduce Formal Methods through property-checking on automata, Binary Decision Diagrams, and Boolean SAT. The Jove website offers an entire semester of guided assignments (template notebooks) and videos. This demo will introduce Jove through examples that attendees can run merely by having access to a browser.

There is growing uptake of shared memory parallelism in high performance computing, and this has increased the need for data race checking during the creation of new parallel codes or parallelizing existing sequential codes. While race checking concepts and implementations have been around for many concurrency models, including tasking models such as Cilk and PThreads (e.g., the Thread Sanitizer tool), practically usable race checkers for other APIs such as OpenMP have been lagging. For example, the OpenMP parallelization of an important library (namely Hypre) was initially unsuccessful due to inexplicable nondeterminism introduced when the code was optimized, and later root-caused to a race by the then recently developed OpenMP race checker Archer [2]. The open-source Archer now enjoys significant traction within several organizations.

Automated techniques for rigorous floating-point round-off error analysis are a prerequisite to placing important activities in HPC such as precision allocation, verification, and code optimization on a formal footing. Yet existing techniques cannot provide tight bounds for expressions beyond a few dozen operators-barely enough for HPC. In this work, we offer an approach embedded in a new tool called SATIHE that scales error analysis by four orders of magnitude compared to today's best-of-class tools. We explain how three key ideas underlying SATIHE helps it attain such scale: path strength reduction, bound optimization, and abstraction. SATIHE provides tight bounds and rigorous guarantees on significantly larger expressions with well over a hundred thousand operators, covering important examples including FFT, matrix multiplication, and PDE stencils.

We present FailAmp, a novel LLVM program transformation algorithm that makes programs employing structured index calculations more robust against soft errors. Without FailAmp, an offset error can go undetected; with FailAmp, all subsequent offsets are relativized, building on the faulty one. FailAmp can exploit ISAs such as ARM to further reduce overheads. We verify correctness properties of FailAMP using an SMT solver, and present a thorough evaluation using many high-performance computing benchmarks under a fault injection campaign. FailAmp provides full soft-error detection for address calculation while incurring an average overhead of around 5%.

We present FPD etect , a low-overhead approach for detecting logical errors and soft errors affecting stencil computations without generating false positives. We develop an offline analysis that tightly estimates the number of floating-point bits preserved across stencil applications. This estimate rigorously bounds the values expected in the data space of the computation. Violations of this bound can be attributed with certainty to errors. FPD etect helps synthesize error detectors customized for user-specified levels of accuracy and coverage. FPD etect also enables overhead reduction techniques based on deploying these detectors coarsely in space and time. Experimental evaluations demonstrate the practicality of our approach.

We present a tool called DiffTrace that approaches debugging via whole program tracing and diffing of typical and erroneous traces. After collecting these traces, a user-configurable front-end filters out irrelevant function calls and then summarizes loops in the retained function calls based on state-of-the-art loop extraction algorithms. Information about these loops is inserted into concept lattices, which we use to compute salient dissimilarities to narrow down bugs. DiffTrace is a clean start that addresses debugging features missing in existing approaches. Our experiments on an MPI/OpenMP program called ILCS and initial measurements on LULESH, a DOE miniapp, demonstrate the advantages of the proposed debugging approach.

Successful HPC software applications are long-lived. When ported across machines and their compilers, these applications often produce different numerical results, many of which are unacceptable. Such variability is also a concern while optimizing the code more aggressively to gain performance. Efficient tools that help locate the program units (files and functions) within which most of the variability occurs are badly needed, both to plan for code ports and to root-cause errors due to variability when they happen in the field. In this work, we offer an enhanced version of the open-source testing framework FLiT to serve these roles. Key new features of FLiT include a suite of bisection algorithms that help locate the root causes of variability. Another added feature allows an analysis of the tradeoffs between performance and the degree of variability. Our new contributions also include a collection of case studies. Results on the MFEM finite-element library include variability/performance tradeoffs, and the identification of a (hitherto unknown) abnormal level of result-variability even under mild compiler optimizations. Results from studying the Laghos proxy application include identifying a significantly divergent floating-point result-variability and successful root-causing down to the problematic function over as little as 14 program executions. Finally, in an evaluation of 4,376 controlled injections of floating-point perturbations on the LULESH proxy application, we showed that the FLiT framework has 100% precision and recall in discovering the file and function locations of the injections all within an average of only 15 program executions.

Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide very pessimistic overestimates, causing unnecessary verification failure. We have developed a new approach called Symbolic Taylor Expansions that avoids these problems, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. FPTaylor emits per-instance analysis certificates in the form of HOL Light proofs that can be machine checked. In this article, we present the basic ideas behind Symbolic Taylor Expansions in detail. We also survey as well as thoroughly evaluate six tool families, namely, Gappa (two tool options studied), Fluctuat, PRECiSA, Real2Float, Rosa, and FPTaylor (two tool options studied) on 24 examples, running on the same machine, and taking care to find the best options for running each of these tools. This study demonstrates that FPTaylor estimates round-off errors within much tighter bounds compared to other tools on a significant number of case studies. We also release FPTaylor along with our benchmarks, thus contributing to future studies and tool development in this area.

The detection and elimination of data races in largescale OpenMP programs is of critical importance. Unfortunately, today's state-of-the-art OpenMP race checkers suffer from high memory overheads and/or miss races. In this paper, we present SWORD, a data race detector that significantly improves upon these limitations. SWORD limits the application slowdown and memory usage by utilizing only a bounded, user-adjustable memory buffer to collect targeted memory accesses. When the buffer fills up, the accesses are compressed and flushed to a file system for later offline analysis. SWORD builds on an operational semantics that formally captures the notion of concurrent accesses within OpenMP regions. An offline race checker that is driven by these semantic rules allows SWORD to improve upon happens-before techniques that are known to mask races. To make its offline analysis highly efficient and scalable, SWORD employs effective self-balancing interval-tree-based algorithms. Our experimental results demonstrate that SWORD is capable of detecting races even within programs that use over 90% of the memory on each compute node. Further, our evaluation shows that it matches or exceeds the best available dynamic OpenMP race checker in detection capability while remaining efficient in execution time.

Virtually all real-valued computations are carried out using floating-point data types and operations. The precision of these data types must be set with the goals of reducing the overall round-off error, but also emphasizing performance improvements. Often, a mixed-precision allocation achieves this optimum; unfortunately, there are no techniques available to compute such allocations and conservatively meet a given error target across all program inputs. In this work, we present a rigorous approach to precision allocation based on formal analysis via Symbolic Taylor Expansions, and error analysis based on interval functions. This approach is implemented in an automated tool called FPTuner that generates and solves a quadratically constrained quadratic program to obtain a precision-annotated version of the given expression. FPTuner automatically introduces all the requisite precision up and down casting operations. It also allows users to flexibly control precision allocation using constraints to cap the number of high precision operators as well as group operators to allocate the same precision to facilitate vectorization. We evaluate FPTuner by tuning several benchmarks and measuring the proportion of lower precision operators allocated as we increase the error threshold. We also measure the reduction in energy consumption resulting from executing mixed-precision tuned code on a real hardware platform. We observe significant energy savings in response to mixed-precision tuning, but also observe situations where unexpected compiler behaviors thwart intended optimizations.

Modern computer scaling trends in pursuit of larger component counts and power efficiency have, unfortunately, lead to less reliable hardware and consequently soft errors escaping into application data ("silent data corruptions"). Techniques to enhance system resilience hinge on the availability of efficient error detectors that have high detection rates, low false positive rates, and lower computational overhead. Unfortunately, efficient detectors to detect faults during address generation have not been widely researched (especially in the context of indexing large arrays). We present a novel lightweight compiler-driven technique called PRESAGE for detecting bit-flips affecting structured address computations. A key insight underlying PRESAGE is that any address computation scheme that propagates an already incurred error is better than a scheme that corrupts one particular array access but otherwise (falsely) appears to compute perfectly. Ensuring the propagation of errors allows one to place detectors at loop exit pointsand helps turn silent corruptions into easily detectable error situations. Our experiments using the PolyBench benchmark suite indicate that PRESAGE-based error detectors have a high error-detection rate while incurring low overheads.

OpenMP plays a growing role as a portable programming model to harness on-node parallelism, yet, existing data race checkers for OpenMP have high overheads and generate many false positives. In this paper, we propose the first OpenMP data race checker, ARCHER, that achieves high accuracy, low overheads on large applications, and portability. ARCHER incorporates scalable happens-before tracking, exploits structured parallelism via combined static and dynamic analysis, and modularly interfaces with OpenMP runtimes. ARCHER significantly outperforms TSan and Intel® Inspector XE, while providing the same or better precision. It has helped detect critical data races in the Hypre library that is central to many projects at Lawrence Livermore National Laboratory and elsewhere.

Despite the growing popularity of GPGPU programming, there is not yet a portable and formally-specified barrier that one can use to synchronise across workgroups. Moreover, the occupancy-bound execution model of GPUs breaks assumptions inherent in traditional software execution barriers, exposing them to deadlock. We present an occupancy discovery protocol that dynamically discovers a safe estimate of the occupancy for a given GPU and kernel, allowing for a starvation-free (and hence, deadlock-free) inter-workgroup barrier by restricting the number of workgroups according to this estimate. We implement this idea by adapting an existing, previously non-portable, GPU inter-workgroup barrier to use OpenCL 2.0 atomic operations, and prove that the barrier meets its natural specification in terms of synchronisation.

Concurrency is pervasive and perplexing, particularly on graphics processing units (GPUs). Current specifications of languages and hardware are inconclusive; thus programmers often rely on folklore assumptions when writing software.

Tools for floating-point error estimation are fundamental to program understanding and optimization. In this paper, we focus on tools for determining the input settings to a floating point routine that maximizes its result error. Such tools can help support activities such as precision allocation, performance optimization, and auto-tuning. We benchmark current abstraction-based precision analysis methods, and show that they often do not work at scale, or generate highly pessimistic error estimates, often caused by non-linear operators or complex input constraints that define the set of legal inputs. We show that while concrete-testing-based error estimation methods based on maintaining shadow values at higher precision can search out higher error-inducing inputs, suit able heuristic search guidance is key to finding higher errors. We develop a heuristic search algorithm called Binary Guided Random Testing (BGRT). In 45 of the 48 total benchmarks, including many real-world routines, BGRT returns higher guaranteed errors. We also evaluate BGRT against two other heuristic search methods called ILS and PSO, obtaining better results.

Even the careful GPU programmer can inadvertently introduce data races while writing and optimizing code. Currently available GPU race checking methods fall short either in terms of their formal guarantees, ease of use, or practicality. Existing symbolic methods: (1) do not fully support existing CUDA kernels, (2) may require user-specified assertions or invariants, (3) often require users to guess which inputs may be safely made concrete, (4) tend to explode in complexity when the number of threads is increased, and (5) explode in the face of thread-ID based decisions, especially in a loop. We present SESA, a new tool combining Symbolic Execution and Static Analysis to analyze C++ CUDA programs that overcomes all these limitations. SESA also scales well to handle non-trivial benchmarks such as Parboil and Lonestar, and is the only tool of its class that handles such practical examples. This paper presents SESA's methodological innovations and practical results.

We present a novel integrated visualization system that enables interactive visual analysis of ensemble simulations of the sea surface height that is used in ocean forecasting. The position of eddies can be derived directly from the sea surface height and our visualization approach enables their interactive exploration and analysis.The behavior of eddies is important in different application settings of which we present two in this paper. First, we show an application for interactive planning of placement as well as operation of off-shore structures using real-world ensemble simulation data of the Gulf of Mexico. Off-shore structures, such as those used for oil exploration, are vulnerable to hazards caused by eddies, and the oil and gas industry relies on ocean forecasts for efficient operations. We enable analysis of the spatial domain, as well as the temporal evolution, for planning the placement and operation of structures.Eddies are also important for marine life. They transport water over large distances and with it also heat and other physical properties as well as biological organisms. In the second application we present the usefulness of our tool, which could be used for planning the paths of autonomous underwater vehicles, so called gliders, for marine scientists to study simulation data of the largely unexplored Red Sea.

We present a novel integrated visualization system that enables interactive visual analysis of ensemble simulations used in ocean forecasting, i.e, simulations of sea surface elevation. Our system enables the interactive planning of both the placement and operation of off-shore structures. We illustrate this using a real-world simulation of the Gulf of Mexico. Off-shore structures, such as those used for oil exploration, are vulnerable to hazards caused by strong loop currents. The oil and gas industry therefore relies on accurate ocean forecasting systems for planning their operations. Nowadays, these forecasts are based on multiple spatio-temporal simulations resulting in multidimensional, multivariate and multivalued data, so-called ensemble data. Changes in sea surface elevation are a good indicator for the movement of loop current eddies, and our visualization approach enables their interactive exploration and analysis. We enable analysis of the spatial domain, for planning the placement of structures, as well as detailed exploration of the temporal evolution at any chosen position, for the prediction of critical ocean states that require the shutdown of rig operations.

With the increasing cost of developing robust HPC software, precise data-flow analysis for MPI programs -- the mainstay of HPC programming -- are essential. The knowledge of communication is essential for precise data-flow analysis and the difficulty of statically determining it makes the conventional techniques insufficient. Hybrid methods combining static and dynamic techniques are needed and in this work we demonstrate one such approach in building the parallel control-flow graph which can then be used to leverage the precision of data-flow analyses for MPI programs.

With the widespread use of graphical processing units (GPUs), it is important to ensure that programmers have a clear understanding of their shared memory consistency model, i.e. what values can be read when issued concurrently with writes. Compared to CPUs, GPUs present different shared memory behavior, and we know of no published formal consistency model for them. To fill this void, we establish a formal state transition model of GPU loads, stores, and fences in the language Murphi, and check properties -- captured in litmus tests that pertain to ordering and visibility properties -- over executions using the Murphi model checker.

Technology scaling and techniques such as dynamic voltage/frequency scaling are predicted to increase the number of transient faults in future processors. Error detectors implemented in hardware are often energy inefficient, as they are "always on." While software-level error detection can augment hardware-level detectors, creating detectors in software that are highly effective remains a challenge. In this paper, we first present anew LLVM-level fault injector called KULFI that helps simulate faults occurring within CPU state elements in a versatile manner. Second, using KULFI, we study the behavior of a family of well-known and simple algorithms under error injection. (We choose a family of sorting algorithms for this study.) We then propose a promising way to interpret our empirical results using a formal model that builds on the idea of predicate state transition diagrams. After introducing the basic abstraction underlying our predicate transition diagrams, we draw connections to the level of resilience empirically observed during fault injection studies. Building on the observed connections, we develop a simple, and yet effective, predicate-abstraction-based fault detector. While in its initial stages, ours is believed to be the first study that offers a formal way to interpret and compare fault injection results obtained from algorithms from within one family. Given the absolutely unpredictable nature of what a fault can do to a computation in general, our approach may help designers choose amongst a class of algorithms one that behaves most resilient of all.

Programs written for GPUs often contain correctness errors such as races, deadlocks, or may compute the wrong result. Existing debugging tools often miss these errors because of their limited input-space and execution-space exploration. Existing tools based on conservative static analysis or conservative modeling of SIMD concurrency generate false alarms resulting in wasted bug-hunting. They also often do not target performance bugs (non-coalesced memory accesses, memory bank conflicts, and divergent warps). We provide a new framework called GKLEE that can analyze C++ GPU programs, locating the aforesaid correctness and performance bugs. For these programs, GKLEE can also automatically generate tests that provide high coverage. These tests serve as concrete witnesses for every reported bug. They can also be used for downstream debugging, for example to test the kernel on the actual hardware. We describe the architecture of GKLEE, its symbolic virtual machine model, and describe previously unknown bugs and performance issues that it detected on commercial SDK kernels. We describe GKLEE's test-case reduction heuristics, and the resulting scalability improvement for a given coverage target.

The growing scale of concurrency requires automated abstraction techniques to cut down the effort in concurrent system analysis. In this paper, we show that the high degree of behavioral symmetry present in GPU programs allows CUDA race detection to be dramatically simplified through abstraction. Our abstraction techniques is one of automatically creating parametric flows - control-flow equivalence classes of threads that diverge in the same manner - and checking for data races only across a pair of threads per parametric flow. We have implemented this approach as an extension of our recently proposed GKLEE symbolic analysis framework and show that all our previous results are dramatically improved in that (i) the parametric flow-based analysis takes far less time, and (ii) because of the much higher scalability of the analysis, we can detect even more data race situations that were previously missed by GKLEE because it was forced to downscale examples to limit analysis complexity. Moreover, the parametric flow-based analysis is applicable to other programs with SPMD models.

We propose a dynamic verification approach for large-scale message passing programs to locate correctness bugs caused by unforeseen nondeterministic interactions. This approach hinges on an efficient protocol to track the causality between nondeterministic message receive operations and potentially matching send operations. We show that causality tracking protocols that rely solely on logical clocks fail to capture all nuances of MPI program behavior, including the variety of ways in which nonblocking calls can complete. Our approach is hinged on formally defining the matches-before relation underlying the MPI standard, and devising lazy update logical clock based algorithms that can correctly discover all potential outcomes of nondeterministic receives in practice. can achieve the same coverage as a vector clock based algorithm while maintaining good scalability. LLCP allows us to analyze realistic MPI programs involving a thousand MPI processes, incurring only modest overheads in terms of communication bandwidth, latency, and memory consumption.

Multicore computers are now the norm. Taking advantage of these multiple cores entails parallel and concurrent programming. There is therefore a pressing need for courses that teach effective programming on multicore architectures. We believe that such courses should emphasize high-level abstractions for performance and correctness and be supported by tools. This paper presents a set of freely available course materials for parallel and concurrent programming, along with a testing tool for performance and correctness concerns called Alpaca (A Lovely Parallelism And Concurrency Analyzer). These course materials can be used for a comprehensive parallel and concurrent programming course, à la carte throughout an existing curriculum, or as starting points for graduate special topics courses. We also discuss tradeoffs we made in terms of what to include in course materials.

We present a preliminary automated verifier based on mechanical decision procedures which is able to prove functional correctness of CUDA programs and guarantee to detect bugs such as race conditions. We also employ a symbolic partial order reduction (POR) technique to mitigate the interleaving explosion problem.

Standard testing methods of MPI programs do not guarantee coverage of all non-deterministic interactions (e.g., wildcard-receives). Programs tested by these methods can have untested paths (bugs) that may become manifest unexpectedly. Previous formal dynamic verifiers cover the space of non-determinism but do not scale, even for small applications. We present DAMPI, the first dynamic analyzer for MPI programs that guarantees scalable coverage of the space of non-determinism through a decentralized algorithm based on Lamport-clocks. DAMPI computes alternative non-deterministic matches and enforces them in subsequent program replays. To avoid interleaving explosion, DAMPI employs heuristics to focus coverage to regions of interest. We show that DAMPI can detect deadlocks and resource-leaks in real applications. Our results on a wide range of applications using over a thousand processes, which is an order of magnitude larger than any previously reported results for MPI dynamic verification tools, demonstrate that DAMPI provides scalable, user-configurable testing coverage.

Interest in Graphical Processing Units (GPUs) is skyrocketing due to their potential to yield spectacular performance on many important computing applications. Unfortunately, writing such efficient GPU kernels requires painstaking manual optimization effort which is very error prone. We contribute the first comprehensive symbolic verifier for kernels written in CUDA C. Called the 'Prover of User GPU programs (PUG),' our tool efficiently and automatically analyzes real-world kernels using Satisfiability Modulo Theories (SMT) tools, detecting bugs such as data races, incorrectly synchronized barriers, bank conflicts, and wrong results. PUG's innovative ideas include a novel approach to symbolically encode thread interleavings, exact analysis for correct barrier placement, special methods for avoiding interleaving generation, dividing up the analysis over barrier intervals, and handling loops through three approaches: loop normalization, overapproximation, and invariant finding. PUG has analyzed over a hundred CUDA kernels from public distributions and in-house projects, finding bugs as well as subtle undocumented assumptions.

Abstract There is a growing need to address the complexity of verifying the numerous concurrent protocols employed in the high‐performance computing software. Today's approaches for verification consist of testing detailed implementations of these protocols. Unfortunately, this approach can seldom show the absence of bugs, and often results in serious bugs escaping into the deployed software. An approach calledModel Checkinghas been demonstrated to be eminently helpful in debugging these protocols early in the software life cycle by offering the ability to represent and exhaustively analyze simplified formal protocol models. The effectiveness of model checking has yet to be adequately demonstrated in high‐performance computing. This paper presents a case study of a concurrent protocol that was thought to be sufficiently well tested, but proved to contain two very non‐obvious deadlocks in them. These bugs were automatically detected through model checking. The protocol models in which these bugs were detected were also easy to create. Recent work in our group demonstrates that even this tedium of model creation can be eliminated by employing dynamic source‐code‐level analysis methods. Our case study comes from the important domain of Message Passing Interface (MPI)‐based programming, which is universally employed for simulating and predicting anything from the structural integrity of combustion chambers to the path of hurricanes. We argue that model checking must be taught as well as used widely within HPC, given this and similar success stories. Copyright © 2009 John Wiley & Sons, Ltd.

We present a dynamic verification tool MCC for Multicore Communication API applications - a new API for communication among cores. MCC systematically explores all relevant interleavings of an MCAPI application using a tailor-made dynamic partial order reduction algorithm (DPOR). Our contributions are (i) a way to model the non-overtaking message matching relation underlying MCAPI calls with a high level algorithm to effect DPOR for MCAPI that controls the lower level details so that the intended executions happen at runtime; and (ii) a list of default safety properties that can be utilized in the process of verification. To our knowledge, this is the first push button model checker for MCAPI application writers that, at present, deals with an interesting subset of MCAPI calls. Our result is the demonstration that we can indeed develop a dynamic model checker for MCAPI that can directly control the non-deterministic behavior at runtime that is inherent in any implementation of the library without additional API modifications or additions.

This paper considers the problem of formal verification of MPI programs operating under a fixed test harness for safety properties without building verification models. In our approach, we directly model-check the MPI/C source code, executing its interleavings with the help of a verification scheduler. Unfortunately, the total feasible number of interleavings is exponential, and impractical to examine even for our modest goals. Our earlier publications formalized and implemented a partial order reduction approach that avoided exploring equivalent interleavings, and presented a verification tool called ISP. This paper presents algorithmic and engineering innovations to ISP, including the use of OpenMP parallelization, that now enables it to handle practical MPI programs, including: (i) ParMETIS- a widely used hypergraph partitioner, and (ii) MADRE- a Memory Aware Data Re-distribution Engine, both developed outside our group. Over these benchmarks, ISP has automatically verified up to 14K lines of MPI/C code, producing error traces of deadlocks and assertion violations within seconds.

The Gauss group at the University of Utah has researched and developed runtime verification tools for MPI programs. Our tool, in-situ partial order (ISP), is being applied to several MPI benchmarks. At the same time, we are embarked on research that ensures the completeness of ISP. Our work on specifying the formal semantics of MPI has also encompassed MPI 2.0. These developments and our plans for our final (fourth) year are elaborated in this paper.

No abstract available.

No abstract available.

Modeling hardware through atomic guard/action transitions with interleaving semantics is popular, owing to the conceptual clarity of modeling and verifying the high level behavior of hardware. In mapping such specifications into hardware, designers often decompose each specification transition into sequences of implementation transitions taking one clock cycle each. Some implementation transitions realizing a specification transition overlap. The implementation transitions realizing different specification transitions can also overlap. We present a formal theory of refinement, showing how a collection of such implementation transitions can be shown to realize a specification. We present a modular refinement verification approach by developing abstraction and assume-guarantee principles that allow implementation transitions realizing a single specification transition to be situated in sufficiently general environments. Illustrated on a non-trivial VHDL cache coherence engine, our work may allow designers to design high performance controllers without being constrained by fixed automated synthesis scripts, and still conduct modular verification.

High-end computing is universally recognized to be a strategic tool for leadership in science and technology. A significant portion of high-end computing is conducted on clusters running the message passing interface (MPI) library. MPI has become a de facto standard in HPC. MPI programs, as well as MPI library implementations can be buggy, especially when aiming high performance, and running on or porting onto new platforms. Our recent work has addressed the following areas: A TLA+ formal semantics of a large subset of MPI-1; A Microsoft Phoenix based model extraction and analysis framework for MPI programs; integration into the visual studio environment for error-trace visualization; A new dynamic partial order reduction algorithm (DPOR) tailored to MPI so that the number of interleavings examined during MPI program verification are dramatically reduced; A program called 'inspector' for analyzing C++ programs that has found bugs in publicly distributed threaded programs (Inspector automatically instruments Pthread programs and searches for races based on a new DPOR); verified byte-range locking protocols using MPI one-sided communication - a case study where we found bugs in published byte-range locking protocols, and designed and verified improved versions of these protocols; A new in-situ model checker for MPI programs, that traps MPI calls using its profiling interface (PMPI) and orchestrates control to maximize coverage with minimal state saving overhead. The progress made in exploring these directions, our publications, and associated software tools are described, as are our future plans.

We illustrate how to employ metacircular assume/guarantee reasoning to reduce the verification complexity of finite instances of protocols for safety, using nothing more than an explicit state model checker. The formal underpinnings of our method are based on establishing a simulation relation between the given protocol M, and several overapproximations thereof, Mtilde1,..., Mtildek. Each Mtildeisimulates M, and represents one "view" of it. The Mtildeis depend on each other both to define the abstractions as well as to justify them. We show that in case of our hierarchical coherence protocol, its designer could easily construct each of the Mtildeiin a counterexample guided manner. This approach is practical, considerably reduces the verification complexity, and has been successfully applied to a complex hierarchical multicore cache coherence protocol which could not be verified through traditional model checking

The quest for high performance drives parallel scientific computing software design. Well over 60% of the high-performance computing (HPC) community writes programs using the MPI library; to gain performance, they are known to perform many manual optimizations. Even tools that accept high level descriptions often generate MPI code, due to its eminent portability. However, since the overall performance of a program does not usually port (due to variations in the target architecture, cluster size, etc.), manual changes to the code are inevitable in today's approaches to MPI programming and optimization. This, together with the vastness and evolving nature of the MPI standard, and the innate complexity of concurrent programming introduces costly bugs. Our research addresses these challenges through specific efforts in the following broad areas: (i) high level expression of the parallel algorithm and compilation thereof into optimized MPI programs, (ii) optimizations of user-written detailed MPI programs through localized transformations such as barrier removal, (iii) formal modeling of complex communication standards, such as the MPI-2 standard and a facility for answering putative queries (this need arises when standard documents are impossibly difficult to manually study in order to answer questions that are not explicitly addressed in the standard), (iv) formal modeling of new (and hence relatively less well understood) features of communication libraries, such as the one-sided communication facility of MPI-2, and (v) formal modeling of intricate control algorithms in these libraries such as the progress engine for TCP and/or shared memory in MPICH2 (a formal model can explicate commonalities, help formally verify, as well as help create better future implementations). Our research gains focus through numerous collaborations

We view shared memories as structures, which define relations over the set of programs and their executions. An implementation is modeled by a transducer, where the relation it realizes is its language. This approach allows us to cast shared memory verification as language inclusion. We show that a specification can be approximated by an infinite hierarchy of finite-state transducers, called the memory model machines. Also, checking whether an execution is generated by a sequentially consistent memory is approached through a constraint satisfaction formulation. It is proved that if a memory implementation generates a non interleaved sequential and unambiguous execution, it necessarily generates one such execution of bounded size. Our paper summarizes the key results from the first author's dissertation, and may help a practitioner understand with clarity what "sequential consistency checking is undecidable" means.

Abstract Given the complicated nature of modern shared memory systems, it is vital to have a systematic approach to specifying and analyzing memory consistency requirements. In this paper, we present the UMM specification framework, which integrates two key features to support memory model verification: (i) it employs a simple and generic memory abstraction that can capture a large collection of memory models as guarded commands with a uniform notation, and (ii) it provides built‐in model checking capability to enable formal reasoning about thread behaviors. Using this framework, memory models can be specified in a parameterized style—designers can simply redefine a few bypassing rules and visibility ordering rules to obtain an executable specification of another memory model. We formalize several classical memory models, including Sequential Consistency, Coherence, and PRAM, to illustrate the general techniques of applying this framework. We then provide an alternative specification of the Java memory model, based on a proposal from Manson and Pugh, and demonstrate how to analyze Java thread semantics using model checking. We also compare our operational specification style with axiomatic specification styles and explore a mechanism that converts a memory model definition from one style to the other. Copyright © 2005 John Wiley & Sons, Ltd.

Summary form only given. Conforming to the underlying memory consistency rules is a fundamental requirement for implementing shared memory systems and developing multiprocessor programs. In order to promote understanding and enable automated verification, it is highly desirable that a memory model specification be both declarative and executable. We present a specification framework called Nemos (Nonoperational yet Executable Memory Ordering Specifications), which supports precise specification and automatic execution in the same framework. We employ a uniform notation based on predicate logic to define shared memory semantics in an axiomatic as well as compositional style. We also apply constraint logic programming and SAT solving to make the axiomatic specifications executable for memory model analysis. To illustrate our approach, we formalize a collection of classical memory models, including sequential consistency, coherence, PRAM, causal consistency, and processor consistency.

The advent of the system-on-chip and intellectual property hardware design paradigms makes protocol compliance verification increasingly important to the success of a project. One of the central tools in any verification project is the modeling language, and we survey the field of candidate languages for protocol compliance verification, limiting our discussion to languages originally intended for hardware and software design and verification activities. We frame our comparison by first constructing a taxonomy of these languages, and then by discussing the applicability of each approach to the compliance verification problem. Each discussion includes a summary of the development of the language, an evaluation of the language's utility for our problem domain, and, where feasible, an example of how the language might be used to specify hardware protocols. Finally, we make some general observations regarding the languages considered.

Provides a simple formal model for Itanium/sup TM/ shared memory consistency covering a core set of instructions, that is reverse-engineered fromand. Our model sheds light on tricky concepts such as causality. It deals with cacheable memory instructions consisting of acquire loads, ordinary loads, release stores and ordinary stores, as well as memory fences. It does not currently handle atomic read-modify-writes, non-cacheable memory or special rules pertaining to data dependencies involving registers. Despite its simplicity, our model captures all published ordering properties of the instructions we consider. While operational models have been proposed for commercial shared memory systems (notably for Sparc V9), a notable feature of our operational model is its use of a few explicit devices such as vector timestamps to clearly describe the tricky notion of causality.

This paper presents a new approach to two-level hazard-free logic minimization in the context of extended burst-mode finite state machine synthesis targeting generalized C-elements (gC). No currently available minimizers for literal-exact two-level hazard-free logic minimization of extended burst-mode gC controllers can handle large circuits without synthesis times ranging up over thousands of seconds. Even existing heuristic approaches take too much time when iterative exploration over a large design space is required and do not yield minimum results. The logic minimization approach presented in this paper is based on state graph exploration in conjunction with single-cube cover algorithms, an approach that has not been considered for minimization of extended burst-mode finite state machines previously. Our algorithm achieves very fast logic minimization by introducing compacted state graphs and cover tables and an efficient single-cube cover algorithm for single-output minimization. Our exact logic minimizer finds minimal number of literal solutions to all currently available benchmarks, in less than one second on a 333 MHz microprocessor-more than three orders of magnitude faster than existing literal exact methods, and over an order of magnitude faster than existing heuristic methods for the largest benchmarks. This includes a benchmark that has never been possible to solve exactly in number of literals before.

The advantages of the programmable control paradigm are widely known in the design of synchronous sequential circuits: easy correction of late design errors, easy upgrade of product families to meet time-to-market constraints, and modifications of the control algorithm, even at run time. However, despite the growing interest in asynchronous (self-timed) circuits, programmable asynchronous controllers based on the idea of microprogramming have not been actively pursued. In this paper, we propose an asynchronous microprogrammed control organization (called a microengine) that targets application-specific implementations and emphasizes simplicity, modularity, and high performance. The architecture takes advantage of the natural ability of self-timed circuits to chain actions efficiently without the clock-based scheduling constraints that would be involved in comparable synchronous designs. The result is a general approach to the design of application-specific microengines featuring a programmable data-path topology that offers very compact microcode and high performance-in fact, performance close to that offered by automated hardwired controllers. In performance comparisons of a CD-player error decoder design, the proposed microengine architecture was 26 times faster than the general purpose hardware of a 280 MIPS microprocessor, over three times as fast as the special purpose hardware of a low-power macromodule based implementation, and even slightly faster than a finite state machine-based implementation.

Most high-level synthesis tools for asynchronous circuits take descriptions in concurrent hardware description languages and generate networks of macromodules or handshake components. In this paper, we propose a peephole optimizer for these networks. Our peephole optimizer first deduces an equivalent blackbox behavior for the network using Dill's trace-theoretic parallel composition operator. It then applies a new procedure called burst-mode reduction to obtain burst-mode machines from the deduced behavior. In a significant number of examples, our optimizer achieves gate-count improvements by a factor of five, and speed (cycle-time) improvements by a factor of two. Burst-mode reduction can be applied to any macromodule network that is delay insensitive as well as deterministic. A significant number of asynchronous circuits, especially those generated by asynchronous high-level synthesis tools, fall into this class, thus making our procedure widely applicable.

With the escalation of clock frequencies and the increasing ratio of wire-to gate-delays, clock skew is a major problem to be overcome in tomorrow's high-speed very large scale integration (VLSI) chips. Also, with an increasing number of stages switching simultaneously comes the problem of higher peak power consumption. In our prior work, we have proposed a novel scheme called counterflow-clocked (C/sup 2/) pipelining to combat these problems, and discussed methods for composing C/sup 2/ pipelined stages. In this paper, we analyze in great detail the timing constraints to be obeyed in designing basic C/sup 2/ pipelined stages, as well as in composing C/sup 2/ pipelined stages. C/sup 2/ pipelining is well suited for systems that exhibit mostly unidirectional data flows as well as possess mostly nearest neighbor connections. C/sup 2/ pipelining eases the distribution of high-speed clocks, shortens the clock period by eliminating global clock signals, allows natural use of level-sensitive dynamic latches, and generates less internal switching noises due to the uniformly distributed latch operation. By applying C/sup 2/ pipelining and its composition methods to build a system, VLSI designers can substitute the global clock-skew problem with many local one-sided delay constraints.

Article Free Access Share on Using “test model-checking” to verify the Runway-PA8000 memory model Authors: Rajnish Ghughal Department of Computer Science, University of Utah, Salt Lake City, UT Department of Computer Science, University of Utah, Salt Lake City, UTView Profile , Abdel Mokkedem Department of Computer Science, University of Utah, Salt Lake City, UT Department of Computer Science, University of Utah, Salt Lake City, UTView Profile , Ratan Nalumasu Department of Computer Science, University of Utah, Salt Lake City, UT Department of Computer Science, University of Utah, Salt Lake City, UTView Profile , Ganesh Gopalakrishnan Department of Computer Science, University of Utah, Salt Lake City, UT Department of Computer Science, University of Utah, Salt Lake City, UTView Profile Authors Info & Claims SPAA '98: Proceedings of the tenth annual ACM symposium on Parallel algorithms and architecturesJune 1998 Pages 231–239https://doi.org/10.1145/277651.277689Published:01 June 1998Publication History 6citation261DownloadsMetricsTotal Citations6Total Downloads261Last 12 Months17Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Article Free Access Share on A technique for synthesizing distributed burst-mode circuits Authors: Prabhakar Kudva IBM T. J. Watson Research Center, Yorktown Heights IBM T. J. Watson Research Center, Yorktown HeightsView Profile , Ganesh Gopalakrishnan Department of Computer Science, University of Utah Department of Computer Science, University of UtahView Profile , Hans Jacobson Department of Computer Science, University of Utah Department of Computer Science, University of UtahView Profile Authors Info & Claims DAC '96: Proceedings of the 33rd annual Design Automation ConferenceJune 1996 Pages 67–70https://doi.org/10.1145/240518.240532Published:01 June 1996Publication History 13citation201DownloadsMetricsTotal Citations13Total Downloads201Last 12 Months11Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

This paper addresses the problem of realizing hazard-free singleoutput Boolean functions through a network of customized complex CMOS gates tailored to a given asynchronous controller specification.A customized CMOS gate network can either be a single CMOS gate or a multilevel network of CMOS gates.It is shown that hazard-free requirements for such networks are less restrictive than for simple gate networks.Analysis and efficient synthesis methods to generate such networks under a multiple-input change assumption (MIC) will be presented.

Most high level synthesis tools for asynchronous circuits take descriptions in concurrent hardware description languages and generate networks of macromodules or handshake components. In this paper we describe a peephole optimizer for such macromodule networks that often effects area and/or time improvements. Our optimizer first deduces an equivalent black-box behavior for the given network of macromodules using Dill's trace-theoretic parallel composition operator. It then applies a new procedure called burst-mode reduction to obtain burst-mode machines, which can be synthesized into gate networks using available tools. Since burst-mode reduction can be applied to any macromodule network that is delay-insensitive as well as deterministic, our optimizer covers a significant number of asynchronous circuits, especially those generated by asynchronous high level synthesis tools.>

Asynchronous/self-timed circuits are beginning to attract renewed attention as a promising means of dealing with the complexity of modern VLSI designs. Very few analysis techniques or tools are available for estimating their performance. We adapt the theory of generalized timed Petri-nets (GTPN) for analyzing and comparing asynchronous circuits ranging from purely control-oriented circuits to those with data dependent control. Experiments with the GTPN analyzer are found to track the observed performance of actual asynchronous circuits, thereby offering empirical evidence towards the soundness of the modeling approach.>

In order to reasonably determine the correctness of asynchronous circuit implementations and specifications, Dill (1989) has developed a variant of trace theory. Trace theory describes the behavior of an asynchronous circuit by representing its possible executions as strings, called "traces." A useful relation defined in this theory is called conformance, which holds when one trace specification can be safely substituted for another. We propose a new relation in the context of Dill's trace theory, called strong conformance. We show that this relation is capable of detecting certain errors in asynchronous circuits that cannot be detected through conformance. Strong conformance also helps to justify circuit optimization rules where a component is replaced by another component having extra capabilities (e.g., it can accept more inputs). The structural operators of Dill's trace theory-compose, rename, and hide-are shown to be monotonic with respect to strong conformance. Experiments are presented using a modified version of Dill's trace theory verifier that implements a check for strong conformance.>

Symbolic simulation has been proposed as a way to formally verify the correct operation of an MOS circuit. By allowing nonground expressions as values, a symbolic simulator avoids the complexity of exhaustive simulation. The symbolic expressions chosen for initializing the state- and input-variables must cover all valid test cases while avoiding those that violate circuit constraints. In this paper, we present a new approach to symbolic simulation-based verification that hinges on the use of parametric forms of Boolean expressions. A parametric form of a Boolean expression E is an equivalent expression in which the variables in E are expressed in terms of expressions over new variables called parametric variables. In our approach, Boolean expressions representing the operating constraints on the circuit node values are first converted into the parametric form, and the resulting parametric expressions are used as initial (symbolic) node values prior to each simulation step. In addition to the proposal to use the parametric form, we make the following additional contributions. We present a new method for generating the parametric form of a Boolean expression that exploits (among other things) the structural recursion involved in defining commonly used arithmetic/relational operators. Our method generates parametric forms that are more compact, as well as more balanced in terms of term-sizes than generated by the following existing methods: Boole's, Lowenheim's, and the generalized cofactor method. We have also developed a variety of example-specific techniques to deal with circuit constraints. All algorithms discussed in this paper have been implemented in a verification prototype system. Experimental results obtained using the COSMOS symbolic simulator are also reported.>

Control-intensive IC's pose a significant challenge to the users of formal methods in designing hardware. These IC's have to support a wide variety of requirements including synchronous and asynchronous operations, polling and interrupt driven modes of operation, multiple concurrent threads of execution, nontrivial computational requirements, and programmability. We illustrate the use of formal methods in the design of a control-intensive IC called the "Intel 8251" Universal Synchronous/Asynchronous Receiver/Transmitter (USART), using our hardware description language "hopCP". A feature of hopCP is that it supports communication via asynchronous ports in addition to synchronous message passing. Asynchronous ports are distributed shared variables writable by exactly one process. We show the usefulness of this combination of communication constructs. We outline algorithms to determine safe usages of asynchronous ports, and also to discover other static properties of the specification. We discuss a compiled-code concurrent functional simulator called CFSIM, as well as the use of concurrent testers for driving CFSIM. The use of a semantically well-specified and simple language, and the associated analysis/simulation tools helps conquer the complexity of specifying and validating control-intensive IC's.>

We consider the language of constraint formula involving Boolean connectives, and relational, logical, and arithmetic operations on bit vectors. An example of a formula in this language is F=((A+B)>

The use of formal methods in hardware design improves the quality of designs in many ways: it promotes better understanding of the design; it permits systematic design refinement through the discovery of invariants; and it allows design verification (informal or formal). In this paper we illustrate the use of formal methods in the design of a custom hardware system called the “Rollback Chip” (RBC), conducted using a simple hardware design description language called “HOP”. An informal specification of the requirements of the RBC is first given, followed by a behavioral description of the RBC stating its desired behavior . The behavioral description is refined into progressively more efficient designs, terminating in a structural description . Key refinement steps are based on system invariants that are discovered during the design, and proved correct during design verification. The first step in design verification is to apply a program called PARCOMP to derive a behavioral description from the structural description of the RBC. The derived behavior is then compared against the desired behavior using equational verification techniques. This work demonstrates that formal methods can be fruitfully applied to a nontrivial hardware design. It also illustrates the particular advantages of our approach based on HOP and PARCOMP. Last, but not the least, it formally verifies the RBC mechanism itself.

SHILPA is a system for the high-level synthesis of self-timed circuits. It takes behavioral descriptions in a process+functional language called hopCP and produces a netlist for the Actel field-programmable gate array (FPGA), supported by the VIEWlogic tools. hopCP descriptions are initially translated into an intermediate form based on hypergraphs called HFGs. SHILPA then applies action refinement, which is a technique for transforming HFGs into asynchronous hardware by a series of graph-based transformation rules. Action refinement is characterized by incremental resource allocation and control decomposition. The major contributions of the proposed work are given.>

Some techniques to make symbolic simulation-based verification efficient in practice are presented. The first technique is applied to the verification of nonregular designs. Minimally instantiated symbolic simulation vectors are first generated, and all these vectors are encoded into one vector using auxiliary (parametric) Boolean variables. The second technique also pertains to nonregular designs, and it offers a way to compactly encode input constraints during symbolic simulation. Two variations of this technique are explored. The third technique relates to the verification of regular arrays. It is shown that many regular arrays require input constraints to be obeyed, and that these constraints can be encoded using parametric Boolean variables. Another related technique (applicable to regular arrays where control-flow is data independent) does not encode the input constraints, but takes them into account after symbolic simulation. All the techniques are supported by experimental results.>

An asynchronous architecture for dynamically reordering sequences of instructions issued to a processing element is presented. The optimizations supported are the exchange of two instructions and the cancellation of an instruction using its predecessor. The design is a modification of I. Sutherland's (1989) micropipeline, and is called the asynchronous reordering micropipeline (ARM). The optimizations to be effected by the ARM are captured using rewrite rules that transform instruction subsequences into more optimal (and semantically equivalent) subsequences. One application of the ARM is in optimizing transactions issued to a system called the rollback chip (RBC), which is used to accelerate the state-saving and rollback activities performed by a processing node when it runs distributed discrete-event simulation using time warp.>

Existing approaches to implement state saving are not appropriate for large Time Warp programs. The authors propose a component called the rollback chip (RBC) that efficiently implements state saving. Such a component could be used in a programmable, special purpose parallel discrete event simulation engine based on Time Warp. The algorithms implemented by the rollback chip are described, as well as mechanisms that allow efficient implementation. Results of simulation studies are presented that show that the rollback chip can virtually eliminate the state saving and rollback overheads that plague current software implementations of Time Warp.>

A special-purpose simulation engine based on the Time Warp mechanism is proposed to attack large-scale discrete-event simulation problems. A key component of this engine is the rollback chip, a hardware component that efficiently implements state saving and rollback functions in Time Warp. The algorithms implemented by the rollback chip are described, as well as mechanisms that allow efficient implementation. Results of simulation studies are presented that show that the rollback chip can virtually eliminate the state-saving overhead that plagues current software implementations of Time Wrap.>