bluuebunny/crossref_metadata_2025 huggingface dataset:
Model checking and modular verification
Authors: Grumberg Orna , Long David E.
Published: October 2002

We describe a framework for compositional verification of finite-state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition, and a preorder on structures which captures the relation between a component and a system containing the component. Satisfaction of a formula in the logic corresponds to being below a particular structure (a tableau for the formula) in the preorder. We show how to do assume-guarantee-style reasoning within this framework. Additionally, we demonstrate efficient methods for model checking in the logic and for checking the preorder in several special cases. We have implemented a system based on these methods, and we use it to give a compositional verification of a CPU controller.
Modular logic programming
Authors: Brogi Antonio , Mancarella Paolo , Pedreschi Dino , Turini Franco
Published: October 2002

Modularity is a key issue in the design of modern programming languages. When designing modular features for declarative languages in general, and for logic programming languages in particular, the challenge lies in avoiding the superimposition of a complex syntactic and semantic structure over the simple structure of the basic language. The modular framework defined here for logic programming consists of a small number of operations over modules which are (meta-) logically defined and semantically justified in terms of the basic logic programming semantics. The operations enjoy a number of algebraic properties, thus yielding an algebra of modules. Despite its simplicity, the suite of operations is shown capable of capturing the core features of modularization: information hiding, import/export relationships, and construction of module hierarchies. A metalevel implementation and a compilation-oriented implementation of the operations are provided and proved sound with respect to the semantics. The compilation-oriented implementation is based on manipulation of name spaces and provides the basis for an efficient implementation.
Improving the ratio of memory operations to floating-point operations in loops
Authors: Carr Steve , Kennedy Ken
Published: October 2002

Over the past decade, microprocessor design strategies have focused on increasing the computational power on a single chip. Because computations often require more data from cache per floating-point operation than a machine can deliver and because operations are pipelined, idle computational cycles are common when scientific applications are executed. To overcome these bottlenecks, programmers have learned to use a coding style that ensures a better balance between memory references and floating-point operations. In our view, this is a step in the wrong direction because it makes programs more machine-specific. A programmer should not be required to write a new program version for each new machine; instead, the task of specializing a program to a target machine should be left to the compiler.

But is our view practical? Can a sophisticated optimizing compiler obviate the need for the myriad of programming tricks that have found their way into practice to improve the performance of the memory hierarchy? In this paper we attempt to answer that question. To do so, we develop and evaluate techniques that automatically restructure program loops to achieve high performance on specific target architectures. These methods attempt to balance computation and memory accesses and seek to eliminate or reduce pipeline interlock. To do this, they estimate statically the balance between memory operations and floating-point operations for each loop in a particular program and use these estimates to determine whether to apply various loop transformations.

Experiments with our automatic techniques show that integer-factor speedups are possible on kernels. Additionally, the estimate of the balance between memory operations and computation, and the application of the estimate are very accurate—experiments reveal little difference between the balance achieved by our automatic system that is made possible by hand optimization.
Supporting dynamic data structures on distributed-memory machines
Authors: Rogers Anne , Carlisle Martin C. , Reppy John H. , Hendren Laurie J.
Published: October 2002

Compiling for distributed-memory machines has been a very active research area in recent years. Much of this work has concentrated on programs that use arrays as their primary data structures. To date, little work has been done to address the problem of supporting programs that use pointer-based dynamic data structures. The techniques developed for supporting SPMD execution of array-based programs rely on the fact that arrays are statically defined and directly addressable. Recursive data structures do not have these properties, so new techniques must be developed. In this article, we describe an execution model for supporting programs that use pointer-based dynamic data structures. This model uses a simple mechanism for migrating a thread of control based on the layout of heap-allocated data and introduces parallelism using a technique based on futures and lazy task creation. We intend to exploit this execution model using compiler analyses and automatic parallelization techniques. We have implemented a prototype system, which we callOlden, that runs on the Intel iPSC/860 and the Thinking Machines CM-5. We discuss our implementation and report on experiments with five benchmarks.
A type system equivalent to flow analysis
Authors: Palsberg Jens , O'Keefe Patrick
Published: October 2002

Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis. In this article we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.
Error repair in shift-reduce parsers
Authors: McKenzie Bruce J. , Yeatman Corey , de Vere Lorraine
Published: October 2002

