Now showing items 41-60 of 245

    • Behavioral Interface Contracts for Java 

      Felleisen, Matthias; Findler, Robert Bruce (2005-08-25)
      Programs should consist of off-the-shelf, interchangeable, black-box components that are produced by a network of independent software companies. These components should not only come with type signatures but also with contracts that describe other aspects of their behavior. One way to express contracts is to state preand postconditions for externally ...
    • Behavioral Software Contracts 

      Findler, Robert Bruce (2002-04-01)
      To sustain a market for software components, component producers and consumers must agree on contracts. These contracts must specify each party’s obligations. To ensure that both sides meet their obligations, they must also agree on standards for monitoring contracts and assigning blame for contract violations This dissertation explores these issues ...
    • Bisimulation Minimization in an Automata-Theoretic Verification Framework 

      Fisler, Kathi; Vardi, Moshe Y. (1998-10-27)
      Bisimulation is a seemingly attractive state-space minimization technique because it can be computed automatically and yields the smallest model preserving all mu -calculus formulas. It is considered impractical for symbolic model checking, however, because the required BDDs are prohibitively large for most designs. We revisit bisimulation minimization, ...
    • BMS-CnC: Bounded Memory Scheduling of Dynamic Task Graphs 

      Budimlić, Zoran; Sarkar, Vivek; Sbîrlea, Dragoș (2013-10-24)
      It is now widely recognized that increased levels of parallelism is a necessary condition for improved application performance on multicore computers. However, as the number of cores increases, the memory-per-core ratio is expected to further decrease, making per-core memory efficiency of parallel programs an even more important concern in future ...
    • Bottleneck Characterization of Dynamic Web Site Benchmarks 

      Amza, Cristiana; Cecchet, Emmanuel; Chanda, Anupam; Cox, Alan; Elnikety, Sameh; (2002-02)
      The absence of benchmarks for Web sites with dynamic content hasbeen a major impediment to research in this area. We describe three benchmarks for evaluating the performance of Web sites with dynamic content. The benchmarks model three common types of dynamic-content Web sites with widely varying application characteristics: an online bookstore, an ...
    • Building a Control-flow Graph from Scheduled Assembly Code 

      Cooper, Keith D.; Harvey, Timothy J.; Waterman, Todd (2002-02-01)
      A variety of applications have arisen where it is worthwhile to apply code optimizations directly to the machine code (or assembly code) produced by a compiler. These include link-time whole-program analysis and optimization, code compression, binary- to-binary translation, and bit-transition reduction (for power). Many, if not most, optimizations ...
    • Building Adaptive Compilers 

      Almagor, L.; Cooper, Keith D.; Grosul, Alexander; Harvey, Timothy J.; Reeves, Steven W.; (2005-01-29)
      Traditional compilers treat all programs equally -that is, they apply the same set of techniques to every program that they compile. Compilers that adapt their behavior to fit specific input programs can produce better results. This paper describes out experience building and using adaptive compilers. It presents experimental evidence to show two ...
    • Building Incentives into Tor 

      Dingledine, Roger; Ngan, Tsuen-Wan "Johnny"; Wallach, Dan S. (2008-11-12)
      Distributed anonymous communication networks like Tor depend on volunteers to donate their resources. However, the efforts of Tor volunteers have not grown as fast as the demands on the Tor network. We explore techniques to incentivize Tor users to relay Tor traffic too; if users contribute resources to the Tor overlay, they should receive faster ...
    • C++.T Formalization in Isar 

      Siek, Jeremy G.; Taha, Walid (2005-12-16)
      A formal account of C++ templates, including the compile-time and run-time semantics. The main result is a proof of type safety. The proof is written in the Isar proof language and can be mechanically verified using the Isabelle 2005 proof assistant.
    • Cache Coherence Using Local Knowledge 

      Darnell, Ervan (1995-04-01)
      Hiding memory latency is critical in modern machines. Typically, machines have used cache and addressed the ensuing cache coherence problem with hardware or VM-based strategies that rely on global inter-cache communication.However, global communication limits scalability. "Local knowledge" coherence strategies, which use compile-time information to ...
    • Cache Management in Scalable Network Servers 

      Pai, Vivek (2000-07-13)
      For many users, the perceived speed of computing is increasingly dependent on the performance of network server systems, underscoring the need for high performance servers. Cost-effective scalable network servers can be built on clusters of commodity components (PCs and LANs) instead of using expensive multiprocessor systems. However, network servers ...
    • Classes and Mixins 

      Felleisen, Matthias; Flatt, Matthew; Krishnamurthi, Shriram (1999)
      While class-based object-oriented programming languages provide a flexible mechanism for re-using and managing related pieces of code, they typically lack linguistic facilities for specifying a uniform extension of many classes with one set of fields and methods. As a result, programmers are unable to express certain abstractions over classes. In ...
    • Combining Analysis, Combining Optimizations 

      Click, Clifford Noel, Jr. (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 ...
    • Combining Particles and Waves for Fluid Animation 

      Hall, Mark (1992-04)
      Modeling fluid motion is a problem largely unsolved by traditional modeling techniques. Animation of fluid motion has been possible only in special cases, falling into one of two general categories. Upper surface representations model wave phenomena for fluid in placid situations, such as calm ocean waves. Particle systems define the chaotic motion ...
    • COMMA: Coordinating the Migration of Multi-tier Applications 

      Liu, Zhaolei; Ng, T. S. Eugene; Sripanidkulchai, Kunwadee; Zheng, Jie (2014-11-24)
      Multi-tier applications are widely deployed in today’s virtualized cloud computing environments. At the same time, management operations in these virtualized environments, such as load balancing, hardware maintenance, workload consolidation, etc., often make use of live virtual machine (VM) migration to control the placement of VMs. Although existing ...
    • Commit Phase Variations in Timestamp-based Software Transactional Memory 

      Zhang, Rui; Budimli?, Zoran; Scherer, William N., III (2008-02-11)
      Timestamp-based Software Transactional Memory (STM) validation techniques use a global shared counter and timestamping of objects being written to reason about sequencing of transactions and their linearization points, while reducing the number of unnecessary validations that have to be performed, thus improving overall system performance. During the ...
    • Communication Generation for Data-Parallel Languages 

      Sethi, Ajay (1996-12)
      Data-parallel languages allow programmers to use the familiar machine-independent programming style to develop programs for multiprocessor systems. These languages relieve users of the tedious task of inserting interprocessor communication and delegate this crucial and error-prone task to the compilers for the languages. Since remote access in ...
    • Communication Optimizations for Distributed-Memory X10 Programs 

      Barik, Rajkishore; Budimlić, Zoran; Grove, David; Peshansky, Igor; Sarkar, Vivek; (2010-04-10)
      X10 is a new object-oriented PGAS (Partitioned Global Address Space) programming language with support for distributed asynchronous dynamic parallelism that goes beyond past SPMD message-passing models such as MPI and SPMD PGAS models such as UPC and Co-Array Fortran. The concurrency constructs in X10 make it possible to express complex computation ...
    • Compilation Order Matters: Exploring the Structure of the Space of Compilation Sequences Using Randomized Search Algorithms 

      Almagor, L.; Cooper, Keith D.; Grosul, Alexander; Harvey, Timothy J.; Reeves, Steven W.; (2004-06-18)
      Most modern compilers operate by applying a fixed sequence of code optimizations, called a compilation sequence, to all programs. Compiler writers determine a small set of good, general-purpose, compilation sequences by extensive hand-tuning over particular benchmarks. The compilation sequence makes a significant difference in the quality of the ...
    • Compiler Support for Machine-Independent Parallelization of Irregular Problems 

      von Hanxleden, Reinhard (1994-12-01)
      Data-parallel languages, such as HIGH PERFORMANCE FORTRAN or FORTRAND, provide a machine-independent data-parallel programming paradigm in which the applications programmer uses a dialect of a sequential language annotated with high-level data-distribution directives. Identifying parallelism in data-parallel applications typically is straightforward, ...