7,482 papers · page 288 of 375
This paper presents a typed programming language and compiler for run-time code generation. The language, called ML', extends ML with modal operators in the style of the Mini-ML'e language of Davies and Pfenning. ML' allows programmers to use types to specify precisely the stages…
We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable…
The conditional branch has long been considered an expensive operation. The relative cost of conditional branches has increased as recently designed machines are now relying on deeper pipelines and higher multiple issue. Reducing the number of conditional branches executed can of…
This paper presents algorithms for reducing the communication overhead for parallel C programs that use dynamically-allocated data structures. The framework consists of an analysis phase called possible-placement analysis, and a transformation phase called communication selection…
Many parallel programs are written in SPMD style i.e. by running the same sequential program on all processes. SPMD programs include synchronization, but it is easy to write incorrect synchronization patterns. We propose a system that verifies a program's synchronization pattern.…
The extension of Haskell with a built-in state monad combines mathematical elegance with operational efficiency: -Semantically, at the source language level, constructs that act on the state are viewed as functions that pass an explicit store data structure around. -Operationally…
We analyze the inherent complexity of implementing Lévy's notion of optimal evaluation for the &lambda-calculus, where similar redexes are contracted in one step via so-called parallel β-reduction. optimal evaluation was finally realized by Lamping, who introduced a beautiful gra…
Edge profiles are the traditional control flow profile of choice for profile-directed compilation. They have been the basis of path-based optimizations that select paths, even though edge profiles contain strictly less information than path profiles. Recent work on path profiling…
Memory expansions are classical means to extract parallelism from imperative programs. However, for dynamic control programs with general memory accesses, such transformations either fail or require some run-time mechanism to restore the data flow. This paper presents an expansio…
We describe an escape analysis [32, 14], used to determine whether the lifetime of data exceeds its static scope.We give a new correctness proof starting directly from a semantics. Contrary to previous proofs, it takes into account all the features of functional languages, includ…
When analyzing programs for value recomputation, one faces the problem of naming the value that flows between equivalent computations with different lexical names. This paper presents a data-flow analysis framework that overcomes this problem by synthesizing a name space tailored…
It has become common to distribute software in forms that are isomorphic to the original source code. An important example is Java bytecode. Since such codes are easy to decompile, they increase the risk of malicious reverse engineering attacks.In this paper we describe the desig…
Previous algorithms for interprocedural control flow analysis of higher-order and/or object-oriented languages have been described that perform propagation or constraint satisfaction and take O(N3) time (such as Shivers's O-CFA and Heintze's set-based analysis), or unification an…
Recent years have seen increasing interest in systems that reason about and manipulate executable code. Such systems can generally benefit from information about aliasing. Unfortunately, most existing alias analyses are formulated in terms of high-level language features, and are…
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, pro…
This paper addresses the problem of how to apply pointer analysis to a wide variety of compiler applications. We are not presenting a new pointer analysis. Rather, we focus on putting two existing pointer analyses, points-to analysis and connection analysis, to work.We demonstrat…
We present a formal specification of unCurrying for a higherorder, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions which are passed as arguments or returned as values. The specification also s…
The SLam calculus is a typed λ-calculus that maintains security information as well as type information. The type system propagates security information for each object in four forms: the object's creators and readers, and the object's indirect creators and readers (i.e., those a…
The problems involved in developing efficient parallel programs have proved harder than those in developing efficient sequential ones, both for programmers and for compilers. Although program calculation has been found to be a promising way to solve these problems in the sequenti…
In standard control-flow analyses for higher-order languages, a single abstract binding for a variable represents a set of exact bindings, and a single abstract reference cell represents a set of exact reference cells. While such analyses provide useful may-alias information, the…