Local error repair of strings during CFG parsing requires the insertion and deletion of symbols in the region of a syntax error to produce a string that is error free. Rather than precalculating tables at parser generation time to assist in finding such repairs, this article shows how such repairs can be found during shift-reduce parsing by using the parsing tables themselves. This results in a substantial space saving over methods that require precalculated tables. Furthermore, the article shows how the method can be integrated with lookahead to avoid finding repairs that immediately result in further syntax errors. The article presents the results of experiments on a version of the LALR(1)-based parser generator
Bison
to which the algorithm was added.
Constrained types and their expressiveness
Authors: Palsberg Jens , Smith Scott
Published: October 2002

A constrained type consists of both a standard type and a constraint set. Such types enable efficient type inference for object-oriented languages with polymorphism and subtyping, as demonstrated by Eifrig, Smith, and Trifonov. Until now, it has been unclear how expressive constrained types are. In this article we study constrained types without universal quantification. We prove that they accept the same programs as the type system of Amadio and Cardelli with subtyping and recursive types. This result gives a precise connection between constrained types and the standard notion of types.
On subtyping and matching
Authors: Abadi Martín , Cardelli Luca
Published: October 2002

A relation between recursive object types, called
matching
, has been proposed as a generalization of subtyping. Unlike subtyping, matching does not support subsumption, but it does support inheritance of binary methods. We argue that matching is a good idea, but that it should not be regarded as a form of F-bounded subtyping (as was originally intended). We show that a new interpretation of matching as higher-order subtyping has better properties. Matching turns out to be a third-order construction, possibly the only one to have been proposed for general use in programming.
A new analysis of LALR formalisms
Authors: Park Joseph C.H. , Choe K. M. , Chang C. H.
Published: October 2002

The traditional LALR analysis is reexamined using a new operator and an associated graph. An improved method that allows factoring out a crucial part of the computation for defining states of LR(0) canonical collection and for computing LALR(1) lookahead sets is presented. This factorization leads to significantly improved algorithms with respect to execution time as well as storage requirements. Experimental results including comparison with other known methods are presented.
Kleene algebra with tests
Authors: Kozen Dexter
Published: October 2002

We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every
while
program can be simulated by a while program can be simulated by a
while
program with at most one
while
loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.
Interprocedural control flow analysis of first-order programs with tail-call optimization
Authors: Debray Saumya K. , Proebsting Todd A.
Published: October 2002

Knowledge of low-level control flow is essential for many compiler optimizations. In systems with tail-call optimization, the determination of interprocedural control flow is complicated by the fact that because of tail-call optimization, control flow at procedure returns is not readily evident from the call graph of the program. This article shows how interprocedural control-flow analysis of first-order programs can be carried out using well-known concepts from parsing theory. In particular, we show that context-insensitive ( or zeroth-order) control-flow analysis corresponds to the notion of FOLLOW sets in context-free grammars, while context-sensitive (or first-order) control-flow analysis corresponds to the notion of LR(1) items. The control-flow information so obtained can be used to improve the precision of interprocedural dataflow analyses as well as to extend certain low-level code optimizations across procedure boundaries.
The design, implementation, and evaluation of Jade
Authors: Rinard Martin C. , Lam Monica S.
Published: October 2002

Jade is a portable, implicitly parallel language designed for exploiting task-level concurrency.Jade programmers start with a program written in a standard serial, imperative language, then use Jade constructs to declare how parts of the program access data. The Jade implementation uses this data access information to automatically extract the concurrency and map the application onto the machine at hand. The resulting parallel execution preserves the semantics of the original serial program. We have implemented Jade as an extension to C, and Jade implementations exist for s hared-memory multiprocessors, homogeneous message-passing machines, and heterogeneous networks of workstations. In this atricle we discuss the design goals and decisions that determined the final form of Jade and present an overview of the Jade implementation. We also present our experience using Jade to implement several complete scientific and engineering applications. We use this experience to evaluate how the different Jade language features were used in practice and how well Jade as a whole supports the process of developing parallel applications. We find that the basic idea of preserving the serial semantics simplifies the program development process, and that the concept of using data access specifications to guide the parallelization offers significant advantages over more traditional control-based approaches. We also find that the Jade data model can interact poorly with concurrency patterns that write disjoint pieces of a single aggregate data structure, although this problem arises in only one of the applications.
Proofs about a folklore let-polymorphic type inference algorithm
Authors: Lee Oukseh , Yi Kwangkeun
Published: October 2002

