ACM DL

ACM Transactions on

Programming Languages and Systems (TOPLAS)

Menu
Latest Articles

Adaptive Static Analysis via Learning with Bayesian Optimization

Building a cost-effective static analyzer for real-world programs is still regarded an art. One key contributor to this grim reputation is the... (more)

NEWS

TOPLAS participates in ORCID

ORCID is a community-based effort to create a global registry of unique researcher identifiers for the purpose of ensuring proper attribution of works to their creators. When you submit a manuscript for review, you will be presented with the opportunity to register for your ORCID.

Forthcoming Articles
Optimal Choice of When to Garbage Collect

We consider the ultimate limits of program-specific garbage collector (GC) performance for real programs. We first characterize the GC schedule optimization problem. Based on this characterization, we develop a linear-time dynamic programming solution that, given a program run and heap size, computes an optimal schedule of collections for a non-generational collector. Using an analysis of a heap object graph of the program, we compute a property of heap objects that we call their pre-birth time. This information enables us to extend the non-generational GC schedule problem to the generational GC case in a way that also admits a dynamic programming solution with cost cubic in the length of the trace (number of objects allocated). This improves our previously reported approximately optimal result. Our experimental results on traces from Java programs of the DaCapo benchmark suite show that there is considerable promise to reduce garbage collection costs for some programs by developing program-specific collection policies. For a given space budget, optimal schedules often obtain modest but useful time savings, and for a given time budget, optimal schedules can obtain considerable space savings.

A Machine-Learning Algorithm with Disjunctive Model for Data-Driven Program Analysis

We present a new machine-learning algorithm with disjunctive model for data-driven program analysis. One major challenge in static program analysis is a substantial amount of manual effort required for tuning the analysis performance. Recently, data-driven program analysis has emerged to address this challenge by automatically adjusting the analysis based on data through a learning algorithm. Although this new approach has proven promising for various program analysis tasks, its effectiveness has been limited due to simple-minded learning models and algorithms that are unable to capture sophisticated, in particular disjunctive, program properties. To overcome this shortcoming, this article presents a new disjunctive model for data-driven program analysis as well as a learning algorithm to find the model parameters. Our model uses boolean formulas over atomic features and therefore is able to express nonlinear combinations of program properties. Key technical challenge is efficiently determine a set of good boolean formulas as brute-force search would simply be impractical. We present a stepwise and greedy algorithm that efficiently learns boolean formulas. We show the effectiveness and generality of our algorithm with two static analyzers: context-sensitive points-to analysis for Java and flow-sensitive interval analysis for C. Experimental results show that our automated technique significantly improves the performance of the state-of-the-art techniques including ones hand-crafted by human experts.

Feature-Specific Profiling

While high-level languages come with significant readability and maintainability benefits, their performance remains difficult to predict. For example, programmers may unknowingly use language features inappropriately, which cause their programs to run slower than expected. To address this issue, we introduce feature-specific profiling}, a technique that reports performance costs in terms of linguistic constructs. These profilers help programmers find expensive uses of specific language features. We describe the architecture of such a profiler, explain prototypes for two languages, and thus provide evidence for the idea's general usefulness as a performance debugging tool.

Rethinking Incremental and Parallel Pointer Analysis

Pointer analysis is at the heart of most interprocedural program analyses. However, scaling pointer analysis to large programs is extremely challenging. In this article, we study differential pointer analysis and present a new algorithm for computing the points-to information incrementally (i.e., upon code insertion, deletion and modification). Underpinned by new observations of differential pointer analysis, our algorithm significantly advances the state-of-the-art in that it avoids redundant computations and the expensive graph reachability analysis without losing the pointer analysis precision. Moreover, it is parallel within each iteration of the fixed- point computation. We have implemented our algorithm, DPA, for Java based on the WALA framework and evaluated its performance extensively on real-world large complex applications. Experimental results show that DPA achieves more than 200X speedups over existing incremental algorithms, two to five orders of magnitude faster than the whole program pointer analysis, and also improves the performance of an incremental data race detector by orders of magnitude. Our DPA implementation is open source and has been adopted by WALA.

Practical Subtyping for Curry-Style Languages

We present a rich type system with subtyping for an extension of System F. Our type constructors include sum and product types, universal and existential quantifiers, inductive and coinductive types. The latter two may carry annotations allowing the encoding of size invariants that are used to ensure the termination of recursive programs. For example, the termination of quicksort can be derived by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed polymorphism and (co-)induction (as for Scott-encoded data types). One of the key ideas is to completely separate the notion of size from recursion. We do not check the termination of programs directly, but rather show that their (circular) typing proofs are well-founded. We then obtain termination using a standard semantic proof of normalisation. To demonstrate the practicality of our system, we provide an implementation which accepts all the examples discussed in the paper.

Probabilistic Termination by Monadic Affine Sized Typing

We introduce a system of monadic affine sized types, which substantially generalise usual sized types, and allows this way to capture probabilistic higher-order programs which terminate almost surely. Going beyond plain, strong normalisation without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility, but requires a substantial adaptation of the technique.

Interconnectability of Session-based Logical Processes

In multiparty session types, interconnection networks identify which roles in a session engage in communication (i.e. two roles are connected if they exchange a message). In session-based interpretations of linear logic the analogue notion corresponds to determining which processes are composed, or cut, using compatible channels typed by linear propositions. In this work we show that well-formed interactions represented in a session-based interpretation of classical linear logic (CLL) form strictly less expressive interconnection networks than those of a multiparty session calculus. To achieve this result we introduce a new compositional synthesis property dubbed partial multiparty compatibility (PMC), enabling us to build a global type denoting the interactions obtained by iterated composition of well-typed CLL threads. We then show that CLL composition induces PMC global types without circular interconnections between three (or more) participants. PMC is then used to define a new CLL composition rule which can form circular interconnections but preserves the deadlock-freedom of CLL.

All ACM Journals | See Full Journal Index

Search TOPLAS
enter search term and/or author name