CiteULike: rob_quill's no-tag

Specifying and refining program transformations using temporal logic side conditions

Sara Kalvala — 2008-05-09T15:05:13-00:00

ACM Trans. Program. Lang. Syst. (2008)

An Algorithm for Translating Boolean Expressions

Bruce Arden — 2008-05-09T15:01:40-00:00

J. ACM, Vol. 9, No. 2. (April 1962), pp. 222-239.

Analysis and Transformation in an Interactive Parallel Programming Tool

K Kennedy — 2008-05-09T15:00:00-00:00

Concurrency: Prac\-tice and Experience, Vol. 5, No. 7. (1993), pp. 575-602.

The ParaScope Editor is a new kind of interactive parallel programming tool for developing scientific Fortran programs. It assists the knowledgeable user by displaying the results of sophisticated program analyses and by providing editing and a set of powerful interactive transformations. After an edit or parallelism-enhancing transformation, the ParaScope Editor incrementally updates both the analyses and source quickly. This paper describes the underlying implementation of the ParaScope...

Program transformation using temporal logic specification

David Lacey — 2008-05-09T14:54:35-00:00

(2003)

Structured Computer Organization (5th Edition)

Andrew Tanenbaum — 2008-05-09T14:41:53-00:00

(25 June 2005)

 This book takes a modern structured, layered approach to understanding computer systems. It's highly accessible - and it's been thoroughly updated to reflect today's most critical new technologies and the latest developments in computer organization and architecture. Tanenbaum’s renowned writing style and painstaking research make this one of the most accessible and accurate books available, maintaining the author’s popular method of presenting a computer as a series of layers, each one built upon the ones below it, and understandable as a separate entity. A CD-ROM for assembly language programmers is available for teachers. For all computer professionals and engineers who need an overview or introduction to computer architecture.

Logic in Computer Science: Modelling and Reasoning about Systems

Michael Huth — 2008-01-13T15:31:44-00:00

(30 August 2004)

The second edition of this successful textbook continues to provide a clear introduction to formal reasoning relevant to the needs of modern computer science and sufficiently exacting for practical applications. Improvements have been made throughout with many new and expanded text sections. The coverage of model-checking has been substantially updated and additional exercises are included. Internet support includes worked solutions for teacher exercises and model solutions to some student exercises. First Edition Hb (2000): 0-521-65200-6 First Edition Pb (2000): 0-521-65602-8

Introduction to Modal and Temporal Mu-Calculi

Julian Bradfield — 2008-05-09T14:36:32-00:00

CONCUR 2002 — Concurrency Theory (2002), pp. 221-231.

Modal mu-calculus is a logic obtained by adding fixpoint operators to ordinary modal logic, or Hennessy-Milner logic. The result is a very expressive logic, sufficient to subsume many other temporal logics such as CTL and CTL✱. The modal mu-calculus is easy to model-check, and so makes a good ‘back-end’ logic for tools; it has an interesting theory, with some major problems still open; but it also has a certain reputation for being hard to read and write. This tutorial provides an introduction to the modal mu-calculus and related logics, suitable for those with some exposure to modal or temporal logic, but without prior knowledge of fixpoint logics. I start by reviewing the basic semantic setting of processes modelled as transition systems,and briefly review basic modal logic and temporal logics such as CTL. I then introduce the modal mu-calculus itself. I cover the formal syntax and semantics, and then give more informally the game-based intuition that is most useful in understanding formula of the logic. I next describe global and local model-checking techniques. Finally, I discuss the relationship between modal mu-calculus, automata and games, and some of the theoretical questions that have been and are now of interest. The tutorial is based around the handbook chapter [1],written with Colin Stirling,which forms the text for the tutorial.

Compiler transformations for high-performance computing

David Bacon — 2008-05-05T18:12:50-00:00

ACM Comput. Surv., Vol. 26, No. 4. (December 1994), pp. 345-420.

Maximum loop distribution and fusion for two-level loops considering code size

M Liu — 2008-05-05T18:10:33-00:00

Parallel Architectures,Algorithms and Networks, 2005. ISPAN 2005. Proceedings. 8th International Symposium on (2005), 6 pp..

In this paper, we propose a technique combining loop distribution with loop fusion to improve the timing performance without increasing the code size of the transformed loops. We first develop the loop distribution theorems that state the conditions distributing any two-level nested loop in the maximum way. Based on the loop distribution theorems, we design an algorithm to conduct maximum loop distribution. Then we propose a technique of maximum loop distribution with direct loop fusion, which performs maximum loop distribution followed by direct loop fusion. The experimental results show that the execution time of the transformed loops by our technique is reduced 41.9% on average compared to the original loops without the increase of the code size.