The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the
de facto
standard Algorithm 𝒲 that is bottom-up (or context-insensitive), and the other is a “folklore” algorithm that is top-down (or context-sensitive). Because the latter algorithm has not been formally presented with its soundness and completeness proofs, and its relation with the 𝒲 algorithm has not been rigorously investigated, its use in place of (or in combination with) 𝒲 is not well founded. In this article, we formally define the context-sensitive, top-down type inference algorithm (named “M”), prove its soundness and completeness, and show a distinguishing property that M always stops earlier than 𝒲 if the input program is ill typed. Our proofs can be seen as theoretical justifications for various type-checking strategies being used in practice.
Efficient and flexible incremental parsing
Authors: Wagner Tim A. , Graham Susan L.
Published: October 2002

Previously published algorithms for LR (
k
) incremental parsing are inefficient, unnecessarily restrictive, and in some cases incorrect. We present a simple algorithm based on parsing LR(
k
) sentential forms that can incrementally parse an arbitrary number of textual and/or structural modifications in optimal time and with no storage overhead. The central role of
balanced sequences
in achieving truly incremental behavior from analysis algorithms is described, along with automated methods to support balancing during parse table generation and parsing. Our approach extends the theory of sentential-form parsing to allow for
ambiguity
in the grammar, exploiting it for notational convenience, to denote sequences, and to construct compact (“abstract”) syntax trees directly. Combined, these techniques make the use of automatically generated incremental parsers in interactive software development environments both practical and effective. In addition, we address
information preservation
in these environments: Optimal node reuse is defined; previous definitions are shown to be insufficient; and a method for detecting node reuse is provided that is both simpler and faster than existing techniques. A program representation based on
self-versioning documents
is used to detect changes in the program, generate efficient change reports for subsequent analyses, and allow the parsing transformation itself to be treated as a reversible modification in the edit log.
Alma-O
Authors: Apt Krzysztof R. , Brunekreef Jacob , Partington Vincent , Schaerf Andrea
Published: October 2002

We describe here an implemented small programming language, called Alma-O, that augments the expressive power of imperative programming by a limited number of features inspired by the logic programming paradigm. These additions encourage declarative programming and make it a more attractive vehicle for problems that involve search. We illustrate the use of Alma-O by presenting solutions to a number of classical problems, including α-β search, STRIPS planning, knapsack, and Eight Queens. These solutions are substantially simpler than their counterparts written in the imperative or in the logic programming style and can be used for different purposes without any modification. We also discuss here the implementation of Alma-O and an operational, executable, semantics of a large subset of the language.
Effectivness of abstract interpretation in automatic parallelization
Authors: Bueno Francisco , García de la Banda María , Hermenegildo Manuel
Published: October 2002

We report on a detailed study of the application and effectiveness of program analysis based on abstract interpretation of automatic program parallelization. We study the case of parallelizing logic programs using the notion of strict independence. We first propose and prove correct a methodology for the application in the parallelization task of the information inferred by abstract interpretation, using a parametric domain. The methodology is generic in the sense of allowing the use of different analysis domains. A number of well-known approximation domains are then studied and the transformation into the parametric domain defined. The transformation directly illustrates the revelance and applicability of each abstract domain for the application. Both local and global analyzers are then built using these domains and embedded in a complete parallelizing compiler. Then, the performance of the domains in this context is assessed through a number of experiments. A comparatively wide range of aspects is studied, from the resources needed by the analyzers in terms of time and memory to the actual benefits obtained from the information inferred. Such benefits are evaluated both in terms of the characteristics of the parallelized code and of the actual speedups obtained from it. The results show that data flow analysis plays an important role in achieving efficient parallelizations, and that the cost of such analysis con be reasonable even for quite sophisticated abstract domains. Furthermore, the results also offer significant insight into the characteristics of the domains, the demands of the application, and the trade-offs involved.
C and tcc
Authors: Poletto Massimiliano , Hsieh Wilson C. , Engler Dawson R. , Kaashoek M. Frans
Published: October 2002

Dynamic code generation allows programmers to use run-time information in order to achieve performance and expressiveness superior to those of static code. The 'C(Tick C) language is a superset of ANSI C that supports efficient and high-level use of dynamic code generation. 'C provides dynamic code generation at the level of C expressions and statements and supports the composition of dynamic code at run time. These features enable programmers to add dynamic code generation to existing C code incrementally and to write important applications (such as “just-in-time” compilers) easily. The article presents many examples of how 'C can be used to solve practical problems. The tcc compiler is an efficient, portable, and freely available implementation of 'C. tcc allows programmers to trade dynamic compilation speed for dynamic code quality: in some aplications, it is most important to generate code quickly, while in others code quality matters more than compilation speed. The overhead of dynamic compilation is on the order of 100 to 600 cycles per generated instruction, depending on the level of dynamic optimizaton. Measurements show that the use of dynamic code generation can improve performance by almost an order of magnitude; two- to four-fold speedups are common. In most cases, the overhead of dynamic compilation is recovered in under 100 uses of the dynamic code; sometimes it can be recovered within one use.
Should your specification language be typed
Authors: Lamport Leslie , Paulson Lawrence C.
Published: October 2002

Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased somplexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages, too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verificaiton, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language.

