Pipelined circuits operate as an assembly line that starts processing new instructions while older ones continue execution. Control properties specify the correct behaviour of the pipeline with respect to how it handles the concurrency between instructions. Control properties stand out as one of the most challenging aspects of pipelined circuit verification. Their verification depends on the datapath and memories, which in practice account for the largest part of the state space of the circuit. To alleviate the state explosion problem, abstraction of memories and datapath becomes mandatory. This thesis provides a methodology for an efficient abstraction of the datapath under all possible control-visible behaviours. For verification of control properties, the abstracted datapath is then substituted in place of the original one and the control circuitry is left unchanged. With respect to control properties, the abstraction is shown conservative by both language containment and simulation. For verification of control properties, the pipeline datapath is represented by a network of registers, unrestricted combinational datapath blocks and muxes. The values flowing through the datapath are called parcels. The control is the state machine that steers the parcels through the network. As parcels travel through the pipeline, they undergo transformations through the datapath blocks. The control- visible results of these transformations fan-out into control variables which in turn influence the next stage the parcels are transferred to by the control. The semantics of the datapath is formalized as a labelled transition system called a parcel automaton. Parcel automata capture the set of all control visible paths through the pipeline and are derived without the need of reachability analysis of the original pipeline. Datapath abstraction is defined using familiar concepts such as language containment or simulation. We have proved results that show that datapath abstraction leads to pipeline abstraction. Our approach has been incorporated into a practical algorithm that yields directly the abstract parcel automaton, bypassing the construction of the concrete parcel automaton. The algorithm uses a SAT solver to generate incrementally all possible control visible behaviours of the pipeline datapath. Our largest case study is a 32-bit two-wide superscalar OpenRISC microprocessor written in VHDL, where it reduced the size of the implementation from 35k gates to 2k gates in less than 10 minutes while using less than 52MB of memory.

Software bugs are expensive. Recent estimates by the US National Institute of Standards and Technology claim that the cost of software bugs to the US economy alone is approximately 60 billion USD annually. As society becomes increasingly software-dependent, bugs also reduce our productivity and threaten our safety and security. Decreasing these direct and indirect costs represents a significant research challenge as well as an opportunity for businesses. Automatic software bug-finding and verification tools have a potential to completely revolutionize the software engineering industry by improving reliability and decreasing development costs. Since software analysis is in general undecidable, automatic tools have to use various abstractions to make the analysis computationally tractable. Abstraction is a double-edged sword: coarse abstractions, in general, yield easier verification, but also less precise results. This thesis focuses on exploiting the structure of software for abstracting away irrelevant behavior. Programmers tend to organize code into objects and functions, which effectively represent natural abstraction boundaries. Humans use such structural abstractions to simplify their mental models of software and for constructing informal explanations of why a piece of code should work. A natural question to ask is: How can automatic bug-finding tools exploit the same natural abstractions? This thesis offers possible answers. More specifically, I present three novel ways to exploit structure at three different steps of the software analysis process. First, I show how symbolic execution can preserve the data-flow dependencies of the original code while constructing compact symbolic representations of programs. Second, I propose structural abstraction, which exploits the structure preserved by the symbolic execution. Structural abstraction solves a long-standing open problem --- scalable interprocedural path- and context-sensitive program analysis. Finally, I present an automatic tuning approach that exploits the fine-grained structural properties of software (namely, data- and control-dependency) for faster property checking. This novel approach resulted in a 500-fold speedup over the best previous techniques. Automatic tuning not only redefined the limits of automatic software analysis tools, but also has already found its way into other domains (like model checking), demonstrating the generality and applicability of this idea.

Specification animation has become a popular technique in industry, particularly for validation in model-based design processes. Animation tools provide the ability to explore and visualise the behaviour of a model without needing to study its internal workings. Formal refinement techniques should also be of interest to industry since they support verifiably correct transformations of system models towards implementation. So far, however, refinement techniques are not widely used. Their application requires a high degree of mathematical skill, even with the currently available tool support. Better tool support is needed to make refinement techniques accessible to industry. In this thesis we investigate the application of existing specification animation and visualisation tools to problems in refinement theory. We show how animation and visualisation can be used to support verification, by refinement, and validation, by comparing the behaviour of a refined specification against its abstract specification. Such techniques can be used to explain and/or improve the understanding of a refinement and to check for the presence of errors in a refinement, for example, before attempting a proof. In the most challenging cases, data refinements, the designer needs to supply an abstraction relation in order to prove the refinement. We initially assume that an abstraction relation is provided as an input to the verification and validation tasks. However, finding abstraction relations is hard, and is currently a matter of trial and error. We therefore study the problem of finding abstraction relations. We show that, if an abstraction relation exists, there is always a unique weakest abstraction relation and at least one minimal abstraction relation, and we describe algorithms for finding both the weakest abstraction relation and minimal abstraction relations. These algorithms can be applied to small finite-state systems to produce abstraction relations in terms of explicit values of state variables. We then investigate a symbolic algorithm for finding abstraction relations, which can be applied to systems with infinite states, to produce abstraction relations in predicate form. The theory and the algorithms we develop thus make it possible for us to extend our animation-based verification and validation techniques so that they can be used without providing a complete abstraction relation. Additionally our extended techniques can help a designer construct an abstraction relation or check a proposed one.

