Programming Languages (PACMPL)


Search Issue
enter search term and/or author name


Proceedings of the ACM on Programming Languages, Volume 1 Issue OOPSLA, October 2017

Here is the link to the page in the digital library for this issue. The digital library may contain some content that is not included in this table of contents, for example front and back matter for the issue.

Section: Types

SAVI objects: sharing and virtuality incorporated
Izzat El Hajj, Thomas B. Jablin, Dejan Milojicic, Wen-mei Hwu
Article No.: 45
DOI: 10.1145/3133869

Direct sharing and storing of memory objects allows high-performance and low-overhead collaboration between parallel processes or application workflows with loosely coupled programs. However, sharing of objects is hindered by the inability to use ...

A simple soundness proof for dependent object types
Marianna Rapoport, Ifaz Kabir, Paul He, Ondřej Lhoták
Article No.: 46
DOI: 10.1145/3133870

Dependent Object Types (DOT) is intended to be a core calculus for modelling Scala. Its distinguishing feature is abstract type members, fields in objects that hold types rather than values. Proving soundness of DOT has been surprisingly ...

Unifying typing and subtyping
Yanpeng Yang, Bruno C. d. S. Oliveira
Article No.: 47
DOI: 10.1145/3133871

In recent years dependent types have become a hot topic in programming language research. A key reason why dependent types are interesting is that they allow unifying types and terms, which enables both additional expressiveness and ...

Fast and precise type checking for JavaScript
Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, Gabriel Levi
Article No.: 48
DOI: 10.1145/3133872

In this paper we present the design and implementation of Flow, a fast and precise type checker for JavaScript that is used by thousands of developers on millions of lines of code at Facebook every day. Flow uses sophisticated type inference to ...

Section: Performance

A volatile-by-default JVM for server applications
Lun Liu, Todd Millstein, Madanlal Musuvathi
Article No.: 49
DOI: 10.1145/3133873

A *memory consistency model* (or simply *memory model*) defines the possible values that a shared-memory read may return in a multithreaded programming language. Choosing a memory model involves an inherent performance-programmability tradeoff. ...

Static placement of computation on heterogeneous devices
Gabriel Poesia, Breno Guimarães, Fabrício Ferracioli, Fernando Magno Quintão Pereira
Article No.: 50
DOI: 10.1145/3133874

Heterogeneous architectures characterize today hardware ranging from super-computers to smartphones. However, in spite of this importance, programming such systems is still challenging. In particular, it is challenging to map computations to ...

Skip blocks: reusing execution history to accelerate web scripts
Sarah Chasins, Rastislav Bodik
Article No.: 51
DOI: 10.1145/3133875

With more and more web scripting languages on offer, programmers have access to increasing language support for web scraping tasks. However, in our experiences collaborating with data scientists, we learned that two issues still plague ...

Virtual machine warmup blows hot and cold
Edd Barrett, Carl Friedrich Bolz-Tereick, Rebecca Killick, Sarah Mount, Laurence Tratt
Article No.: 52
DOI: 10.1145/3133876

Virtual Machines (VMs) with Just-In-Time (JIT) compilers are traditionally thought to execute programs in two phases: the initial warmup phase determines which parts of a program would most benefit from dynamic compilation, before JIT compiling ...

Section: Gradual Types and Memory

Model checking copy phases of concurrent copying garbage collection with various memory models
Tomoharu Ugawa, Tatsuya Abe, Toshiyuki Maeda
Article No.: 53
DOI: 10.1145/3133877

Modern concurrent copying garbage collection (GC), in particular, real-time GC, uses fine-grained synchronizations with a mutator, which is the application program that mutates memory, when it moves objects in its copy phase. It resolves a data ...

Sound gradual typing: only mostly dead
Spenser Bauman, Carl Friedrich Bolz-Tereick, Jeremy Siek, Sam Tobin-Hochstadt
Article No.: 54
DOI: 10.1145/3133878

While gradual typing has proven itself attractive to programmers, many systems have avoided sound gradual typing due to the run time overhead of enforcement. In the context of sound gradual typing, both anecdotal and systematic evidence has ...

