waashk/dblp huggingface dataset:
artemis: practical runtime monitoring of applications for execution anomalies. a number of hardware and software techniques have been proposed to detect dynamic program behaviors that may indicate a bug in a program. because these techniques suffer from high overheads they are useful in finding bugs in programs before they are released, but are significantly less useful in finding bugs in long-running programs on production systems -- the same bugs that are the most difficult to find using traditional techniques. in this paper we propose the artemis1 is the greek goddess of the hunt and wild animals. our framework guides the hunt for wild bugs. compiler-based instrumentation framework that complements many pre-existing runtime monitoring techniques. the artemis framework guides baseline monitoring techniques toward regions of the program where bugs are likely to occur, yielding a low asymptotic monitoring overhead. artemis also facilitates system-load aware runtime monitoring that allows the monitoring coverage to be dynamically scaled up to take advantage of extra cycles when the system load is low, and dynamically scaled down to monitor only the most suspicious regions when the system load is high. our experiments show that artemis' asymptotic overhead can outperform the performance floor overhead of random sampling for many tools, and that artemis can effectively guide a monitoring tool to the buggy regions of a program. our experimental results show that artemis applied to a hardware-based pc-invariance monitoring scheme and a value-based invariance detection and checking scheme significantly improves their runtime monitoring overhead (by up to 4.6 times) with moderate impact on their bug-detecting capabilities.
modular verification of assembly code with stack-based control abstractions. runtime stacks are critical components of any modern software--they are used to implement powerful control structures such as function call/return, stack cutting and unwinding, coroutines, and thread context switch. stack operations, however, are very hard to reason about: there are no known formal specifications for certifying c-style setjmp/longjmp, stack cutting and unwinding, or weak continuations (in c--). in many proof-carrying code (pcc) systems, return code pointers and exception handlers are treated as general first-class functions (as in continuation-passing style) even though both should have more limited scopes.in this paper we show that stack-based control abstractions follow a much simpler pattern than general first-class code pointers. we present a simple but flexible hoare-style framework for modular verification of assembly code with all kinds of stackbased control abstractions, including function call/return, tail call, setjmp/longjmp, weak continuation, stack cutting, stack unwinding, multi-return function call, coroutines, and thread context switch. instead of presenting a specific logic for each control structure, we develop all reasoning systems as instances of a generic framework. this allows program modules and their proofs developed in different pcc systems to be linked together. our system is fully mechanized. we give the complete soundness proof and a full verification of several examples in the coq proof assistant.
simple and effective link-time optimization of modula-3 programs. modula-3 supports development of modular programs by separating an object's interface from its implementation. this separation induces a runtime overhead in the implementation of objects, because it prevents the compiler from having complete information about a program's type hierarchy. this overhead can be reduced at link time, when the entire type hierarchy becomes available. we describe opportunities for link-time optimization of modula-3, present two link-time optimizations that reduce the runtime costs of modula-3's opaque types and methods, and show how link-time optimization could provide c++ which the benefits of opaques types at no additional runtime cost.our optimization techniques are implemented in mld, a retargetable linker for the mips, sparc, and intel 486, mld links a machine-independent intermediate code that is suitable for link-time optimization and code generation. linking intermediate code simplifies implementation of the optimizations and makes it possible to evaluate them on a wide range of architectures. mld's optimizations are effective: they reduce the total number of instructions executed by up to 14% and convert as many as 79% of indirect calls to direct calls.
pads: a domain-specific language for processing ad hoc data. pads is a declarative data description language that allows data analysts to describe both the physical layout of ad hoc data sources and semantic properties of that data. from such descriptions, the pads compiler generates libraries and tools for manipulating the data, including parsing routines, statistical profiling tools, translation programs to produce well-behaved formats such as xml or those required for loading relational databases, and tools for running xqueries over raw pads data sources. the descriptions are concise enough to serve as "living" documentation while flexible enough to describe most of the ascii, binary, and cobol formats that we have seen in practice. the generated parsing library provides for robust, application-specific error handling.
parallelizing complex scans and reductions. we present a method for automatically extracting parallel prefix programs from sequential loops, even in the presence of complicated conditional statements. rather than searching for associative operators in the loop body directly, the method rests on the observation that functional composition itself is associative. accordingly, we model the loop body as a multivalued function of multiple parameters, and look for a closed-form representation of arbitrary compositions of loop body instances. careful analysis of conditionals allows this search to succeed in cases where existing automatic methods fail. the method has been implemented and used to generate code for the iwarp parallel computer.
the design of a class mechanism for moby. typical class-based languages, such as c++ and java, provide complex class mechanisms but only weak module systems. in fact, classes in these languages incorporate many of the features found in richer module mechanisms. in this paper, we describe an alternative approach to designing a language that has both classes and modules. in our design, we rely on a rich ml-style module system to provide features such as visibility control and parameterization, while providing a minimal class mechanism that includes only those features needed to support inheritance. programmers can then use the combination of modules and classes to implement the full range of class-based features and idioms. our approach has the advantage that it provides a full-featured module system (useful in its own right), while keeping the class mechanism quite simple.we have incorporated this design in moby, which is an ml-style language that supports class-based object-oriented programming. in this paper, we describe our design via a series of simple examples, show how various class-based features and idioms are realized in moby, compare our design with others, and sketch its formal semantics.
type-based race detection for java. this paper presents a static race detection analysis for multithreaded java programs. our analysis is based on a formal type system that is capable of capturing many common synchronization patterns. these patterns include classes with internal synchronization, classes thatrequire client-side synchronization, and thread-local classes. experience checking over 40,000 lines of java code with the type system demonstrates that it is an effective approach for eliminating races conditions. on large examples, fewer than 20 additional type annotations per 1000 lines of code were required by the type checker, and we found a number of races in the standard java libraries and other test programs.
componential set-based analysis. set based analysis is a constraint-based whole program analysis that is applicable to functional and object-oriented programming language. unfortunately, the analysis is useless for large programs, since it generates descriptions of data flow relationships that grow quadratically in the size of the program.this paper presents componential set-based analysis, which is faster and handles larger programs without any loss of accuracy over set-based analysis. the design of the analysis exploits a number of theoretical results concerning constraint systems, including a completeness result and a decision algorithm concerning the observable equivalance of constraint systems. experimental results validate the practically of the analysis.
extended static checking for java. software development and maintenance are costly endeavors. the cost can be reduced if more software defects are detected earlier in the development cycle. this paper introduces the extended static checker for java (esc/java), an experimental compile-time program checker that finds common programming errors. the checker is powered by verification-condition generation and automatic theorem-proving techniques. it provides programmers with a simple annotation language with which programmer design decisions can be expressed formally. esc/java examines the annotated software and warns of inconsistencies between the design decisions recorded in the annotations and the actual code, and also warns of potential runtime errors in the code. this paper gives an overview of the checker architecture and annotation language and describes our experience applying the checker to tens of thousands of lines of java programs.
a type and effect system for atomicity. ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions between threads. previous work addressed this problem by devising tools for detecting race conditions, a situation where two threads simultaneously access the same data variable, and at least one of the accesses is a write. however, verifying the absence of such simultaneous-access race conditions is neither necessary nor sufficient to ensure the absence of errors due to unexpected thread interactions.we propose that a stronger non-interference property is required, namely atomicity. atomic methods can be assumed to execute serially, without interleaved steps of other threads. thus, atomic methods are amenable to sequential reasoning techniques, which significantly simplifies both formal and informal reasoning about program correctness.this paper presents a type system for specifying and verifying the atomicity of methods in multithreaded java programs. the atomic type system is a synthesis of lipton's theory of reduction and type systems for race detection.we have implemented this atomic type system for java and used it to check a variety of standard java library classes. the type checker uncovered subtle atomicity violations in classes such as <tt>java.lang.string</tt> and <tt>java.lang.string-buffer</tt> that cause crashes under certain thread interleavings.this paper proposes that a stronger non-interference property is required, namely atomicity, and presents a type system for verifying the atomicity of methods in multithreaded java programs. methods in a class can be annotated with the keyword <tt>atomic</tt>. clients of a well-typed class can then assume that each atomic method is executed in one step, thus significantly simplifying both formal and informal reasoning about the client's correctness.
the essence of compiling with continuations. in order to simplify the compilation process, many compilers for higher-order languages use the continuation-passing style (cps) transformation in a first phase to generate an intermediate representation of the source program. the salient aspect of this intermediate form is that all procedures take an argument that represents the rest of the computation (the "continuation"). since the na&iuml;ve cps transformation considerably increases the size of programs, cps compilers perform reductions to produce a more compact intermediate representation. although often implemented as a part of the cps transformation, this step is conceptually a second phase. finally, code generators for typical cps compilers treat continuations specially in order to optimize the interpretation of continuation parameters.a thorough analysis of the abstract machine for cps terms shows that the actions of the code generator invert the na&iuml;ve cps translation step. put differently, the combined effect of the three phases is equivalent to a source-to-source transformation that simulates the compaction phase. thus, fully developed cps compilers do not need to employ the cps transformation but can achieve the same results with a simple source-level transformation.
kill-safe synchronization abstractions. when an individual task can be forcefully terminated at any time, cooperating tasks must communicate carefully. for example, if two tasks share an object, and if one task is terminated while it manipulates the object, the object may remain in an inconsistent or frozen state that incapacitates the other task. to support communication among terminable tasks, language run-time systems (and operating systems) provide kill-safe abstractions for inter-task communication. no kill-safe guarantee is available, however, for abstractions that are implemented outside the run-time system.in this paper, we show how a run-time system can support new kill-safe abstractions without requiring modification to the run-time system, and without requiring the run-time system to trust any new code. our design frees the run-time implementor to provide only a modest set of synchronization primitives in the trusted computing base, while still allowing tasks to communicate using sophisticated abstractions.
units: cool modules for hot languages. a module system ought to enable assembly-line programming using separate compilation and an expressive linking language. separate compilation allows programmers to develop parts of a program independently. a linking language gives programmers precise control over the assembly of parts into a whole. this paper presents models of program units, mzscheme's module language for assembly-line programming. units support separate compilation, independent module reuse, cyclic dependencies, hierarchical structuring, and dynamic linking. the models explain how to integrate units with untyped and typed languages such as scheme and ml.
a theory of type qualifiers. we describe a framework for adding type qualifiers to a language. type qualifiers encode a simple but highly useful form of subtyping. our framework extends standard type rules to model the flow of qualifiers through a program, where each qualifier or set of qualifiers comes with additional rules that capture its semantics. our framework allows types to be polymorphic in the type qualifiers. we present a const-inference system for c as an example application of the framework. we show that for a set of real c programs, many more consts can be used than are actually present in the original code.
flow-sensitive type qualifiers. we present a system for extending standard type systems with flow-sensitive type qualifiers. users annotate their programs with type qualifiers, and inference checks that the annotations are correct. in our system only the type qualifiers are modeled flow-sensitively---the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. we demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the linux kernel.
formal loop merging for signal transforms. a critical optimization in the domain of linear signal transforms, such as the discrete fourier transform (dft), is loop merging, which increases data locality and reuse and thus performance. in particular, this includes the conversion of shuffle operations into array reindexings. to date, loop merging is well understood only for the dft, and only for cooley-tukey fft based algorithms, which excludes dft sizes divisible by large primes. in this paper, we present a formal loop merging framework for general signal transforms and its implementation within the spiral code generator. the framework consists of ε-spl, a mathematical language to express loops and index mappings; a rewriting system to merge loops in ε-spl and a compiler that translates ε-spl into code. we apply the framework to dft sizes that cannot be handled using only the cooley-tukey fft and compare our method to fftw 3.0.1 and the vendor library intel mkl 7.2.1. compared to fftw our generated code is a factor of 2--4 faster under equal implementation conditions (same algorithms, same unrolling threshold). for some sizes we show a speed-up of a factor of 9 using bluestein's algorithm. further, we give a detailed comparison against the intel vendor library mkl; our generated code is between 2 times faster and 4.5 times slower.
automatic inference of models for statistical code compression. this paper describes experiments that apply machine learning to compress computer programs, formalizing and automating decisions about instruction encoding that have traditionally been made by humans in a more ad hoc manner. a program accepts a large training set of program material in a conventional compiler intermediate representation (ir) and automatically infers a decision tree that separates ir code into streams that compress much better than the undifferentiated whole. driving a conventional arithmetic compressor with this model yields code 30% smaller than the previous record for ir code compression, and 24% smaller than an ambitious optimizing compiler feeding an ambitious general-purpose data compressor.
finite-static code generation. this paper describes gburg, which generates tiny, fast code generators based on finite-state machine pattern matching. the code generators translate postfix intermediate code into machine instructions in one pass (except, of course, for backpatching addresses). a stack-based virtual machine---known as the lean virtual machine (lvm)---tuned for fast code generation is also described. gburg translates the two-page lvm-to-x86 specification into a code generator that fits entirely in an 8 kb i-cache and that emits x86 code at 3.6 mb/set on a 266-mhz p6. our just-in-time code generator translates and executes small benchmarks at speeds within a factor of two of executables derived from the conventional compile-time code generator on which it is based.
a fast fourier transform compiler. the fftw library for computing the discrete fourier transform (dft) has gained a wide acceptance in both academia and industry, because it provides excellent performance on a variety of machines (even competitive with or faster than equivalent libraries supplied by vendors). in fftw, most of the performance-critical code was generated automatically by a special-purpose compiler, called genfft, that outputs c code. written in objective caml, genfft can produce dft programs for any input length, and it can specialize the dft program for the common case where the input data are real instead of complex. unexpectedly, genfft "discovered" algorithms that were previously unknown, and it was able to reduce the arithmetic complexity of some other existing algorithms. this paper describes the internals of this special-purpose compiler in some detail, and it argues that a specialized compiler is a valuable tool.
the implementation of the cilk-5 multithreaded language. the fifth release of the multithreaded language cilk uses a provably good "work-stealing" scheduling algorithm similar to the first system, but the language has been completely redesigned and the runtime system completely reengineered. the efficiency of the new implementation was aided by a clear strategy that arose from a theoretical analysis of the scheduling algorithm: concentrate on minimizing overheads that contribute to the work, even at the expense of overheads that contribute to the critical path. although it may seem counterintuitive to move overheads onto the critical path, this "work-first" principle has led to a portable cilk-5 implementation in which the typical cost of spawning a parallel thread is only between 2 and 6 times the cost of a c function call on a variety of contemporary machines. many cilk programs run on one processor with virtually no degradation compared to equivalent c programs. this paper describes how the work-first principle was exploited in the design of cilk-5's compiler and its runtime system. in particular, we present cilk-5's novel "two-clone" compilation strategy and its dijkstra-like mutual-exclusion protocol for implementing the ready deque in the work-stealing scheduler.
checking type safety of foreign function calls. foreign function interfaces (ffis) allow components in different languages to communicate directly with each other. while ffis are useful, they often require writing tricky low-level code and include little or no static safety checking, thus providing a rich source of hard-to-find programming errors. in this article, we study the problem of enforcing type safety across the ocaml-to-c ffi and the java native interface (jni). we present o-saffire and j-saffire, a pair of multilingual type inference systems that ensure c code that uses these ffis accesses high-level data safely. our inference systems use representational types to model c's low-level view of ocaml and java values, and singleton types to track integers, strings, memory offsets, and type tags through c. j-saffire, our java system, uses a polymorphic flow-insensitive, unification-based analysis. polymorphism is important because it allows us to precisely model user-defined wrapper functions and the more than 200 jni functions. o-saffire, our ocaml system, uses a monomorphic flow-sensitive analysis because, while polymorphism is much less important for the ocaml ffi flow-sensitivity is critical to track conditional branches, which are used when pattern matching ocaml data in c. o-saffire also tracks garbage collection information to ensure that local c pointers to the ocaml heap are registered properly, which is not necessary for the jni. we have applied o-saffire and j-saffire to a set of benchmarks and found many bugs and questionable coding practices. these results suggest that static checking of ffis can be a valuable tool in writing correct multilingual software.
a timed petri-net model for fine-grain loop scheduling. efficient execution of loops is one of the most important obstacles facing high-performance computer architectures. loop scheduling involves handling a partially ordered set of operations which are to be performed repetitively over a number of iterations.in this paper we study loop scheduling using petri nets, due to their unique power for modeling both partial orders and cycles. the behavior of loops can be modeled by constructing, at compile time, a petri-net behavior graph which exhibits a repetitive firing sequence known as a cyclic frustum. from a cyclic frustum, a time-optimal schedule for the corresponding loop can be derived. a polynomial time bound for such a cyclic frustum to occur has been established. simulation results on a number of livermore loops, both with and without loop-carried dependences, have demonstrated the feasibility of determining the cyclic frustum at compile time.