Diss.--Munich, 1967. / Bibliography: p. 107-108.

Thesis (M.A.)--Ohio University, June, 2009. / Title from PDF t.p. Includes bibliographical references.

Thesis (M.S.)--University of California, Santa Cruz, 1988. / Typescript. Includes bibliographical references.

Thesis (M.A.)--Indiana University, 2010. / Title from screen (viewed on July 19, 2010). Department of English, Indiana University-Purdue University Indianapolis (IUPUI). Advisor(s): Susan Shepherd, Frederick J. DiCamilla, Jonathan R. Eller. Includes vitae. Includes bibliographical references (leaves 90-94).

In the current dissertation an implementation of shared memory abstraction on top of contemporary multi-core and many-core clusters has taken place. The results of the presented research effort are mainly depicted in the implementation of the cluster middleware platform Pleiad. Pleiad is a Java-based prototype that incorporates best practices from the field of distributed shared memory systems and also includes some prototype characteristics. Next we review briefly the main results and contributions of the current dissertation: • e presented middleware, Pleiad, is characterized by a highly modular design. Moreover, contrast to most other related efforts, which are usually bound to a specific implementation of consistency, Pleiad has the infrastructure to incorporate many implementations for a certain mechanism and can even interchange such implementations during runtime. • Reference implementations are offered for the relaxed consistency models of Lazy Release Consistency (LRC) and Scope Consistency (ScC). Pleiad is the first Javabased middleware to incorporate implementations for both protocols. • In the current dissertation is taking place one of the few evaluations on a cluster that is supplied with low-power processors (Intel Atom) and thus can be thought as a characteristic case of embedded oriented multi-core clusters. • In the current dissertation one of the first implementations of shared memory abstraction on top of GPU clusters is presented. Shared memory abstraction is evaluated under two schemes. On the first scheme shared memory programming with GPU clusters is achieved under a hybrid combination of the first commercial implementation of OpenMP for clusters, the Intel Cluster OpenMP, and the CUDA platform. e evaluated scheme is the first evaluation of OpenMP and CUDA in the context of GPU clusters. e second scheme involves the enhancement of Pleiad in order to support utilization of GPU clusters. Such implementation is one of the few unified implementation of a shared memory abstraction programming environment that • For the moment there is no establishment of available and widely used benchmarks or application codes that utilize multiple GPUs, either on a cluster or a single node. us, among the thesis contributions is considered the evaluation of shared memory abstraction with real application codes, since the few related systems either have used simple kernels or have been evaluated on a single node. • Specifically, in the current thesis applications from two characteristic domains, computational fluid dynamics (CFD) and data clustering, have been implemented and evaluated using GPU clusters and single GPUs. In the first case, a computationally intensive CDF code that operates on structured grids has been accelerated on a GPU cluster, while a simulation that manipulates unstructured grid has been accelerated in the context of a single GPU and demonstrates its potential for GPU cluster acceleration. Accordingly, a partitional data clustering algorithm is accelerated using shared memory abstraction on GPU clusters and a preliminary implementation of a hierarchical data clustering algorithm on GPUs is described. / -

This thesis seeks to unfold the concept of the ‘degree zero art’ as an artistic and cultural project as manifested in the practices of two very different artists, Milan-based Piero Manzoni (Soncino 1933- Milan 1963) and Rio-born Hélio Oiticica (Rio de Janeiro 1937-1980), during the second half of the twentieth century. Despite the clear contrasts between their works and their very different cultural formations, the thesis focuses on these artists in order to show how their practices align around the challenge to aesthetic categories, stylistic labels and political frameworks employed by much recent critical literature. In order to discuss intellectual and critical structures developed to narrate varieties of North American conceptual practices, this thesis proposes a new interpretative frame: a ‘degree zero aesthetics’, creating a transnational dialogue between the work of Manzoni and Oiticica. Borrowing from the understanding of zero proposed by the German Zero group at the beginning of the sixties, I argue that the idea of zero denotes a fresh start and constructive will; it therefore explains the process of erasing and rebuilding from scratch that has characterised the post-war generation. Alongside the process of construing an aesthetic around the notion of ‘zero’, this thesis aims to deconstruct popular sites of discourse around the tropes of ‘participation’ and ‘politics’, critically readdressing the historiography surrounding these themes. Lastly, this project attempts to discuss the literature on both artists, who have become paradigmatic of certain key movements and moments in Latin American and European art respectively, and in recent elaborations of global art histories.

No description available.