The VM already knew that: leveraging compile-time knowledge to optimize gradual typing
Gregor Richards, Ellen Arteca, Alexi Turcotte
Article No.: 55
DOI: 10.1145/3133879

Programmers in dynamic languages wishing to constrain and understand the behavior of their programs may turn to gradually-typed languages, which allow types to be specified optionally and check values at the boundary between dynamic and static ...

Sound gradual typing is nominally alive and well
Fabian Muehlboeck, Ross Tate
Article No.: 56
DOI: 10.1145/3133880

Recent research has identified significant performance hurdles that sound gradual typing needs to overcome. These performance hurdles stem from the fact that the run-time checks gradual type systems insert into code can cause significant ...

Section: Tools

Effective interactive resolution of static analysis alarms
Xin Zhang, Radu Grigore, Xujie Si, Mayur Naik
Article No.: 57
DOI: 10.1145/3133881

We propose an interactive approach to resolve static analysis alarms. Our approach synergistically combines a sound but imprecise analysis with precise but unsound heuristics, through user interaction. In each iteration, it solves an optimization ...

Abridging source code
Binhang Yuan, Vijayaraghavan Murali, Christopher Jermaine
Article No.: 58
DOI: 10.1145/3133882

In this paper, we consider the problem of source code abridgment, where the goal is to remove statements from a source code in order to display the source code in a small space, while at the same time leaving the ``important'' parts of ...

Evaluating and improving semistructured merge
Guilherme Cavalcanti, Paulo Borba, Paola Accioly
Article No.: 59
DOI: 10.1145/3133883

While unstructured merge tools rely only on textual analysis to detect and resolve conflicts, semistructured merge tools go further by partially exploiting the syntactic structure and semantics of the involved artifacts. Previous studies ...

Learning to blame: localizing novice type errors with data-driven diagnosis
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
Article No.: 60
DOI: 10.1145/3138818

Localizing type errors is challenging in languages with global type inference, as the type checker must make assumptions about what the programmer intended to do. We introduce Nate, a data-driven approach to error localization based on supervised ...

Section: Synthesis

Model-assisted machine-code synthesis
Venkatesh Srinivasan, Ara Vartanian, Thomas Reps
Article No.: 61
DOI: 10.1145/3133885

Binary rewriters are tools that are used to modify the functionality of binaries lacking source code. Binary rewriters can be used to rewrite binaries for a variety of purposes including optimization, hardening, and extraction of executable ...

Synthesis of data completion scripts using finite tree automata
Xinyu Wang, Isil Dillig, Rishabh Singh
Article No.: 62
DOI: 10.1145/3133886

In application domains that store data in a tabular format, a common task is to fill the values of some cells using values stored in other cells. For instance, such data completion tasks arise in the context of missing value ...

SQLizer: query synthesis from natural language
Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, Thomas Dillig
Article No.: 63
DOI: 10.1145/3133887

This paper presents a new technique for automatically synthesizing SQL queries from natural language (NL). At the core of our technique is a new NL-based program synthesis methodology that combines semantic parsing techniques from the NLP ...

Synthesizing configuration file specifications with association rule learning
Mark Santolucito, Ennan Zhai, Rahul Dhodapkar, Aaron Shim, Ruzica Piskac
Article No.: 64
DOI: 10.1145/3133888

System failures resulting from configuration errors are one of the major reasons for the compromised reliability of today's software systems. Although many techniques have been proposed for configuration error detection, these approaches can ...

Natural synthesis of provably-correct data-structure manipulations
Xiaokang Qiu, Armando Solar-Lezama
Article No.: 65
DOI: 10.1145/3133889

This paper presents natural synthesis, which generalizes the proof-theoretic synthesis technique to support very expressive logic theories. This approach leverages the natural proof methodology and reduces an intractable, unbounded-size synthesis ...

Section: Dynamic Analysis

Practical initialization race detection for JavaScript web applications
Christoffer Quist Adamsen, Anders Møller, Frank Tip
Article No.: 66
DOI: 10.1145/3133890

Event races are a common source of subtle errors in JavaScript web applications. Several automated tools for detecting event races have been developed, but experiments show that their accuracy is generally quite low. We present a new approach ...

