## Search

Now showing items 1-10 of 90

#### Combining Analysis, Combining Optimizations

(1995-02)

This thesis presents a framework for describing optimizations. It shows how to combine two such frameworks and how to reason about the properties of the resulting framework. The structure of the framework provides insight into when a combination yields better results. Also presented is a simple iterative algorithm for solving these frameworks. A ...

#### Why Is Modal Logic So Robustly Decidable?

(1997-04-12)

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 ...

#### Value-Driven Redundancy Elimination

(1996-04)

Value-driven 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 ...

#### Effective Static Debugging via Componential Set-Based Analysis

(1997-08-28)

Sophisticated software systems are inherently complex. Understanding, debugging and maintaining such systems requires inferring high-level characteristics of the system's behavior from a myriad of low-level details. For large systems, this quickly becomes an extremely difficult task. MrSpidey is a static debugger that augments the programmers ability ...

#### Improving TLB Miss Handling with Page Table Pointer Caches

(1997-12-16)

Page table pointer caches are a hardware supplement for TLBs that cache pointers to pages of page table entries rather than page table entries themselves. A PTPC traps and handles most TLB misses in hardware with low overhead (usually a single memory access). PTPC misses are filled in software, allowing for an easy hardware implementation, similar ...

#### Ants and Reinforcement Learning: A Case Study in Routing in Dynamic Networks

(1997-02-17)

We investigate two new distributed routing algorithms for data networks based on simple biological "ants" that explore the network and rapidly learn good routes, using a novel variation of reinforcement learning. These two algorithms are fully adaptive to topology changes and changes in link costs in the network, and have space and computational ...

#### Practical Techniques to Augment Dependence Analysis in the Presence of Symbolic Terms

(1997-05)

Dependence analysis is an indispensable tool in the automatic vectorization and parallelization of sequential programs, but performing symbolic dependence analysis can be costly and may fail to resolve many unknown terms. In this thesis, we explore ways to overcome the problems symbolic terms create for dependence analysis. We investigate three ...

#### Fixpoint Logics, Relational Machines, and Computational Complexity

(1996-10-11)

We establish a general connection between fixpoint logic and complexity. On one side, we have fixpoint logic, parameterized by the choices of 1st-order operators (inflationary or noninflationary) and iteration constructs (deterministic, nondeterministic, or alternating). On the other side, we have the complexity classes between P and EXPTIME. Our ...

#### Relating Linear and Branching Model Checking

(1998-06-08)

The difference in the complexity of branching and linear model checking has been viewed as an argument in favor of the branching paradigm. In particular, the computational advantage of CTL model checking over LTL model checking makes CTL a popular choice, leading to efficient model-checking tools for this logic. Can we use these tools in order to ...

#### The Maximum of a Random Walk and Its Application to Rectangle Packing

(1997-07-28)

Let S0,...,Sn be a symmetric random walk that starts at the origin (S0 = 0), and takes steps uniformly distributed on [-1,+1]. We study the large-n behavior of the expected maximum excursion and prove the estimate$$ \exd \max_{0 \leq k \leq n} S_k = \sqrt{\frac{2n}{3\pi}} c +\frac{1}{5}\sqrt{\frac{2}{3\pi}} n^{-1/2} + O(n^{-3/2}), where c = 0.297952... ...