We consider only specification languages, not programming languages.
Towards monolingual programming environments
Authors: Heering Jan , Klint Paul
Published: October 2002

Most programming environments are much too complex. One way of simplifying them is to reduce the number of mode-dependent languages the user has to be familiar with. As a first step towards this end, the feasibility of unified command/programming/debugging languages, and the concepts on which such languages have to be based, are investigated. The unification process is accomplished in two phases. First, a unified command/programming framework is defined and, second, this framework is extended by adding an integrated debugging capability to it. Strict rules are laid down by which to judge language concepts presenting themselves as candidates for inclusion in the framework during each phase. On the basis of these rules many of the language design questions that have hitherto been resolved this way or that, depending on the taste of the designer, lose their vagueness and can be decided in an unambiguous manner.
Is Sometimes Ever Better Than Always?
Authors: Gries David
Published: October 2002

The “intermittent assertion” method for proving programs correct is explained and compared with the conventional method. Simple conventional proofs of iterative algorithms that compute recursively defined functions, including Ackermann's function, are given.
Noncanonical SLR(1) Grammars
Authors: Tai Kou-Chung
Published: October 2002

Two noncanonical extensions of the simple LR(1) (SLR(1)) method are presented, which reduce not only handles but also other phrases of sentential forms. A class of context-free grammars called
leftmost
SLR(1) (LSLR(1)) is defined by using lookahead symbols which appear in leftmost derivations. This class includes the SLR(1), reflected SMSP, and total precedence grammars as proper subclasses. The class of LSLR(1) languages properly includes the deterministic context-free languages, their reflections, and total precedence languages. By requiring that phrases which have been scanned be reduced as early as possible, a larger class of context-free grammars called
noncanonical
SLR(1) (NSLR(1)) is defined. The NSLR(1) languages can be recognized deterministically in linear time using a two-stack pushdown automaton. An NSLR(1) parser generator has been implemented. Empirical results show that efficient NSLR(1) parsers can be constructed for some non-LR grammars which generate nondeterministic languages. Applications of the NSLR(1) method to improve the parsing and translation of programming languages are discussed.
Graph rewrite systems for program optimization
Authors: Assmann Uwe
Published: October 2002

Graph rewrite systems can be used to specify and generate program optimizations. For termination of the systems several rule-based criteria are developed, defining
exhaustive graph rewrite systems
. For nondeterministic systems
stratification
is introduced which automatically selects single normal forms. To illustrate how far the methodology reaches, parts of the lazy code motion optimization are specified. The resulting graph rewrite system classes can be evaluated by a uniform algorithm, which forms the basis for the optimizer generator OPTIMIX. With this tool several optimizer components have been generated, and some numbers on their speed are presented.
Program transformation and runtime support for threaded MPI execution on shared-memory machines
Authors: Tang Hong , Shen Kai , Yang Tao
Published: October 2002

Parallel programs written in MPI have been widely used for developing high-performance applications on various platforms. Because of a restriction of the MPI computation model, conventional MPI implementations on shared-memory machines map each MPI node to an OS process, which can suffer serious performance degradation in the presence of multiprogramming. This paper studies compile-time and runtime techniques for enhancing performance portability of MPI code running on multiprogrammed shared-memory machines. The proposed techniques allow MPI nodes to be executed safety and efficiently as threads. Compile-time transformation eliminates global and static variables in C code using node-specific data. The runtime support includes an efficient and provably correct communication protocol that uses lock-free data structure and takes advantage of address space sharing among threads. The experiments on SGI Origin 2000 show that our MPI prototype called TMPI using the proposed techniques is competitive with SGI's native MPI implementation in a dedicated environment, and that it has significant performance advantages in a multiprogrammed environment.
The benefits and costs of DyC's run-time optimizations
Authors: Grant Brian , Mock Markus , Philipose Matthai , Chambers Craig , Eggers Susan J.
Published: October 2002