Efficient logging in non-volatile memory by exploiting coherency protocols
Nachshon Cohen, Michal Friedman, James R. Larus
Article No.: 67
DOI: 10.1145/3133891

Non-volatile memory technologies such as PCM, ReRAM and STT-RAM allow data to be saved to persistent storage significantly faster than hard drives or SSDs. Many of the use cases for non-volatile memory requires persistent logging since it enables ...

Heaps don't lie: countering unsoundness with heap snapshots
Neville Grech, George Fourtounis, Adrian Francalanza, Yannis Smaragdakis
Article No.: 68
DOI: 10.1145/3133892

Static analyses aspire to explore all possible executions in order to achieve soundness. Yet, in practice, they fail to capture common dynamic behavior. Enhancing static analyses with dynamic information is a common pattern, with tools such as ...

Instrumentation bias for dynamic data race detection
Benjamin P. Wood, Man Cao, Michael D. Bond, Dan Grossman
Article No.: 69
DOI: 10.1145/3133893

This paper presents Fast Instrumentation Bias (FIB), a sound and complete dynamic data race detection algorithm that improves performance by reducing or eliminating the costs of analysis atomicity. In addition to checking for errors in target ...

Section: Types and Language Design

Familia: unifying interfaces, type classes, and family polymorphism
Yizhou Zhang, Andrew C. Myers
Article No.: 70
DOI: 10.1145/3133894

Parametric polymorphism and inheritance are both important, extensively explored language mechanisms for providing code reuse and extensibility. But harmoniously integrating these apparently distinct mechanisms—and powerful recent forms of ...

Static stages for heterogeneous programming
Adrian Sampson, Kathryn S. McKinley, Todd Mytkowicz
Article No.: 71
DOI: 10.1145/3133895

Heterogeneous hardware is central to modern advances in performance and efficiency. Mainstream programming models for heterogeneous architectures, however, sacrifice safety and expressiveness in favor of low-level control over performance ...

Orca: GC and type system co-design for actor languages
Sylvan Clebsch, Juliana Franco, Sophia Drossopoulou, Albert Mingkun Yang, Tobias Wrigstad, Jan Vitek
Article No.: 72
DOI: 10.1145/3133896

ORCA is a concurrent and parallel garbage collector for actor programs, which does not require any STW steps, or synchronization mechanisms, and that has been designed to support zero-copy message passing and sharing of mutable data. ORCA is part ...

Monadic composition for deterministic, parallel batch processing
Ryan G. Scott, Omar S. Navarro Leija, Joseph Devietti, Ryan R. Newton
Article No.: 73
DOI: 10.1145/3133897

Achieving determinism on real software systems remains difficult. Even a batch-processing job, whose task is to map input bits to output bits, risks nondeterminism from thread scheduling, system calls, CPU instructions, and leakage of ...

Section: Optimizing Compilation

GLORE: generalized loop redundancy elimination upon LER-notation
Yufei Ding, Xipeng Shen
Article No.: 74
DOI: 10.1145/3133898

This paper presents GLORE, a novel approach to enabling the detection and removal of large-scoped redundant computations in nested loops. GLORE works on LER-notation, a new representation of computations in both regular and irregular loops. ...

Verifying spatial properties of array computations
Dominic Orchard, Mistral Contrastin, Matthew Danish, Andrew Rice
Article No.: 75
DOI: 10.1145/3133899

Arrays computations are at the core of numerical modelling and computational science applications. However, low-level manipulation of array indices is a source of program error. Many practitioners are aware of the need to ensure program ...

TreeFuser: a framework for analyzing and fusing general recursive tree traversals
Laith Sakka, Kirshanthan Sundararajah, Milind Kulkarni
Article No.: 76
DOI: 10.1145/3133900

Series of traversals of tree structures arise in numerous contexts: abstract syntax tree traversals in compiler passes, rendering traversals of the DOM in web browsers, kd-tree traversals in computational simulation codes. In each of these ...