Practical techniques to augment dependence analysis in the presence of symbolic terms

Gina Goff — 2008-05-05T18:05:45-00:00

(1997)

Chair-Ken Kennedy

Minimum dependence distance tiling of nested loops with non-uniform dependences

S Punyamurtula — 2008-05-05T18:02:23-00:00

Parallel and Distributed Processing, 1994. Proceedings. Sixth IEEE Symposium on (1994), pp. 74-81.

We address the problem of partitioning nested loops with non-uniform (irregular) dependence vectors. Although many methods exist for nested loop partitioning, most of these perform poorly when parallelizing nested loops with irregular dependencies. We apply the results of classical convex theory and principles of linear programming to iteration spaces and show the correspondence between minimum dependence distance computation and iteration space tiling. The cross-iteration dependencies are analyzed by forming an Integer Dependence Convex Hull (IDCH). A simple way to compute minimum dependence distances from the dependence distance vectors of the extreme points of the IDCH is presented. Using these minimum dependence distances the iteration space can be tiled. Iterations in a tile can be executed in parallel and the tiles can be executed with proper synchronization. We demonstrate that our technique gives much better speedup and extracts more parallelism than the existing techniques

The power test for data dependence

M Wolfe — 2008-05-05T17:55:28-00:00

Parallel and Distributed Systems, IEEE Transactions on, Vol. 3, No. 5. (1992), pp. 591-601.

A data dependence decision algorithm called the power test is introduced. The power test is a combination of the extended GCD algorithm and the Fourier-Motzkin method to eliminate variables in a system of inequalities. This is the first test that can generate the information needed for some advanced transformations, and that can handle complex simultaneous loop limits. Previous work in data dependence decision algorithms is reviewed. Some examples which motivated the development of this test are examined, including those which demonstrate the additional power of the power test. Although it may be too expensive for use as a general-purpose dependence test in a compiler, the power test has proved useful in an interactive program restructuring environment

Automated soundness proofs for dataflow analyses and transformations via local rules

Sorin Lerner — 2005-06-11T04:21:32-00:00

Vol. 40, No. 1. (January 2005), pp. 364-377.

On exact data dependence analysis

Kleanthis Psarris — 2008-05-05T17:37:34-00:00

(1992), pp. 303-312.

A practical algorithm for exact array dependence analysis

William Pugh — 2008-05-05T15:45:58-00:00

Commun. ACM, Vol. 35, No. 8. (August 1992), pp. 102-114.

A Survey of Parallel Machine Organization and Programming

David Kuck — 2008-05-05T14:56:21-00:00

ACM Comput. Surv., Vol. 9, No. 1. (March 1977), pp. 29-59.

Efficient and exact data dependence analysis

Dror Maydan — 2008-05-05T14:53:41-00:00

(1991), pp. 1-14.

Delinearization: an efficient way to break multiloop dependence equations

Vadim Maslov — 2008-05-05T14:50:20-00:00

SIGPLAN Not., Vol. 27, No. 7. (July 1992), pp. 152-161.

Automatically proving the correctness of program analyses and transformations

Sorin Lerner — 2008-05-05T14:47:39-00:00

(2006)

Adviser-Craig Chambers

Dependency Analysis Of For-Loop Structures For Automatic Parallization Of C Code

Tim Jacobson — 2008-05-05T14:45:18-00:00

(April 2003)

Dependence Testing for Parallelizing Compilers

Franjo Plavec — 2008-05-05T14:08:40-00:00

(May 2003)

Definitions of dependence distance

William Pugh — 2008-05-04T22:45:37-00:00

ACM Lett. Program. Lang. Syst., Vol. 1, No. 3. (September 1992), pp. 261-265.

An Overview of Cache Optimization Techniques and Cache-Aware Numerical Algorithms

Markus Kowarschik — 2008-05-04T22:32:40-00:00

Algorithms for Memory Hierarchies (2003), pp. 213-232.