DyC selectively dynamically compiles programs during their execution, utilizing the run-time-computed values of variables and data structures to apply optimizations that are based on partial evaluation. The dynamic optimizations are preplanned at static compile time in order to reduce their run-time cost; we call this
staging
. DyC's staged optimizations include (1) an advanced binding-time analysis that supports polyvariant specialization (enabling both single-way and multiway complete loop unrolling), polyvariant division, static loads, and static calls, (2) low-cost, dynamic versions of traditional global optimizations, such as zero and copy propagation and dead-assignment elimination, and (3) dynamic peephole optimizations, such as strength reduction. Because of this large suite of optimizations and its low dynamic compilation overhead, DyC achieves good performance improvements on programs that are larger and more complex than the kernels previously targeted by other dynamic compilation systems. This paper evaluates the benefits and costs of applying DyC's optimizations. We assess their impact on the performance of a variety of small to medium-sized programs, both for the regions of code that are actually transformed and for the entire application as a whole. Our study includes an analysis of the contribution to performance of individual optimizations, the performance effect of changing the applications' inputs, and a detailed accounting of dynamic compilation costs.
Program transformations in a denotational setting
Authors: Nielson Flemming
Published: October 2002

Program transformations are frequently performed by optimizing compilers, and the correctness of applying them usually depends on data flow information. For language-to-same-language transformations, it is shown how a denotational setting can be useful for validating such program transformations.

Strong equivalence is obtained for transformations that exploit information from a class of forward data flow analyses, whereas only weak equivalence is obtained for transformations that exploit information from a class of backward data flow analyses. To obtain strong equivalence, both the original and the transformed program must be data flow analysed, but consideration of a transformation-exploiting liveness of variables indicates that a more satisfactory approach may be possible.
Virtual time
Authors: Jefferson David R.
Published: October 2002

Virtual time
is a new paradigm for organizing and synchronizing distributed systems which can be applied to such problems as distributed discrete event simulation and distributed database concurrency control. Virtual time provides a flexible abstraction of real time in much the same way that virtual memory provides an abstraction of real memory. It is implemented using the Time Warp mechanism, a synchronization protocol distinguished by its reliance on lookahead-rollback, and by its implementation of rollback via antimessages.
Director strings as combinators
Authors: Kennaway Richard , Sleep Ronan
Published: October 2002

A simple calculus (the Director String Calculus-DSC) for expressing abstractions is introduced, which captures the essence of the “long reach” combinators introduced by Turner. We present abstraction rules that preserve the
applicative structure
of the original lambda term, and that cannot increase the number of subterms in the translation.

A translated lambda term can be reduced according to the evaluation rules of DSC. If this terminates with a DSC normal form, this can be translated into a lambda term using rules presented below. We call this process of abstracting a lambda term, reducing to normal form in the space of DSC terms, and translating back to a lambda term an
implementation
.

We show that our implementation of the lambda calculus is correct: For lambda terms with a normal form that contains no lambdas (
ground terms
), the implementation is shown to yield a lambda calculus normal form. For lambda terms whose normal forms represent functions, it is shown that the implementation yields lambda terms that are beta-convertible in zero or more steps to the normal form of the original lambda term. In this sense, our implementation involves
weak
reduction according to Hindley et al. [9].
Model checking of hierarchical state machines
Authors: Alur Rajeev , Yannakakis Mihalis
Published: October 2002

Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. We investigate the model checking of sequential hierarchical (nested) systems, i.e., finite-state machines whose states themselves can be other machines. This nesting ability is common in various software design methodologies, and is available in several commercial modeling tools. The straightforward way to analyze a hierarchical machine is to flatten it (thus incurring an exponential blow up) and apply a model-checking tool on the resulting ordinary FSM. We show that this flattening can be avoided. We develop algorithms for verifying linear-time requirements whose complexity is polynomial in the size of the hierarchical machine. We also address the verification of branching time requirements and provide efficient algorithms and matching lower bounds.
Examining 25 years of technology in U.S. education
Authors: Norris Cathleen , Soloway Elliot , Sullivan Terry
Published: October 2002

The potential of technology has not been realized in primary and secondary classrooms. What conditions aren't being met, and what must be done.
Primitive types in Java considered harmful
Authors: Ourusoff Nick
Published: October 2002

Expression evaluation raises doubts about Java as an exemplar programming language when teaching the object-oriented paradigm.
Token-based scanning of source code for security problems
Authors: Viega John , Bloch J. T. , Kohno Tadayoshi , McGraw Gary
Published: October 2002

