Browsing Computer Science Technical Reports by Title
Now showing items 233245 of 245

Understanding Unfulfilled Memory Reuse Potential in Scientific Applications
(20071005)The potential for improving the performance of dataintensive scientific programs by enhancing data reuse in cache is substantial because CPUs are significantly faster than memory. Traditional performance tools typically collect or simulate cache miss counts or rates and attribute them at the function level. While such information identifies program ... 
Uniform Logical Relations
(20110401)Strong Normalization (SN) is an important property for intensional constructive type theories such as the Calculus of Inductive Constructions (CiC), the basis for the Coq theorem prover. Not only does SN imply consistency, but it also ensures that typechecking is decidable, and further, it provides a straightforward model, the term model, for a ... 
Universal Domains for Sequential Computation
(199505)Classical recursion theory asserts that all conventional programming languages are equally expressive because they can define all partial recursive functions over the natural numbers. However, most real programming languages support some form of higherorder data such as potentially infinite streams, lazy trees, and functions. Since these objects do ... 
UserSpecified and Automatic Data Layout Selection for Portable Performance
(20130425)This paper describes a new approach to managing array data layouts to optimize performance for scientific codes. Prior research has shown that changing data layouts (e.g., interleaving arrays) can improve performance. However, there have been two major reasons why such optimizations are not widely used: (1) the need to select different layouts for ... 
Using Problem Topology in Parallelization
(199409)Problem topology is the key to efficient parallelization support for partially regular applications. Specifically, problem topology provides the information necessary for automatic data distribution and regular application optimization of partially regular applications. Problem topology is the dimensionality, size, and connectivity of the problem. ... 
ValueDriven Redundancy Elimination
(199604)Valuedriven redundancy elimination is a combination of value numbering and code motion. Value numbering is an optimization that assigns numbers to values in such a way that two values are assigned the same number if the compiler can prove they are equal. When this optimization discovers two computations that produce the same value, it can (under ... 
Variational Subdivision for Laplacian Splines
(19971003)The fundamental problem of geometric design is the representation of curved shapes. Traditionally such shapes are represented by parametric spline curves, e.g. NURBS, which are defined as the minimizers of variational problems. For example, cubic Bsplines minimize the bending energy functional. More recently subdivision curves and surfaces emerged ... 
Verification of Fair Transition Systems
(19970827)In program verification we check that an implementation meets its specification. Both the specification and the implementation describe the possible behaviors of the program, though at different levels of abstraction. We distinguish between two approaches to implementation of specifications. The first approach is tracebased implementation, where we ... 
Verification of Open Systems
(19980404)In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of ... 
WellFounded Touch Optimization for Futures
(19941001)The future annotations of MultiLisp provide a simple method for taming the implicit parallelism of functional programs, but require touch operations at all placeholderstrict positions of program operations to ensure proper synchronization between threads. These touch operations contribute substantially to a program's execution time. We use an ... 
Why Is Modal Logic So Robustly Decidable?
(19970412)In the last 20 years modal logic has been applied to numerous areas of computer science, including artificial intelligence, program verification, hardware verification, database theory, and distributed computing. There are two main computational problems associated with modal logic. The first problem is checking if a given formula is true in a given ... 
WorkFirst and HelpFirst Scheduling Policies for Terminally Strict Parallel Programs
(20081113)Multiple programming models are emerging to address an increased need for dynamic task parallelism in applications for multicore processors and sharedaddress space parallel computing. Examples include OpenMP 3.0, Java Concurrency Utilities, Microsoft Task Parallel Library, Intel Thread Building Blocks, Cilk, X10, Chapel, and Fortress. Scheduling ... 
λ group: Using Optics to Take Group Data Delivery in the Datacenter to the Next Degree
(20140217)The increasing number of datacenter applications with heavy onetomany communications has raised the need for an efficient group data delivery solution. This paper presents an unconventional cleanslate architecture called λ group that uses optical networking technologies to enable ultrafast, energyefficient, low cost, and highly reliable group ...