waashk/dblp huggingface dataset:
efficiently and precisely locating memory leaks and bloat. inefficient use of memory, including leaks and bloat, remain a significant challenge for c and c++ developers. applications with these problems become slower over time as their working set grows and can become unresponsive. at the same time, memory leaks and bloat remain notoriously difficult to debug, and comprise a large number of reported bugs in mature applications. previous tools for diagnosing memory inefficiencies-based on garbage collection, binary rewriting, or code sampling-impose high overheads (up to 100x) or generate many false alarms. this paper presents hound, a runtime system that helps track down the sources of memory leaks and bloat in c and c++ applications. hound employs data sampling, a staleness-tracking approach based on a novel heap organization, to make it both precise and efficient. hound has no false positives, and its runtime and space overhead are low enough that it can be used in deployed applications. we demonstrate hound's efficacy across a suite of synthetic benchmarks and real applications.
snugglebug: a powerful approach to weakest preconditions. symbolic analysis shows promise as a foundation for bug-finding, specification inference, verification, and test generation. this paper addresses demand-driven symbolic analysis for object-oriented programs and frameworks. many such codes comprise large, partial programs with highly dynamic behaviors--polymorphism, reflection, and so on--posing significant scalability challenges for any static analysis. we present an approach based on interprocedural backwards propagation of weakest preconditions. we present several novel techniques to improve the efficiency of such analysis. first, we present directed call graph construction, where call graph construction and symbolic analysis are interleaved. with this technique, call graph construction is guided by constraints discovered during symbolic analysis, obviating the need for exhaustively exploring a large, conservative call graph. second, we describe generalization, a technique that greatly increases the reusability of procedure summaries computed during interprocedural analysis. instead of tabulating how a procedure transforms a symbolic state in its entirety, our technique tabulates how the procedure transforms only the pertinent portion of the symbolic state. additionally, we show how integrating an inexpensive, custom logic simplifier with weakest precondition computation dramatically improves performance. we have implemented the analysis in a tool called snugglebug and evaluated it as a bug-report feasibility checker. our results show that the algorithmic techniques were critical for successfully analyzing large java applications.
taj: effective taint analysis of web applications. taint analysis, a form of information-flow analysis, establishes whether values from untrusted methods and parameters may flow into security-sensitive operations. taint analysis can detect many common vulnerabilities in web applications, and so has attracted much attention from both the research community and industry. however, most static taint-analysis tools do not address critical requirements for an industrial-strength tool. specifically, an industrial-strength tool must scale to large industrial web applications, model essential web-application code artifacts, and generate consumable reports for a wide range of attack vectors. we have designed and implemented a static taint analysis for java (taj) that meets the requirements of industry-level applications. taj can analyze applications of virtually any size, as it employs a set of techniques designed to produce useful answers given limited time and space. taj addresses a wide variety of attack vectors, with techniques to handle reflective calls, flow through containers, nested taint, and issues in generating useful reports. this paper provides a description of the algorithms comprising taj, evaluates taj against production-level benchmarks, and compares it with alternative solutions.
dynamic software updates: a vm-centric approach. software evolves to fix bugs and add features. stopping and restarting programs to apply changes is inconvenient and often costly. dynamic software updating (dsu) addresses this problem by updating programs while they execute, but existing dsu systems for managed languages do not support many updates that occur in practice and are inefficient. this paper presents the design and implementation of jvolve, a dsu-enhanced java vm. updated programs may add, delete, and replace fields and methods anywhere within the class hierarchy. jvolve implements these updates by adding to and coordinating vm classloading, just-in-time compilation, scheduling, return barriers, on-stack replacement, and garbage collection. jvolve, is safe: its use of bytecode verification and vm thread synchronization ensures that an update will always produce type-correct executions. jvolve is flexible: it can support 20 of 22 updates to three open-source programs--jetty web server, javaemailserver, and crossftp server--based on actual releases occurring over 1 to 2 years. jvolve is efficient: performance experiments show that incurs no overhead during steady-state execution. these results demonstrate that this work is a significant step towards practical support for dynamic updates in virtual machines for managed languages.
programming model for a heterogeneous x86 platform. the client computing platform is moving towards a heterogeneous architecture consisting of a combination of cores focused on scalar performance, and a set of throughput-oriented cores. the throughput oriented cores (e.g. a gpu) may be connected over both coherent and non-coherent interconnects, and have different isas. this paper describes a programming model for such heterogeneous platforms. we discuss the language constructs, runtime implementation, and the memory model for such a programming environment. we implemented this programming environment in a x86 heterogeneous platform simulator. we ported a number of workloads to our programming environment, and present the performance of our programming environment on these workloads.
typed self-representation. self-representation -- the ability to represent programs in their own language -- has important applications in reflective languages and many other domains of programming language design. although approaches to designing typed program representations for sublanguages of some base language have become quite popular recently, the question whether a fully metacircular typed self-representation is possible is still open. this paper makes a big step towards this aim by defining the fω* calculus, an extension of the higher-order polymorphic lambda calculus fω that allows typed self-representations. while the usability of these representations for metaprogramming is still limited, we believe that our approach makes a significant step towards a new generation of reflective languages that are both safe and efficient.
towards a holistic approach to auto-parallelization: integrating profile-driven parallelism detection and machine-learning based mapping. compiler-based auto-parallelization is a much studied area, yet has still not found wide-spread application. this is largely due to the poor exploitation of application parallelism, subsequently resulting in performance levels far below those which a skilled expert programmer could achieve. we have identified two weaknesses in traditional parallelizing compilers and propose a novel, integrated approach, resulting in significant performance improvements of the generated parallel code. using profile-driven parallelism detection we overcome the limitations of static analysis, enabling us to identify more application parallelism and only rely on the user for final approval. in addition, we replace the traditional target-specific and inflexible mapping heuristics with a machine-learning based prediction mechanism, resulting in better mapping decisions while providing more scope for adaptation to different target architectures. we have evaluated our parallelization strategy against the nas and spec omp benchmarks and two different multi-core platforms (dual quad-core intel xeon smp and dual-socket qs20 cell blade). we demonstrate that our approach not only yields significant improvements when compared with state-of-the-art parallelizing compilers, but comes close to and sometimes exceeds the performance of manually parallelized codes. on average, our methodology achieves 96% of the performance of the hand-tuned openmp nas and spec parallel benchmarks on the intel xeon platform and gains a significant speedup for the ibm cell platform, demonstrating the potential of profile-guided and machine-learning based parallelization for complex multi-core platforms.
type-based data structure verification. we present a refinement type-based approach for the static verification of complex data structure invariants. our approach is based on the observation that complex data structures are typically fashioned from two elements: recursion (e.g., lists and trees), and maps (e.g., arrays and hash tables). we introduce two novel type-based mechanisms targeted towards these elements: recursive refinements and polymorphic refinements. these mechanisms automate the challenging work of generalizing and instantiating rich universal invariants by piggybacking simple refinement predicates on top of types, and carefully dividing the labor of analysis between the type system and an smt solver. further, the mechanisms permit the use of the abstract interpretation framework of liquid type inference to automatically synthesize complex invariants from simple logical qualifiers, thereby almost completely automating the verification. we have implemented our approach in dsolve, which uses liquid types to verify ocaml programs. we present experiments that show that our type-based approach reduces the manual annotation required to verify complex properties like sortedness, balancedness, binary-search-ordering, and acyclicity by more than an order of magnitude.
ceal: a c-based language for self-adjusting computation. self-adjusting computation offers a language-centric approach to writing programs that can automatically respond to modifications to their data (e.g., inputs). except for several domain-specific implementations, however, all previous implementations of self-adjusting computation assume mostly functional, higher-order languages such as standard ml. prior to this work, it was not known if self-adjusting computation can be made to work with low-level, imperative languages such as c without placing undue burden on the programmer. we describe the design and implementation of ceal: a c-based language for self-adjusting computation. the language is fully general and extends c with a small number of primitives to enable writing self-adjusting programs in a style similar to conventional c programs. we present efficient compilation techniques for translating ceal programs into c that can be compiled with existing c compilers using primitives supplied by a run-time library for self-adjusting computation. we implement the proposed compiler and evaluate its effectiveness. our experiments show that ceal is effective in practice: compiled self-adjusting programs respond to small modifications to their data by orders of magnitude faster than recomputing from scratch while slowing down a from-scratch run by a moderate constant factor. compared to previous work, we measure significant space and time improvements.
binary analysis for measurement and attribution of program performance. modern programs frequently employ sophisticated modular designs. as a result, performance problems cannot be identified from costs attributed to routines in isolation; understanding code performance requires information about a routine's calling context. existing performance tools fall short in this respect. prior strategies for attributing context-sensitive performance at the source level either compromise measurement accuracy, remain too close to the binary, or require custom compilers. to understand the performance of fully optimized modular code, we developed two novel binary analysis techniques: 1) on-the-fly analysis of optimized machine code to enable minimally intrusive and accurate attribution of costs to dynamic calling contexts; and 2) post-mortem analysis of optimized machine code and its debugging sections to recover its program structure and reconstruct a mapping back to its source code. by combining the recovered static program structure with dynamic calling context information, we can accurately attribute performance metrics to calling contexts, procedures, loops, and inlined instances of procedures. we demonstrate that the fusion of this information provides unique insight into the performance of complex modular codes. this work is implemented in the hpctoolkit performance tools (http://hpctoolkit.org).
error propagation analysis for file systems. unchecked errors are especially pernicious in operating system file management code. transient or permanent hardware failures are inevitable, and error-management bugs at the file system layer can cause silent, unrecoverable data corruption. we propose an interprocedural static analysis that tracks errors as they propagate through file system code. our implementation detects overwritten, out-of-scope, and unsaved unchecked errors. analysis of four widely-used linux file system implementations (cifs, ext3, ibm jfs and reiserfs), a relatively new file system implementation (ext4), and shared virtual file system (vfs) code uncovers 312 error propagation bugs. our flow- and context-sensitive approach produces more precise results than related techniques while providing better diagnostic information, including possible execution paths that demonstrate each bug found.
proving optimizations correct using parameterized program equivalence. translation validation is a technique for checking that, after an optimization has run, the input and output of the optimization are equivalent. traditionally, translation validation has been used to prove concrete, fully specified programs equivalent. in this paper we present parameterized equivalence checking (pec), a generalization of translation validation that can prove the equivalence of parameterized programs. a parameterized program is a partially specified program that can represent multiple concrete programs. for example, a parameterized program may contain a section of code whose only known property is that it does not modify certain variables. by proving parameterized programs equivalent, pec can prove the correctness of transformation rules that represent complex optimizations once and for all, before they are ever run. we implemented our pec technique in a tool that can establish the equivalence of two parameterized programs. to highlight the power of pec, we designed a language for implementing complex optimizations using many-to-many rewrite rules, and used this language to implement a variety of optimizations including software pipelining, loop unrolling, loop unswitching, loop interchange, and loop fusion. finally, to demonstrate the effectiveness of pec, we used our pec implementation to verify that all the optimizations we implemented in our language preserve program behavior.
progress guarantee for parallel programs via bounded lock-freedom. parallel platforms are becoming ubiquitous with modern computing systems. many parallel applications attempt to avoid locks in order to achieve high responsiveness, aid scalability, and avoid deadlocks and livelocks. however, avoiding the use of system locks does not guarantee that no locks are actually used, because progress inhibitors may occur in subtle ways through various program structures. notions of progress guarantee such as lock-freedom, wait-freedom, and obstruction-freedom have been proposed in the literature to provide various levels of progress guarantees. in this paper we formalize the notions of progress guarantees using linear temporal logic (ltl). we concentrate on lock-freedom and propose a variant of it denoted bounded lock-freedom, which is more suitable for guaranteeing progress in practical systems. we use this formal definition to build a tool that checks if a concurrent program is bounded lock-free for a given bound. we then study the interaction between programs with progress guarantees and the underlying system (e.g., compilers, runtimes, operating systems, and hardware platforms). we propose a means to argue that an underlying system supports lock-freedom. a composition theorem asserts that bounded lock-free algorithms running on bounded lock-free supporting systems retain bounded lock-freedom for the composed execution.
implementation of the memory-safe full ansi-c compiler. this paper describes a completely memory-safe compiler for c language programs that is fully compatible with the ansi c specification. programs written in c often suffer from nasty errors due to dangling pointers and buffer overflow. such errors in internet server programs are often exploited by malicious attackers to crack an entire system. the origin of these errors is usually corruption of in-memory data structures caused by out-of-bound array accesses. usual c compilers do not provide any protection against such out-of-bound access, although many other languages such as java and ml do provide such protection. there have been several proposals for preventing such memory corruption from various aspects: runtime buffer overrun detectors, designs for new c-like languages, and compilers for (subsets of) the c language. however, as far as we know, none of them have achieved full memory protection and full compatibility with the c language specification at the same time. we propose the most powerful solution to this problem ever presented. we have developed fail-safe c, a memory-safe implementation of the full ansi c language. it detects and disallows all unsafe operations, yet conforms to the full ansi c standard (including casts and unions). this paper introduces several techniques--both compile-time and runtime--to reduce the overhead of runtime checks, while still maintaining 100% memory safety. this compiler lets programmers easily make their programs safe without heavy rewriting or porting of their code. it also supports many of the "dirty tricks" commonly used in many existing c programs, which do not strictly conform to the standard specification. in this paper, we demonstrate several real-world server programs that can be processed by our compiler and present technical details and benchmark results for it.
go with the flow: profiling copies to find runtime bloat. many large-scale java applications suffer from runtime bloat. they execute large volumes of methods, and create many temporary objects, all to execute relatively simple operations. there are large opportunities for performance optimizations in these applications, but most are being missed by existing optimization and tooling technology. while jit optimizations struggle for a few percent, performance experts analyze deployed applications and regularly find gains of 2x or more. finding such big gains is difficult, for both humans and compilers, because of the diffuse nature of runtime bloat. time is spread thinly across calling contexts, making it difficult to judge how to improve performance. bloat results from a pile-up of seemingly harmless decisions. each adds temporary objects and method calls, and often copies values between those temporary objects. while data copies are not the entirety of bloat, we have observed that they are excellent indicators of regions of excessive activity. by optimizing copies, one is likely to remove the objects that carry copied values, and the method calls that allocate and populate them. we introduce copy profiling, a technique that summarizes runtime activity in terms of chains of data copies. a flat copy profile counts copies by method. we show how flat profiles alone can be helpful. in many cases, diagnosing a problem requires data flow context. tracking and making sense of raw copy chains does not scale, so we introduce a summarizing abstraction called the copy graph. we implement three clients analyses that, using the copy graph, expose common patterns of bloat, such as finding hot copy chains and discovering temporary data structures. we demonstrate, with examples from a large-scale commercial application and several benchmarks, that copy profiling can be used by a programmer to quickly find opportunities for large performance gains.
verifiable composition of deterministic grammars. there is an increasing interest in extensible languages, (domain-specific) language extensions, and mechanisms for their specification and implementation. one challenge is to develop tools that allow non-expert programmers to add an eclectic set of language extensions to a host language. we describe mechanisms for composing and analyzing concrete syntax specifications of a host language and extensions to it. these specifications consist of context-free grammars with each terminal symbol mapped to a regular expression, from which a slightly-modified lr parser and context-aware scanner are generated. traditionally, conflicts are detected when a parser is generated from the composed grammar, but this comes too late since it is the non-expert programmer directing the composition of independently developed extensions with the host language. the primary contribution of this paper is a modular analysis that is performed independently by each extension designer on her extension (composed alone with the host language). if each extension passes this modular analysis, then the language composed later by the programmer will compile with no conflicts or lexical ambiguities. thus, extension writers can verify that their extension will safely compose with others and, if not, fix the specification so that it will. this is possible due to the context-aware scanner's lexical disambiguation and a set of reasonable restrictions limiting the constructs that can be introduced by an extension. the restrictions ensure that the parse table states can be partitioned so that each state can be attributed to the host language or a single extension.
safe and timely updates to multi-threaded programs. many dynamic updating systems have been developed that enable a program to be patched while it runs, to fix bugs or add new features. this paper explores techniques for supporting dynamic updates to multi-threaded programs, focusing on the problem of applying an update in a timely fashion while still producing correct behavior. past work has shown that this tension of safety versus timeliness can be balanced for single-threaded programs. for multi-threaded programs, the task is more difficult because myriad thread interactions complicate understanding the possible program states to which a patch could be applied. our approach allows the programmer to specify a few program points (e.g., one per thread) at which a patch may be applied, which simplifies reasoning about safety. to improve timeliness, a combination of static analysis and run-time support automatically expands these few points to many more that produce behavior equivalent to the originals. experiments with thirteen realistic updates to three multi-threaded servers show that we can safely perform a dynamic update within milliseconds when more straightforward alternatives would delay some updates indefinitely.