The tensor algebra compiler
Fredrik Kjolstad, Shoaib Kamil, Stephen Chou, David Lugato, Saman Amarasinghe
Article No.: 77
DOI: 10.1145/3133901

Tensor algebra is a powerful tool with applications in machine learning, data analytics, engineering and the physical sciences. Tensors are often sparse and compound operations must frequently be computed in a single kernel for performance and to ...

Section: Verification

Seam: provably safe local edits on graphs
Manolis Papadakis, Gilbert Louis Bernstein, Rahul Sharma, Alex Aiken, Pat Hanrahan
Article No.: 78
DOI: 10.1145/3133902

Algorithms that create and mutate graph data structures are challenging to implement correctly. However, verifying even basic properties of low-level implementations, such as referential integrity and memory safety, remains non-trivial. ...

TiML: a functional language for practical complexity analysis with invariants
Peng Wang, Di Wang, Adam Chlipala
Article No.: 79
DOI: 10.1145/3133903

We present TiML (Timed ML), an ML-like functional language with time-complexity annotations in types. It uses indexed types to express sizes of data structures and upper bounds on running time of functions; and refinement kinds to constrain ...

FairSquare: probabilistic verification of program fairness
Aws Albarghouthi, Loris D'Antoni, Samuel Drews, Aditya V. Nori
Article No.: 80
DOI: 10.1145/3133904

With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we aggressively investigate fairness and bias in decision-making programs. First, we show that a number of recently proposed formal ...

Reasoning on divergent computations with coaxioms
Davide Ancona, Francesco Dagnino, Elena Zucca
Article No.: 81
DOI: 10.1145/3133905

Coaxioms have been recently introduced to enhance the expressive power of inference systems, by supporting interpretations which are neither purely inductive, nor coinductive. This paper proposes a novel approach based on coaxioms to capture ...

Section: Mining Software Repositories and Parsing

Restricting grammars with tree automata
Michael D. Adams, Matthew Might
Article No.: 82
DOI: 10.1145/3133906

Precedence and associativity declarations in systems like yacc resolve ambiguities in context-free grammars (CFGs) by specifying restrictions on allowed parses. However, they are special purpose and do not handle the grammatical restrictions ...

Exploiting implicit beliefs to resolve sparse usage problem in usage-based specification mining
Samantha Syeda Khairunnesa, Hoan Anh Nguyen, Tien N. Nguyen, Hridesh Rajan
Article No.: 83
DOI: 10.1145/3133907

Frameworks and libraries provide application programming interfaces (APIs) that serve as building blocks in modern software development. As APIs present the opportunity of increased productivity, it also calls for correct use to avoid buggy code. ...

DéjàVu: a map of code duplicates on GitHub
Cristina V. Lopes, Petr Maj, Pedro Martins, Vaibhav Saini, Di Yang, Jakub Zitny, Hitesh Sajnani, Jan Vitek
Article No.: 84
DOI: 10.1145/3133908

Previous studies have shown that there is a non-trivial amount of duplication in source code. This paper analyzes a corpus of 4.5 million non-fork projects hosted on GitHub representing over 428 million files written in Java, C++, Python, and ...

Understanding the use of lambda expressions in Java
Davood Mazinanian, Ameya Ketkar, Nikolaos Tsantalis, Danny Dig
Article No.: 85
DOI: 10.1145/3133909

Java 8 retrofitted lambda expressions, a core feature of functional programming, into a mainstream object-oriented language with an imperative paradigm. However, we do not know how Java developers have adapted to the functional style of thinking, ...

Section: Verification in Practice

A model for reasoning about JavaScript promises
Magnus Madsen, Ondřej Lhoták, Frank Tip
Article No.: 86
DOI: 10.1145/3133910

In JavaScript programs, asynchrony arises in situations such as web-based user-interfaces, communicating with servers through HTTP requests, and non-blocking I/O. Event-based programming is the most popular approach for managing asynchrony, ...

A verified messaging system
William Mansky, Andrew W. Appel, Aleksey Nogin
Article No.: 87
DOI: 10.1145/3133911

We present a concurrent-read exclusive-write buffer system with strong correctness and security properties. Our motivating application for this system is the distribution of sensor values in a multicomponent vehicle-control system, where some ...