We describe
ITS4
, a tool for statically scanning C and C++ source code for security vulnerabilities. Compared to other approaches, our scanning technique stakes out a new middle ground between accuracy and efficiency. This method is efficient enough to offer real-time feedback to developers during coding while producing few false negatives. Unlike other techniques, our method is also simple enough to scan C++ code despite the complexities inherent in the language. Using
ITS4
, we found new remotely exploitable vulnerabilities in a widely distributed software package as well as in a major piece of e-commerce software.We also describe functionality in more recent tools modeled after
ITS4
, and discuss algorithms that could easily be used to augment these kinds of tools. Particularly, we describe a solution we have prototyped that allows for more rigorous analysis of C and C++ source code, without failing to analyze parts of the program due to preprocessor conditionals.
Design and evaluation of a conit-based continuous consistency model for replicated services
Authors: Yu Haifeng , Vahdat Amin
Published: October 2002

The tradeoffs between consistency, performance, and availability are well understood. Traditionally, however, designers of replicated systems have been forced to choose from either strong consistency guarantees or none at all. This paper explores the semantic space between traditional strong and optimistic consistency models for replicated services. We argue that an important class of applications can tolerate relaxed consistency, but benefit from bounding the maximum rate of inconsistent access in an application-specific manner. Thus, we develop a conit-based continuous consistency model to capture the consistency spectrum using three application-independent metrics,
numerical error
,
order error
, and
staleness
. We then present the design and implementation of TACT, a middleware layer that enforces arbitrary consistency bounds among replicas using these metrics. We argue that the TACT consistency model can simultaneously achieve the often conflicting goals of generality and practicality by describing how a broad range of applications can express their consistency semantics using TACT and by demonstrating that application-independent algorithms can efficiently enforce target consistency levels. Finally, we show that three replicated applications running across the Internet demonstrate significant semantic and performance benefits from using our framework.
Simulating heavy tailed processes using delayed hazard rate twisting
Authors: Juneja Sandeep , Shahabuddin Perwez
Published: October 2002

Consider the problem of estimating the small probability that the maximum of a random walk exceeds a large threshold, when the process has a negative drift and the underlying random variables may have heavy tailed distributions, that is, their tail distribution decays at a subexponential rate. We consider one class of such problems that has applications in estimating the ruin probability associated with insurance claim processes with subexponentially distributed claim sizes, and in estimating the probability of large delays in an
M
/
G
/1 queue with subexponentially distributed service times. Significant work has been done on analogous problems for the light tailed case (when the tail distribution decreases at an exponential rate or faster) that involve importance sampling methods using appropriate exponential twisting. However, for the subexponential case, such exponential twisting is infeasible and alternative techniques are needed. In this paper we introduce importance sampling techniques where the new probability measure is obtained by twisting the hazard rate of the original distribution. For subexponential distributions this amounts to subexponential twisting---twisting at a subexponential rate. In addition, we introduce the technique of "delaying" the twisting and show that the combination of the two techniques produces asymptotically optimal estimates of the small probability mentioned above.
Gradient domain high dynamic range compression
Authors: Fattal Raanan , Lischinski Dani , Werman Michael
Published: October 2002

We present a new method for rendering high dynamic range images on conventional displays. Our method is conceptually simple, computationally efficient, robust, and easy to use. We manipulate the gradient field of the luminance image by attenuating the magnitudes of large gradients. A new, low dynamic range image is then obtained by solving a Poisson equation on the modified gradient field. Our results demonstrate that the method is capable of drastic dynamic range compression, while preserving fine details and avoiding common artifacts, such as halos, gradient reversals, or loss of local contrast. The method is also able to significantly enhance ordinary images by bringing out detail in dark regions.
Real-time 3D model acquisition
Authors: Rusinkiewicz Szymon , Hall-Holt Olaf , Levoy Marc
Published: October 2002

The digitization of the 3D shape of real objects is a rapidly expanding field, with applications in entertainment, design, and archaeology. We propose a new 3D model acquisition system that permits the user to rotate an object by hand and see a continuously-updated model as the object is scanned. This tight feedback loop allows the user to find and fill holes in the model in real time, and determine when the object has been completely covered. Our system is based on a 60 Hz. structured-light rangefinder, a real-time variant of ICP (iterative closest points) for alignment, and point-based merging and rendering algorithms. We demonstrate the ability of our prototype to scan objects faster and with greater ease than conventional model acquisition pipelines.
Frequency space environment map rendering
Authors: Ramamoorthi Ravi , Hanrahan Pat
Published: October 2002