In order to mitigate the impact of the growing gap between CPU speed and main memory performance, today’s computer architectures implement hierarchical memory structures. The idea behind this approach is to hide both the low main memory bandwidth and the latency of main memory accesses which is slow in contrast to the floating-point performance of the CPUs. Usually, there is a small and expensive high speed memory sitting on top of the hierarchy which is usually integrated within the processor chip to provide data with low latency and high bandwidth; i.e., the CPU registers. Moving further away from the CPU, the layers of memory successively become larger and slower. The memory components which are located between the processor core and main memory are called cache memories or caches. They are intended to contain copies of main memory blocks to speed up accesses to frequently needed data [378], [392]. The next lower level of the memory hierarchy is the main memory which is large but also comparatively slow. While external memory such as hard disk drives or remote memory components in a distributed computing environment represent the lower end of any common hierarchical memory design, this paper focuses on optimization techniques for enhancing cache performance.

Reordering the statements with dependence cycles to improve the performance of parallel loops

Chih-Ping Chu — 2008-05-04T22:10:32-00:00

Parallel and Distributed Systems, 1997. Proceedings., 1997 International Conference on (1997), pp. 322-328.

In this paper, we study the exploitation of statement-level parallelism in dependence cycles of Do-loops executed in a random (general) synchronization mode, with emphasis on the effect of statement ordering on parallelism level. For a dependence cycle of a single parallel loop, the parallelism exposed, in general, varies with the alignment of statements. Statement reordering (without modifying the semantics) relies on the compile-time prediction of execution-time of the loop. An improved timing formula and the derived algorithm of statement reordering in single Do loop with dependence cycles to improve the performance of parallel loops are proposed and discussed

An analysis of recurrence relations in Fortran Do-loops for vector processing

Chih-Ping Chu — 2008-05-04T22:07:32-00:00

Parallel Processing Symposium, 1991. Proceedings., Fifth International (1991), pp. 619-625.

Analyzes the recurrences from the breakability of the dependence links. The major findings include: (1) The node splitting algorithm cannot be used directly to break an essential antidependence link, of which the source variable that results in antidependence is itself the sink variable of another true dependence. (2) A sink variable renaming technique, which can reposition an undesired antidependence and/or output dependence link, is capable of breaking an antidependence and/or output-dependence link. (3) For recurrences connected by only true dependences, a dynamic dependence concept and the derived technique are powerful in terms of parallelism exploitation. (4) By the employment of global dependence testing, link-breaking strategy, Tarjan's depth-first search algorithm, and a topological sorting, an algorithm for resolving a general multistatement recurrence is proposed

Automatic translation of FORTRAN programs to vector form

Randy Allen — 2008-05-02T02:46:14-00:00

ACM Trans. Program. Lang. Syst., Vol. 9, No. 4. (October 1987), pp. 491-542.

Using Z: Specification, Refinement, and Proof (Prentice-Hall International Series in Computer Science)

Jim Woodcock — 2008-05-01T21:10:19-00:00

(22 March 1996)

Compilers: Principles, Techniques, and Tools (2nd Edition)

Alfred Aho — 2007-01-10T13:19:52-00:00

(31 August 2006)

 This book provides the foundation for understanding the theory and pracitce of compilers. Revised and updated, it reflects the current state of compilation. Every chapter has been completely revised to reflect developments in software engineering, programming languages, and computer architecture that have occurred since 1986, when the last edition published. The authors, recognizing that few readers will ever go on to construct a compiler, retain their focus on the broader set of problems faced in software design and software development. Computer scientists, developers, and aspiring students that want to learn how to build, maintain, and execute a compiler for a major programming language.

Practical dependence testing

G Goff — 2008-05-01T21:03:39-00:00

SIGPLAN Notices, Vol. 26, No. 6. (June 1991), pp. 15-29.

Precise and efficient dependence tests are essential to the effectiveness of a parallelizing compiler. This paper proposes a dependence testing scheme based on classifying pairs of subscripted variable references. Exact yet fast dependence tests are presented for certain classes of array references, as well as empirical results showing that these references dominate scientific Fortran codes. These dependence tests are being implemented at Rice University in both PFC, a parallelizing compiler,...

A loop parallelization algorithm for HPF compilers

Kazuaki Ishizaki — 2008-05-01T20:35:24-00:00

Languages and Compilers for Parallel Computing (1996), pp. 176-190.

This paper presents a formalized loop parallelization algorithm for effectively extracting parallelism from data to be allocated to processors with array decomposition directives, in languages such as High Performance Fortran (HPF). We define a communication dependence vector that shows data dependence among processors, and use it in our algorithm to formalize and unify the detection of vector prefetch communication and vector pipeline communication for loop parallelization. The paper also presents a method, based on our algorithm for generating vector communications. We implemented the algorithm in our HPF compiler and carried out experiments with two applications on an IBM RS/6000 Scalable POWERparallel System.