Who guards the guards? formal validation of the Arm v8-m architecture specification
Alastair Reid
Article No.: 88
DOI: 10.1145/3133912

Software and hardware are increasingly being formally verified against specifications, but how can we verify the specifications themselves? This paper explores what it means to formally verify a specification. We solve three challenges: (1) How ...

Robust and compositional verification of object capability patterns
David Swasey, Deepak Garg, Derek Dreyer
Article No.: 89
DOI: 10.1145/3133913

In scenarios such as web programming, where code is linked together from multiple sources, object capability patterns (OCPs) provide an essential safeguard, enabling programmers to protect the private state of their objects from ...

Section: Testing

Type test scripts for TypeScript testing
Erik Krogh Kristensen, Anders Møller
Article No.: 90
DOI: 10.1145/3133914

TypeScript applications often use untyped JavaScript libraries. To support static type checking of such applications, the typed APIs of the libraries are expressed as separate declaration files. This raises the challenge of checking that the ...

A solver-aided language for test input generation
Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, Serdar Tasiran
Article No.: 91
DOI: 10.1145/3133915

Developing a small but useful set of inputs for tests is challenging. We show that a domain-specific language backed by a constraint solver can help the programmer with this process. The solver can generate a set of test inputs and guarantee ...

Transforming programs and tests in tandem for fault localization
Xia Li, Lingming Zhang
Article No.: 92
DOI: 10.1145/3133916

Localizing failure-inducing code is essential for software debugging. Manual fault localization can be quite tedious, error-prone, and time-consuming. Therefore, a huge body of research e orts have been dedicated to automated fault localization. ...

Automated testing of graphics shader compilers
Alastair F. Donaldson, Hugues Evrard, Andrei Lascu, Paul Thomson
Article No.: 93
DOI: 10.1145/3133917

We present an automated technique for finding defects in compilers for graphics shading languages. key challenge in compiler testing is the lack of an oracle that classifies an output as correct or incorrect; this is particularly pertinent in ...

Bounded exhaustive test-input generation on GPUs
Ahmet Celik, Sreepathi Pai, Sarfraz Khurshid, Milos Gligoric
Article No.: 94
DOI: 10.1145/3133918

Bounded exhaustive testing is an effective methodology for detecting bugs in a wide range of applications. A well-known approach for bounded exhaustive testing is Korat. It generates all test inputs, up to a given small size, based on a formal ...

Section: Language Design

Project snowflake: non-blocking safe manual memory management in .NET
Matthew Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott, Aaron Blankstein, Jonathan Balkind
Article No.: 95
DOI: 10.1145/3141879

Garbage collection greatly improves programmer productivity and ensures memory safety. Manual memory management on the other hand often delivers better performance but is typically unsafe and can lead to system crashes or security ...

Alpaca: intermittent execution without checkpoints
Kiwan Maeng, Alexei Colin, Brandon Lucia
Article No.: 96
DOI: 10.1145/3133920

The emergence of energy harvesting devices creates the potential for batteryless sensing and computing devices. Such devices operate only intermittently, as energy is available, presenting a number of challenges for software developers. ...

An auditing language for preventing correlated failures in the cloud
Ennan Zhai, Ruzica Piskac, Ronghui Gu, Xun Lao, Xi Wang
Article No.: 97
DOI: 10.1145/3133921

Today's cloud services extensively rely on replication techniques to ensure availability and reliability. In complex datacenter network architectures, however, seemingly independent replica servers may inadvertently share deep dependencies ...

Reliable and automatic composition of language extensions to C: the ableC extensible language framework
Ted Kaminski, Lucas Kramer, Travis Carlson, Eric Van Wyk
Article No.: 98
DOI: 10.1145/3138224

This paper describes an extensible language framework, ableC, that allows programmers to import new, domain-specific, independently-developed language features into their programming language, in this case C. Most importantly, this framework ...

Section: Static Analysis

IDEal: efficient and precise alias-aware dataflow analysis
Johannes Späth, Karim Ali, Eric Bodden
Article No.: 99
DOI: 10.1145/3133923