We present a new method for real-time rendering of objects with complex isotropic BRDFs under distant natural illumination, as specified by an environment map. Our approach is based on spherical frequency space analysis and includes three main contributions. Firstly, we are able to theoretically analyze required sampling rates and resolutions, which have traditionally been determined in an ad-hoc manner. We also introduce a new compact representation, which we call a
spherical harmonic reflection map (SHRM),
for efficient representation and rendering. Finally, we show how to rapidly prefilter the environment map to compute the
SHRM
---our frequency domain prefiltering algorithm is generally orders of magnitude faster than previous angular (spatial) domain approaches.
Articulated body deformation from range scan data
Authors: Allen Brett , Curless Brian , Popović Zoran
Published: October 2002

This paper presents an example-based method for calculating skeleton-driven body deformations. Our example data consists of range scans of a human body in a variety of poses. Using markers captured during range scanning, we construct a kinematic skeleton and identify the pose of each scan. We then construct a mutually consistent parameterization of all the scans using a posable subdivision surface template. The detail deformations are represented as displacements from this surface, and holes are filled smoothly within the displacement maps. Finally, we combine the range scans using
k
-nearest neighbor interpolation in pose space. We demonstrate results for a human upper body with controllable pose, kinematics, and underlying surface shape.
Synthesis of bidirectional texture functions on arbitrary surfaces
Authors: Tong Xin , Zhang Jingdan , Liu Ligang , Wang Xi , Guo Baining , Shum Heung-Yeung
Published: October 2002

The bidirectional texture function (BTF) is a 6D function that can describe textures arising from both spatially-variant surface reflectance and surface mesostructures. In this paper, we present an algorithm for synthesizing the BTF on an arbitrary surface from a sample BTF. A main challenge in surface BTF synthesis is the requirement of a consistent mesostructure on the surface, and to achieve that we must handle the large amount of data in a BTF sample. Our algorithm performs BTF synthesis based on
surface textons,
which extract essential information from the sample BTF to facilitate the synthesis. We also describe a general search strategy, called the
k-coherent search,
for fast BTF synthesis using surface textons. A BTF synthesized using our algorithm not only looks similar to the BTF sample in all viewing/lighthing conditions but also exhibits a consistent mesostructure when viewing and lighting directions change. Moreover, the synthesized BTF fits the target surface naturally and seamlessly. We demonstrate the effectiveness of our algorithm with sample BTFs from various sources, including those measured from real-world textures.
Chromium
Authors: Humphreys Greg , Houston Mike , Ng Ren , Frank Randall , Ahern Sean , Kirchner Peter D. , Klosowski James T.
Published: October 2002

We describe Chromium, a system for manipulating streams of graphics API commands on clusters of workstations. Chromium's stream filters can be arranged to create sort-first and sort-last parallel graphics architectures that, in many cases, support the same applications while using only commodity graphics accelerators. In addition, these stream filters can be extended programmatically, allowing the user to customize the stream transformations performed by nodes in a cluster. Because our stream processing mechanism is completely general, any cluster-parallel rendering algorithm can be either implemented on top of or embedded in Chromium. In this paper, we give examples of real-world applications that use Chromium to achieve good scalability on clusters of workstations, and describe other potential uses of this stream processing technology. By completely abstracting the underlying graphics architecture, network topology, and API command processing semantics, we allow a variety of applications to run in different environments.
Ray tracing on programmable graphics hardware
Authors: Purcell Timothy J. , Buck Ian , Mark William R. , Hanrahan Pat
Published: October 2002

Recently a breakthrough has occurred in graphics hardware: fixed function pipelines have been replaced with programmable vertex and fragment processors. In the near future, the graphics pipeline is likely to evolve into a general programmable stream processor capable of more than simply feed-forward triangle rendering.In this paper, we evaluate these trends in programmability of the graphics pipeline and explain how ray tracing can be mapped to graphics hardware. Using our simulator, we analyze the performance of a ray casting implementation on next generation programmable graphics hardware. In addition, we compare the performance difference between non-branching programmable hardware using a multipass implementation and an architecture that supports branching. We also show how this approach is applicable to other ray tracing algorithms such as Whitted ray tracing, path tracing, and hybrid rendering algorithms. Finally, we demonstrate that ray tracing on graphics hardware could prove to be faster than CPU based implementations as well as competitive with traditional hardware accelerated feed-forward triangle rendering.
Stylization and abstraction of photographs
Authors: DeCarlo Doug , Santella Anthony
Published: October 2002

