waashk/dblp huggingface dataset:
how to read floating-point numbers accurately. converting decimal scientific notation into binary floating point is nontrivial, but this conversion can be performed with the best possible accuracy without sacrificing efficiency.consider the problem of converting decimal scientific notation for a number into the best binary floating point approximation to that number, for some fixed precision. this problem cannot be solved using arithmetic of any fixed precision. hence the ieee standard for binary floating-point arithmetic does not require the result of such a conversion to be the best approximation.this paper presents an efficient algorithm that always finds the best approximation. the algorithm uses a few extra bits of precision to compute an ieee-conforming approximation while testing an intermediate result to determine whether the approximation could be other than the best. if the approximation might not be the best, then the best approximation is determined by a few simple operations on multiple-precision integers, where the precision is determined by the input. when using 64 bits of precision to compute ieee double precision results, the algorithm avoids higher-precision arithmetic over 99% of the time.the input problem considered by this paper is the inverse of an output problem considered by steele and white: given a binary floating point number, print a correctly rounded decimal representation of it using the smallest number of digits that will allow the number to be read without loss of accuracy. the steele and white algorithm assumes that the input problem is solved; an imperfect solution to the input problem, as allowed by the ieee standard and ubiquitous in current practice, defeats the purpose of their algorithm.
proper tail recursion and space efficiency. the ieee/ansi standard for scheme requires implementations to be properly tail recursive. this ensures that portable code can rely upon the space efficiency of continuation-passing style and other idioms. on its face, proper tail recursion concerns the efficiency of procedure calls that occur within a tail context. when examined closely, proper tail recursion also depends upon the fact that garbage collection can be asymptotically more space-efficient than algol-like stack allocation.proper tail recursion is not the same as ad hoc tail call optimization in stack-based languages. proper tail recursion often precludes stack allocation of variables, but yields a well-defined asymptotic space complexity that can be relied upon by portable programs.this paper offers a formal and implementation-independent definition of proper tail recursion for scheme. it also shows how an entire family of reference implementations can be used to characterize related safe-for-space properties, and proves the asymptotic inequalities that hold between them.
generational garbage collection and the radioactive decay model. if a fixed exponentially decreasing probability distribution function is used to model every object's lifetime, then the age of an object gives no information about its future life expectancy. this radioactive decay model implies there can be no rational basis for deciding which live objects should be promoted to another generation. yet there remains a rational basis for deciding how many objects to promote, when to collect garbage, and which generations to collect.analysis of the model leads to a new kind of generational garbage collector whose effectiveness does not depend upon heuristics that predict which objects will live longer than others.this result provides insight into the computational advantages of generational garbage collection, with implications for the management of objects whose life expectancies are difficult to predict.
space-time trade-off optimization for a class of electronic structure calculations. the accurate modeling of the electronic structure of atoms and molecules is very computationally intensive. many models of electronic structure, such as the coupled cluster approach, involve collections of tensor contractions. there are usually a large number of alternative ways of implementing the tensor contractions, representing different trade-offs between the space required for temporary intermediates and the total number of arithmetic operations. in this paper, we present an algorithm that starts with an operation-minimal form of the computation and systematically explores the possible space-time trade-offs to identify the form with lowest cost that fits within a specified memory limit. its utility is demonstrated by applying it to a computation representative of a component in the ccsd(t) formulation in the nwchem quantum chemistry suite from pacific northwest national laboratory.
automatically closing open reactive programs. we study in this paper the problem of analyzing implementations of open systems --- systems in which only some of the components are present. we present an algorithm for automatically closing an open concurrent reactive system with its most general environment, i.e., the environment that can provide any input at any time to the system. the result is a nondeterministic closed (i.e., self-executable) system which can exhibit all the possible reactive behaviors of the original open system. these behaviors can then be analyzed using verisoft, an existing tool for systematically exploring the state spaces of closed systems composed of multiple (possibly nondeterministic) processes executing arbitrary code. we have implemented the techniques introduced in this paper in a prototype tool for automatically closing open programs written in the c programming language. we discuss preliminary experimental results obtained with a large telephone-switching software application developed at lucent technologies.
a certifying compiler for java. this paper presents the initial results of a project to determine if the techniques of proof-carrying code and certifying compilers can be applied to programming languages of realistic size and complexity. the experiment shows that: (1) it is possible to implement a certifying native-code compiler for a large subset of the java programming language; (2) the compiler is freely able to apply many standard local and global optimizations; and (3) the pcc binaries it produces are of reasonable size and can be rapidly checked for type safety by a small proof-checker. this paper also presents further evidence that pcc provides several advantages for compiler development. in particular, generating proofs of the target code helps to identify compiler bugs, many of which would have been difficult to discover by testing.
tile size selection using cache organization and data layout. when dense matrix computations are too large to fit in cache, previous research proposes tiling to reduce or eliminate capacity misses. this paper presents a new algorithm for choosing problem-size dependent tile sizes based on the cache size and cache line size for a direct-mapped cache. the algorithm eliminates both capacity and self-interference misses and reduces cross-interference misses. we measured simulated miss rates and execution times for our algorithm and two others on a variety of problem sizes and cache organizations. at higher set associativity, our algorithm does not always achieve the best performance. however on direct-mapped caches, our algorithm improves simulated miss rates and measured execution times when compared with previous work.
reverse interpretation + mutation analysis = automatic retargeting. there are three popular methods for constructing highly retargetable compilers: (1) the compiler emits abstract machine code which is interpreted at run-time, (2) the compiler emits c code which is subsequently compiled to machine code by the native c compiler, or (3) the compiler's code-generator is generated by a back-end generator from a formal machine description produced by the compiler writer.these methods incur high costs at run-time, compile-time, or compiler-construction time, respectively.in this paper we will describe a novel method which promises to significantly reduce the effort required to retarget a compiler to a new architecture, while at the same time producing fast and effective compilers. the basic idea is to use the native c compiler at compiler construction time to discover architectural features of the new architecture. from this information a formal machine description is produced. given this machine description, a native code-generator can be generated by a back-end generator such as beg or burg.a prototype automatic architecture discovery unit has been implemented. the current version is general enough to produce machine descriptions for the integer instruction sets of common risc and cisc architectures such as the sun sparc, digital alpha, mips, dec vax, and intel x86. the tool is completely automatic and requires minimal input from the user: principally, the user needs to provide the internet address of the target machine and the command-lines by which the c compiler, assembler, and linker are invoked.
dynamic path-based software watermarking. software watermarking is a tool used to combat software piracy by embedding identifying information into a program. most existing proposals for software watermarking have the shortcoming that the mark can be destroyed via fairly straightforward semantics-preserving code transformations. this paper introduces path-based watermarking, a new approach to software watermarking based on the dynamic branching behavior of programs. the advantage of this technique is that error-correcting and tamper-proofing techniques can be used to make path-based watermarks resilient against a wide variety of attacks. experimental results, using both java bytecode and ia-32 native code, indicate that even relatively large watermarks can be embedded into programs at modest cost.
ccured in the real world. ccured is a program transformation system that adds memory safety guarantees to c programs by verifying statically that memory errors cannot occur and by inserting run-time checks where static verification is insufficient.this paper addresses major usability issues in a previous version of ccured, in which many type casts required the use of pointers whose representation was expensive and incompatible with precompiled libraries. we have extended the ccured type inference algorithm to recognize and verify statically a large number of type casts; this goal is achieved by using physical subtyping and pointers with run-time type information to allow parametric and subtype polymorphism. in addition, we present a new instrumentation scheme that splits ccured's metadata into a separate data structure whose shape mirrors that of the original user data. this scheme allows instrumented programs to invoke external functions directly on the program's data without the use of a wrapper function.with these extensions we were able to use ccured on real-world security-critical network daemons and to produce instrumented versions without memory-safety vulnerabilities.
termination proofs for systems code. program termination is central to the process of ensuring that systems code can always react. we describe a new program termination prover that performs a path-sensitive and context-sensitive program analysis and provides capacity for large program fragments (i.e. more than 20,000 lines of code) together with support for programming language features such as arbitrarily nested loops, pointers, function-pointers, side-effects, etc.we also present experimental results on device driver dispatch routines from thewindows operating system. the most distinguishing aspect of our tool is how it shifts the balance between the two tasks of constructing and respectively checking the termination argument. checking becomes the hard step. in this paper we show how we solve the corresponding challenge of checking with binary reachability analysis.
interprocedural side-effect analysis in linear time. we present a new method for solving banning's alias-free flow-insensitive side-effect analysis problem. the algorithm employs a new data structure, called the binding multi-graph, along with depth-first search to achieve a running time that is linear in the size of the call multi-graph of the program. this method can be extended to produce fast algorithms for data-flow problems with more complex lattice structures.
enhanced code compression for embedded risc processors. this paper explores compiler techniques for reducing the memory needed to load and run program executables. in embedded systems, where economic incentives to reduce both ram and rom are strong, the size of compiled code is increasingly important. similarly, in mobile and network computing, the need to transmit an executable before running it places a premium on code size. our work focuses on reducing the size of a program's code segment, using pattern-matching techniques to identify and coalesce together repeated instruction sequences. in contrast to other methods, our framework preserves the ability to run program executables directly, without an intervening decompression stage. our compression framework is integrated into an industrial-strength optimizing compiler, which allows us to explore the interaction between code compression and classical code optimization techniques, and requires that we contend with the difficulties of compressing previously optimized code. the specific contributions in this paper include a comprehensive experimental evaluation of code compression for a risc-like architecture, a more powerful pattern-matching scheme for improved identification of repeated code fragments, and a new form of profile-driven code compression that reduces the speed penalty arising from compression.
design of an interpretive environment for turing. this paper presents the design of an interpreter structure for modern programming languages such as turing and modula ii that is modular and highly orthogonal while providing maximal flexibility and efficiency in implementation. at the outermost level, the structure consists of a front end, responsible for interaction with the user, and a back end, responsible for execution. the two are linked by a single database consisting of the tokenized statements of the user program. interfaces between the major modules of each part are defined in such a way as to maximize reusability, and each interface can service a range of plug-compatible modules implementing radically different semantics. the design accommodates a wide spectrum of interpreter types ranging from batch-oriented compiler-simulators to statement-by-statement interactive execution, and provides for a range of program editing tools from simple line editors through to modern language-directed programming environments. it has served as the basis for several interpretive systems including the production turing interpreter, the turing programming environment, and the turing tool software maintenance tool.
an lr substring parser for noncorrecting syntax error recovery. for a context-free grammar g, a construction is given to produce an lr parser that recognizes any substring of the language generated by g. the construction yields a conflict-free (deterministic) parser for the bounded context class of grammars (floyd, 1964). the same construction yields either a left-to-right or right-to-left substring parser, as required to implement non-correcting syntax error recovery as proposed by richter (1985). experience in constructing a substring parser for pascal is described.
type-dependent parameter inference. an algorithm is presented to infer the type and operation parameters of polymorphic functions. operation parameters are named and typed at the function definition, but are selected from the set of overloaded definitions available wherever the function is used. these parameters are always implicit, implying that the complexity of using a function does not increase with the generality of its type.
doc: a practical approach to source-level debugging of globally optimized code. as optimizing compilers become more sophisticated, the problem of debugging the source code of an application becomes more difficult. in order to investigate this problem, we implemented doc, a prototype solution for debugging optimized code. doc is a modification of the existing c compiler and source-level symbolic debugger for the hp9000 series 800. this paper describes our experiences in this effort. we show in an actual implementation that source-level debugging of globally optimized code is viable.
what is a recursive module? a hierarchical module system is an effective tool for structuring large programs. strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. this can impede modular programming by forcing mutually-dependent components to be consolidated into a single module. recently there have been several proposals for module systems that admit cyclic dependencies, but it is not clear how these proposals relate to one another, nor how one might integrate them into an expressive module system such as that of ml.to address this question we provide a type-theoretic analysis of the notion of a recursive module in the context of a "phase-distinction" formalism for higher-order module systems. we extend this calculus with a recursive module mechanism and a new form of signature, called a recursively dependent signature, to support the definition of recursive modules. these extensions are justified by an interpretation in terms of more primitive language constructs. this interpretation may also serve as a guide for implementation.
efficient accomodation of may-alias information in ssa form. we present an algorithm for incrementally including may-alias information into static single assignment form by computing a sequence of increasingly precise (and correspondingly larger) partial ssa forms. our experiments show significant speedup of our method over exhaustive use of may-alias information, as optimization problems converge well before most may-aliases are needed.
automatically partitioning packet processing applications for pipelined architectures. modern network processors employs parallel processing engines (pes) to keep up with explosive internet packet processing demands. most network processors further allow processing engines to be organized in a pipelined fashion to enable higher processing throughput and flexibility. in this paper, we present a novel program transformation technique to exploit parallel and pipelined computing power of modern network processors. our proposed method automatically partitions a sequential packet processing application into coordinated pipelined parallel subtasks which can be naturally mapped to contemporary high-performance network processors. our transformation technique ensures that packet processing tasks are balanced among pipeline stages and that data transmission between pipeline stages is minimized. we have implemented the proposed transformation method in an auto-partitioning c compiler product for intel network processors. experimental results show that our method provides impressive speed up for the commonly used npf ipv4 forwarding and ip forwarding benchmarks. for a 9-stage pipeline, our auto-partitioning c compiler obtained more than 4x speedup for the ipv4 forwarding pps and the ip forwarding pps (for both the ipv4 traffic and ipv6 traffic).
memory allocation and higher-order functions. this paper presents a constant-time marking-collecting algorithm to efficiently implement recursion with a general heap memory rather than with a vectorial stack, in a context of frequent captures of continuations. it has been seen to reduce the 80% garbage collection overhead to less than 5% on average.the algorithm has been built into a virtual machine to efficiently implement at the assembly level the actor language plasma, an actor-oriented version of prolog and a variant of scheme, currently in use on 8086, 68000 and vax.the rationale to use the heap memory is that continuations are available via a single pointer in a unified memory and can be shared optimally when recurrently captured, which is simply impossible using a strategy based on stack recopy. further, non-captured continuations can be incrementally garbage collected on the fly.part i describes the elementary recursive instructions of the virtual machine. part ii presents and proves the marking-collecting strategy. part iii safely generalizes the transformation "call + return = branch" in a way compatible with the possible capture of the current continuation. an appendix relates its integration in the virtual scheme machine supporting scheme 84.
esp: path-sensitive program verification in polynomial time. in this paper, we present a new algorithm for partial program verification that runs in polynomial time and space. we are interested in checking that a program satisfies a given temporal safety property. our insight is that by accurately modeling only those branches in a program for which the property-related behavior differs along the arms of the branch, we can design an algorithm that is accurate enough to verify the program with respect to the given property, without paying the potentially exponential cost of full path-sensitive analysis.we have implemented this "property simulation" algorithm as part of a partial verification tool called esp. we present the results of applying esp to the problem of verifying the file i/o behavior of a version of the gnu c compiler (gcc, 140,000 loc). we are able to prove that all of the 646 calls to .fprintf in the source code of gcc are guaranteed to print to valid, open files. our results show that property simulation scales to large programs and is accurate enough to verify meaningful properties.
cint: a risc interpreter for the c programming language. cint is an interpretation system for the c programming language. like most interpretation systems, it provides "load and go" type execution as well as enhanced debugging and performance analysis tools. cint consists of two phases--a translator and an interpreter. the translator compiles the source program into code for a virtual machine. the interpreter then loads and executes this code. while providing services similar to traditional interpreters, cint differs from them in two important ways. first, the virtual machine languages used by many interpreters are quite large; machines with 100 to 200 operations are common. in contrast, cint's virtual machine has only 63 operations. second, to achieve acceptable execution speeds, interpreters are often implemented in the assembly language of the host machine. cint, however, is written entirely in c and is therefore portable. in fact, it has been transported to four machines without modification. despite the compact size of the virtual machine language and the high-level language implementation, cint's execution speed is comparable to that of other interpreters. this paper describes the design of the virtual machine, the implementation of the interpreter, and the performance of the system.