7,482 papers · page 203 of 375
Taming wildcards in Java's type system
Wildcards have become an important part of Java's type system since their introduction 7 years ago. Yet there are still many open problems with Java's wildcards. For example, there are no known sound and complete algorithms for subtyping (and consequently type checking) Java wild…
Languages as libraries
Programming language design benefits from constructs for extending the syntax and semantics of a host language. While C's string-based macros empower programmers to introduce notational shorthands, the parser-level macros of Lisp encourage experimentation with domain-specific lan…
Evaluating value-graph translation validation for LLVM
Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the value-graphs of an original function and its transformed counterpart. In this paper, we present the …
ALTER: exploiting breakable dependences for parallelization
For decades, compilers have relied on dependence analysis to determine the legality of their transformations. While this conservative approach has enabled many robust optimizations, when it comes to parallelization there are many opportunities that can only be exploited by changi…
LeakChaser: helping programmers narrow down causes of memory leaks
In large programs written in managed languages such as Java and C#, holding unnecessary references often results in memory leaks and bloat, degrading significantly their run-time performance and scalability. Despite the existence of many leak detectors for such languages, these d…
Finding and understanding bugs in C compilers
Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every …
Cruiser: concurrent heap buffer overflow monitoring using lock-free data structures
An SSA-based algorithm for optimal speculative code motion under an execution profile
To derive maximum optimization benefits from partial redundancy elimination (PRE),it is necessary to go beyond its safety constraint. Algorithms for optimal speculative code motion have been developed based on the application of minimum cut to flow networks formed out of the cont…
Composable asynchronous events
Although asynchronous communication is an important feature of many concurrent systems, building composable abstractions that leverage asynchrony is challenging. This is because an asynchronous operation necessarily involves two distinct threads of control -- the thread that init…
Blame for all
Several programming languages are beginning to integrate static and dynamic typing, including Racket (formerly PLT Scheme), Perl 6, and C# 4.0 and the research languages Sage (Gronski, Knowles, Tomb, Freund, and Flanagan, 2006) and Thorn (Wrigstad, Eugster, Field, Nystrom, and Vi…
Streaming transducers for algorithmic verification of single-pass list-processing programs
We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data domain t…
Dynamic inference of static types for ruby
There have been several efforts to bring static type inference to object-oriented dynamic languages such as Ruby, Python, and Perl. In our experience, however, such type inference systems are extremely difficult to develop, because dynamic languages are typically complex, poorly …
Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated
Building correct and efficient concurrent algorithms is known to be a difficult problem of fundamental importance. To achieve efficiency, designers try to remove unnecessary and costly synchronization. However, not only is this manual trial-and-error process ad-hoc, time consumin…
Mathematizing C++ concurrency
Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong gua…
Space overhead bounds for dynamic memory management with partial compaction
Dynamic memory allocation is ubiquitous in today's runtime environments. Allocation and de-allocation of objects during program execution may cause fragmentation and foil the program's ability to allocate objects. Robson has shown that a worst case scenario can create a space ove…
Step-indexed kripke models over recursive worlds
Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to some of these challenges: …
Safe nondeterminism in a deterministic-by-default parallel language
A number of deterministic parallel programming models with strong safety guarantees are emerging, but similar support for nondeterministic algorithms, such as branch and bound search, remains an open question. We present a language together with a type and effect system that supp…
Static analysis of multi-staged programs via unstaging translation
Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preservin…
Making prophecies with decision predicates
We describe a new algorithm for proving temporal properties expressed in LTL of infinite-state programs. Our approach takes advantage of the fact that LTL properties can often be proved more efficiently using techniques usually associated with the branching-time logic CTL than th…