Good information design depends on clarifying the meaningful structure in an image. We describe a computational approach to stylizing and abstracting photographs that explicitly responds to this design goal. Our system transforms images into a line-drawing style using bold edges and large regions of constant color. To do this, it represents images as a hierarchical structure of parts and boundaries computed using state-of-the-art computer vision. Our system identifies the meaningful elements of this structure using a model of human perception and a record of a user's eye movements in looking at the photo; the system renders a new image using transformations that preserve and highlight these visual elements. Our method thus represents a new alternative for non-photorealistic rendering both in its visual style, in its approach to visual form, and in its techniques for interaction.
Merging multiple conventional models in one stable model
Authors: Fayad Mohamed , Wu Shasha
Published: October 2002

Stability models may demand greater investment in analysis, but when used wisely, savings in development and maintenence costs more than make up for it.
COCA
Authors: Zhou Lidong , Schneider Fred B. , Van Renesse Robbert
Published: October 2002

COCA is a fault-tolerant and secure online certification authority that has been built and deployed both in a local area network and in the Internet. Extremely weak assumptions characterize environments in which COCA's protocols execute correctly: no assumption is made about execution speed and message delivery delays; channels are expected to exhibit only intermittent reliability; and with 3t+ 1 COCA servers up totmay be faulty or compromised. COCA is the first system to integrate a Byzantine quorum system (used to achieve availability) with proactive recovery (used to defend against mobile adversaries which attack, compromise, and control one replica for a limited period of time before moving on to another). In addition to tackling problems associated with combining fault-tolerance and security, new proactive recovery protocols had to be developed. Experimental results give a quantitative evaluation for the cost and effectiveness of the protocols.
Ordered and quantum treemaps
Authors: Bederson Benjamin B. , Shneiderman Ben , Wattenberg Martin
Published: October 2002

Treemaps, a space-filling method for visualizing large hierarchical data sets, are receiving increasing attention. Several algorithms have been previously proposed to create more useful displays by controlling the aspect ratios of the rectangles that make up a treemap. While these algorithms do improve visibility of small items in a single layout, they introduce instability over time in the display of dynamically changing data, fail to preserve order of the underlying data, and create layouts that are difficult to visually search. In addition, continuous treemap algorithms are not suitable for displaying fixed-sized objects within them, such as images.This paper introduces a new "strip" treemap algorithm which addresses these shortcomings, and analyzes other "pivot" algorithms we recently developed showing the trade-offs between them. These ordered treemap algorithms ensure that items near each other in the given order will be near each other in the treemap layout. Using experimental evidence from Monte Carlo trials and from actual stock market data, we show that, compared to other layout algorithms, ordered treemaps are more stable, while maintaining relatively favorable aspect ratios of the constituent rectangles. A user study with 20 participants clarifies the human performance benefits of the new algorithms. Finally, we present quantum treemap algorithms, which modify the layout of the continuous treemap algorithms to generate rectangles that are integral multiples of an input object size. The quantum treemap algorithm has been applied to PhotoMesa, an application that supports browsing of large numbers of images.
ECCS and LIPS: two languages for OSI systems specification and verification
Authors: Carchiolo V. , Di Stefano A. , Faro A. , Pappalardo G.
Published: October 2002

An issue of current interest in the Open Systems Interconnection (OSI) field is the choice of a language well suited to specification and verification. For this purpose, two languages based on Milner's communication calculi are proposed, respectively intended for the specification of asynchronous and synchronous OSI systems. A formal verification method, relying upon the algebraic foundations of the two languages, is introduced and illustrated by means of examples based on nontrivial protocols and services.
The PegaSys System: pictures as formal documentation of large programs
Authors: Moriconi Mark , Hare Dwight F.
Published: October 2002

PegsSys is an experimental system in which a user formally describes how a program is put together by means of a hierarchically structured collection of pictures, called
formal dependency diagrams
(FDDs). Icons in an FDD denote a wide range of data and control dependencies among the relatively coarse-grained entities contained in large programs. Dependencies considered atomic with respect to one level in a hierarchy can be decomposed into a number of dependencies at a lower level. Each dependency can be a predefined primitive of the FDD language or it can be defined by a PegaSys user in terms of the primitives.

A PegsSys user is given the illusion that logical formulas do not exist, even though PegaSys reasons about them internally. This involves (1) checking whether an FDD is meaningful syntactically, (2) determining whether hierarchical refinements of an FDD are methodologically sound, and (3) deciding whether an FDD hierarchy is logically consistent with the program that it is intended to describe. The techniques used to provide these capabilities are discussed along with the logical properties that enable PegaSys to maintain the user illusion.