Program analyses frequently track objects throughout a program, which requires reasoning about aliases. Most dataflow analysis frameworks, however, delegate the task of handling aliases to the analysis clients, which causes a number of problems. ...

Data-driven context-sensitivity for points-to analysis
Sehun Jeong, Minseok Jeon, Sungdeok Cha, Hakjoo Oh
Article No.: 100
DOI: 10.1145/3133924

We present a new data-driven approach to achieve highly cost-effective context-sensitive points-to analysis for Java. While context-sensitivity has greater impact on the analysis precision and performance than any other precision-improving ...

Automatically generating features for learning program analysis heuristics for C-like languages
Kwonsoo Chae, Hakjoo Oh, Kihong Heo, Hongseok Yang
Article No.: 101
DOI: 10.1145/3133925

We present a technique for automatically generating features for data-driven program analyses. Recently data-driven approaches for building a program analysis have been developed, which mine existing codebases and automatically learn heuristics ...

P/Taint: unified points-to and taint analysis
Neville Grech, Yannis Smaragdakis
Article No.: 102
DOI: 10.1145/3133926

Static information-flow analysis (especially taint-analysis) is a key technique in software security, computing where sensitive or untrusted data can propagate in a program. Points-to analysis is a fundamental static program analysis, ...

Section: Usability and Deadlock

Deadlock avoidance in parallel programs with futures: why parallel tasks should not wait for strangers
Tiago Cogumbreiro, Rishi Surendran, Francisco Martins, Vivek Sarkar, Vasco T. Vasconcelos, Max Grossman
Article No.: 103
DOI: 10.1145/3143359

Futures are an elegant approach to expressing parallelism in functional programs. However, combining futures with imperative programming (as in C++ or in Java) can lead to pernicious bugs in the form of data races and deadlocks, as a consequence ...

Detecting argument selection defects
Andrew Rice, Edward Aftandilian, Ciera Jaspan, Emily Johnston, Michael Pradel, Yulissa Arroyo-Paredes
Article No.: 104
DOI: 10.1145/3133928

Identifier names are often used by developers to convey additional information about the meaning of a program over and above the semantics of the programming language itself. We present an algorithm that uses this information to detect argument ...

How type errors were fixed and what students did?
Baijun Wu, Sheng Chen
Article No.: 105
DOI: 10.1145/3133929

Providing better supports for debugging type errors has been an active research area in the last three decades. Numerous approaches from different perspectives have been developed. Most approaches work well under certain conditions only, for ...

Learning user friendly type-error messages
Baijun Wu, John Peter Campora III, Sheng Chen
Article No.: 106
DOI: 10.1145/3133930

Type inference is convenient by allowing programmers to elide type annotations, but this comes at the cost of often generating very confusing and opaque type error messages that are of little help to fix type errors. Though there have been ...

Section: Distributed Systems

Geo-distribution of actor-based services
Philip A. Bernstein, Sebastian Burckhardt, Sergey Bykov, Natacha Crooks, Jose M. Faleiro, Gabriel Kliot, Alok Kumbhare, Muntasir Raihan Rahman, Vivek Shah, Adriana Szekeres, Jorgen Thelin
Article No.: 107
DOI: 10.1145/3133931

Many service applications use actors as a programming model for the middle tier, to simplify synchronization, fault-tolerance, and scalability. However, efficient operation of such actors in multiple, geographically distant datacenters is ...

Paxos made EPR: decidable reasoning about distributed protocols
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
Article No.: 108
DOI: 10.1145/3140568

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in verifying such protocols. However, ...

Verifying strong eventual consistency in distributed systems
Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, Alastair R. Beresford
Article No.: 109
DOI: 10.1145/3133933

Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly ...

Verifying distributed programs via canonical sequentialization
Alexander Bakst, Klaus v. Gleissenthall, Rami Gökhan Kıcı, Ranjit Jhala
Article No.: 110
DOI: 10.1145/3133934

We introduce canonical sequentialization, a new approach to verifying unbounded, asynchronous, message-passing programs at compile-time. Our approach builds upon the following observation: due the combinatorial explosion in complexity, ...