Search

X10 is a high-performance, high-productivity programming language aimed at large-scale distributed and shared-memory parallel applications. It is based on the Asynchronous Partitioned Global Address Space (APGAS) programming model, supporting the same fine-grained concurrency mechanisms within and across shared-memory nodes. We demonstrate that X10 delivers solid performance at petascale by running (weak scaling) eight application kernels on an IBM Power--775 supercomputer utilizing up to 55,680 Power7 cores (for 1.7Pflop/s of theoretical peak performance). For the four HPC Class 2 Challenge benchmarks, X10 achieves 41% to 87% of the system’s potential at scale (as measured by IBM’s HPCC Class 1 optimized runs). We also implement K-Means, Smith-Waterman, Betweenness Centrality, and Unbalanced Tree Search (UTS) for geometric trees. Our UTS implementation is the first to scale to petaflop systems. We describe the advances in distributed termination detection, distributed load balancing, and use of high-performance interconnects that enable X10 to scale out to tens of thousands of cores. We discuss how this work is driving the evolution of the X10 language, core class libraries, and runtime systems.

Log analysis is required in many domains, and especially in the emerging field of cloud computing. Cloud applications are often built by composing diverse services. When something goes wrong, finding the root cause of the problem can be difficult. Many services are only reachable through their Application Programming Interfaces (APIs) with no possibility for live introspection. In this context, logs become an essential tool for monitoring and debugging. Cloud services typically generate very large quantities of log messages, with formats that may not be well specified and may vary over time. In this paper, we present CloudLens, a language for the analysis of semi-structured textual data as found in logs, and specify its formal semantics. CloudLens is a reactive language and views logs as streams of objects. Our objective is to facilitate exploring the contents of logs interactively and to write reusable analyses succinctly, using familiar constructs. We implemented an interpreter for the Apache Zeppelin notebook to provide an interactive IDE. Our prototype implementation is open source and we report on a detailed case study using logs from the Apache OpenWhisk project.

Companies want to offer chat bots to their customers and employees which can answer questions, enable self-service, and showcase their products and services. Implementing and maintaining chat bots by hand costs time and money. Companies typically have web APIs for their services, which are often documented with an API specification. This paper presents a compiler that takes a web API specification written in Swagger and automatically generates a chat bot that helps the user make API calls. The generated bot is self-documenting, using descriptions from the API specification to answer help requests. Unfortunately, Swagger specifications are not always good enough to generate high-quality chat bots. This paper addresses this problem via a novel in-dialogue curation approach: the power user can improve the generated chat bot by interacting with it. The result is then saved back as an API specification. This paper reports on the design and implementation of the chat bot compiler, the in-dialogue curation, and working case studies.

Since our work on verification sixteen years ago, our views of the role of verification, and the centrality of correctness, have evolved. In our presentation, we’ll talk about some of our concerns about the limitations of this kind of technology, including: usability as a key factor; the unknowable properties of the environment; and the inadequacy of specifications as a means of capturing users’ desires. We’ll describe two approaches we’re currently working on to mitigate these concerns — (1) moving to higher level abstractions with correctness by construction and (2) focusing on the conceptual structure of applications — and will argue that, combined with traditional verification tools, these offer the possibility of applications that are both usable and correct.

Linked Data on the web consists of over 1000 datasets from a variety of domains. They are queried with the SPARQL query language. There exist many implementations of SPARQL, and this rich ecosystem has demanded a precise specification and compliance tests. However, the SPARQL specification has grown in complexity, and it is increasingly difficult for developers to validate their implementations. In this paper, we present a declarative specification for SPARQL, based on relational logic. It describes SPARQL with just a few operators, and is executable: queries written in it can be directly executed against real datasets.

Concurrency-related errors, such as data races, are frustratingly difficult to track down and eliminate in large object-oriented programs. Traditional approaches to preventing data races rely on protecting instruction sequences with synchronization operations. Such control-centric approaches are inherently brittle, as the burden is on the programmer to ensure that all concurrently accessed memory locations are consistently protected. Data-centric synchronization is an alternative approach that offloads some of the work on the language implementation. Data-centric synchronization groups fields of objects into atomic sets to indicate that these fields must always be updated atomically. Each atomic set has associated units of work , that is, code fragments that preserve the consistency of that atomic set. Synchronization operations are added automatically by the compiler. We present an extension to the Java programming language that integrates annotations for data-centric concurrency control. The resulting language, called AJ, relies on a type system that enables separate compilation and supports atomic sets that span multiple objects and that also supports full encapsulation for more efficient code generation. We evaluate our proposal by refactoring classes from standard libraries, as well as a number of multithreaded benchmarks, to use atomic sets. Our results suggest that data-centric synchronization is easy to use and enjoys low annotation overhead, while successfully preventing data races. Moreover, experiments on the SPECjbb benchmark suggest that acceptable performance can be achieved with a modest amount of tuning.

This paper concerns automatically verifying safety properties of concurrent programs. In our work, the safety property of interest is to check for multi-location data races in concurrent Java programs, where a multi-location data race arises when a program is supposed to maintain an invariant over multiple data locations, but accesses/updates are not protected correctly by locks. The main technical challenge that we address is how to generate a program model that retains (at least some of) the synchronization operations of the concrete program, when the concrete program uses dynamic memory allocation. Static analysis of programs typically begins with an abstraction step that generates an abstract program that operates on a finite set of abstract objects. In the presence of dynamic memory allocation, the finite number of abstract objects of the abstract program must represent the unbounded number of concrete objects that the concrete program may allocate, and thus by the pigeon-hole principle some of the abstract objects must be summary objects—they represent more than one concrete object. Because abstract summary objects represent multiple concrete objects, the program analyzer typically must perform weak updates on the abstract state of a summary object, where a weak update accumulates information. Because weak updates accumulate rather than overwrite, the analyzer is only able to determine weak judgements on the abstract state, i.e., that some property possibly holds, and not that it definitely holds. The problem with weak judgements is that determining whether an interleaved execution respects program synchronization requires the ability to determine strong judgements, i.e., that some lock is definitely held, and thus the analyzer needs to be able to perform strong updates—an overwrite of the abstract state—to enable strong judgements. We present the random-isolation abstraction as a new principle for enabling strong updates of special abstract objects. The idea is to associate with a program allocation site two abstract objects, $${r^{\sharp}}$$ and $${o^{\sharp}}$$, where $${r^{\sharp}}$$ is a non-summary object and $${o^{\sharp}}$$ is a summary object. Abstract object $${r^{\sharp}}$$ models a distinguished concrete object that is chosen at random in each program execution. Because $${r^{\sharp}}$$ is a non-summary object—i.e, it models only one concrete object—strong updates are able to be performed on its abstract state. Because which concrete object $${r^{\sharp}}$$ models is chosen randomly, a proof that a safety property holds for $${r^{\sharp}}$$ generalizes to all objects modeled by $${o^{\sharp}}$$. We implemented the random isolation abstraction in a tool called Empire, which verifies atomic-set serializability of concurrent Java programs (atomic-set serializability is one notion of multi-location data-race freedom). Random isolation allows Empire to track lock states in ways that would not otherwise have been possible with conventional approaches.

Memory models are hard to reason about due to their complexity, which stems from the need to strike a balance between ease-of-programming and allowing compiler and hardware optimizations. In this paper, we present an automated tool, MemSAT, that helps in debugging and reasoning about memory models. Given an axiomatic specification of a memory model and a multi-threaded test program containing assertions, MemSAT outputs a trace of the program in which both the assertions and the memory model axioms are satisfied, if one can be found. The tool is fully automatic and is based on a SAT solver. If it cannot find a trace, it outputs a minimal subset of the memory model and program constraints that are unsatisfiable. We used MemSAT to check several existing memory models against their published test cases, including the current Java Memory Model by Manson et al. and a revised version of it by Sevcik and Aspinall. We found subtle discrepancies between what was expected and the actual results of test programs.

X10 is a high-performance, high-productivity programming language aimed at large-scale distributed and shared-memory parallel applications. It is based on the Asynchronous Partitioned Global Address Space (APGAS) programming model, supporting the same fine-grained concurrency mechanisms within and across shared-memory nodes.We demonstrate that X10 delivers solid performance at petascale by running (weak scaling) eight application kernels on an IBM Power 775 supercomputer utilizing up to 55,680 Power7 cores (for 1.7 Pflop/s of theoretical peak performance). We detail our advances in distributed termination detection, distributed load balancing, and use of high-performance interconnects that enable X10 to scale out to tens of thousands of cores.For the four HPC Class 2 Challenge benchmarks, X10 achieves 41% to 87% of the system's potential at scale (as measured by IBM's HPCC Class 1 optimized runs). We also implement K-Means, Smith-Waterman, Betweenness Centrality, and Unbalanced Tree Search (UTS) for geometric trees. Our UTS implementation is the first to scale to petaflop systems.

Continuous data streams are ubiquitous and represent such a high volume of data that they cannot be stored to disk, yet it is often crucial for them to be analyzed in real-time. Stream processing is a programming paradigm that processes these immediately, and enables continuous analytics. Our objective is to make it easier for analysts, with little programming experience, to develop continuous analytics applications directly. We propose enhancing a spreadsheet, a pervasive tool, to obtain a programming platform for stream processing. We present the design and implementation of an enhanced spreadsheet that enables visualizing live streams, live programming to compute new streams, and exporting computations to be run on a server where they can be shared with other users, and persisted beyond the life of the spreadsheet. We formalize our core language, and present case studies that cover a range of stream processing applications.

Model checking is a proven successful technology for verifying hardware. It works, however, on only finite state machines, and most software systems have infinitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, θ, to be verified. We check θ on an abstracted, but finite, model of S. Following this approach we verified three cache coherence protocols used in distributed file systems. These protocols have to satisfy this property: “If a client believes that a cached file is valid then the authorized server believes that the client's copy is valid.” In our finite model of the system, we need only represent the “beliefs” that a client and a server have about a cached file; we can abstract from the caches, the files' contents, and even the files themselves. Moreover, by successive application of the generalization rule from predicate logic, we need only consider a model with at most two clients, one server, and one file. We used McMillan's SMV model checker; on our most complicated protocol, SMV took less than 1 s to check over 43600 reachable states.

Model checking is a proven successful technology for verifying hardware. It works, however, on only fInite state machines, and most software systems have infInitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, phi to be verifIed. We check phi on an abstracted, but fInite, model of S. Following this approach we verified three cache coherence protocols used in distributed file systems. These protocols have to satisfy this property: 'If a client believes that a cached file is valid then the authorized server believes that the client's copy is valid.' In our finite model of the system, we need only represent the 'beliefs' that a client and a server have about a cached file; we can abstract from the caches, the files' contents, and even the files themselves. Moreover, by successive application of the generalization rule from predicate logic, we need only consider a model with at most two clients, one server, and one file. We used McMillan's SMV model checker; on our most complicated protocol, SMV took less than 1 second to check over 43,600 reachable states.

Writing multi-threaded shared variable code is notoriously difficult because a given program can result in different possible executions due to non-determinism. Observed executions may also vary depending on the specific compiler and runtime system at hand. Many aspects of behavior are beyond the control of the programmer at the language's level of abstraction (e.g., compiler transformations), and as a result, debugging and performance tuning are very difficult tasks. In this position paper, we propose that the language implementation stack (compiler, runtime system) should be open, i.e., transparent, accountable, and interactive, so that the programmer may have direct access to invaluable information, and regain control over the behavior of the program in a given environment.

Previously we presented atomic sets, memory locations that share some consistency property, and units of work, code fragments that preserve consistency of atomic sets on which they are declared. We also proposed atomic-set serializability as a correctness criterion for concurrent programs, stating that units of work must be serializable for each atomic set. We showed that a set of problematic data access patterns characterize executions that are not atomic-set serializable. Our criterion subsumes data races (single-location atomic sets) and serializability (all locations in one set). In this paper, we present a dynamic analysis for detecting violations of atomic-set serializability. The analysis can be implemented efficiently, and does not depend on any specific synchronization mechanism. We implemented the analysis and evaluated it on a suite of real programs and benchmarks. We found a number of known errors as well as several problems not previously reported.

This paper describes the methods used in Empire , a tool to detect concurrency-related bugs, namely atomic-set serializability violations in Java programs. The correctness criterion is based on atomic sets of memory locations, which share a consistency property, and units of work , which preserve consistency when executed sequentially. Empire checks that, for each atomic set, its units of work are serializable. This notion subsumes data races (single-location atomic sets), and serializability (all locations in one atomic set). To obtain a sound, finite model of locking behavior for use in Empire , we devised a new abstraction principle, random isolation , which allows strong updates to be performed on the abstract counterpart of each randomly-isolated object. This permits Empire to track the status of a Java lock, even for programs that use an unbounded number of locks. The advantage of random isolation is that properties proved about a randomly-isolated object can be generalized to all objects allocated at the same site. We ran Empire on eight programs from the ConTest benchmark suite, for which Empire detected numerous violations.

We present an approach for checking code against rich specifications, based on existing work that consists of encoding the program in a relational logic and using a constraint solver to find specification violations. We improve the efficiency of this approach with a new encoding of the program that effectively slices it at the logical level with respect to the specification. We also present new encodings for integer values and arrays, enabling the verification of realistic fragments of code that manipulate both. Our technique can handle integers of much larger ranges than previously possible, and permits large sparse arrays to be handled efficiently.We present a soundness proof for our slicing algorithm and a general condition under which relational formulae may be sliced. We implemented our technique and evaluated it by checking data structure invariants of several classes taken from the Java Collections Framework. We also checked for violations of Java's equality contract in a variety of open-source programs, and found several bugs.

Getting a new programming language into the hands of users is still a huge undertaking. SAFARI is an Eclipse-based meta-tooling framework for generating language-specific IDEs that greatly accelerates that process. It exploits common themes and structures that recur in many languages and language tools. It supports the generation of language-dependent IDE services, while allowing developers to focus on the language-specific aspects of their environments rather than the surrounding IDE framework. SAFARI has been used to generate IDEs for several languages. These IDEs include such features as parser generation; editors with keyword highlighting, text folding, text completion, hyperlinking and so on; outline views, project building; and more.

OOPSLA attendees have traditionally looked to the panel program for red-meat relief from a diet of high-fiber technical track material and abstruse Onward! exotica. However, panels often feature a tired parade of the usual suspects: the same faces hawking the same hackneyed twentieth century ideas over and over again. At the same time, familiar names are a predicable draw. The effect is that it may take many years for new blood to find its way into the panel program.This panel seeks to break this logjam by featuring only panelists at or under the age of 0x20. They will offer their opinions and insights as to what we have been doing wrong for the last twenty years and what they will have to do fix it. Grudging recognition of what has gone right may be offered as well.Mechanisms to guarantee the anonymity of the most brash positions will allow the participants to be provocative as well as precocious.

Concurrency-related bugs may happen when multiple threads access shared data and interleave in ways that do not correspond to any sequential execution. Their absence is not guaranteed by the traditional notion of "data race" freedom. We present a new definition of data races in terms of 11 problematic interleaving scenarios, and prove that it is complete by showing that any execution not exhibiting these scenarios is serializable for a chosen set of locations. Our definition subsumes the traditional definition of a data race as well as high-level data races such as stale-value errors and inconsistent views. We also propose a language feature called atomic sets of locations, which lets programmers specify the existence of consistency properties between fields in objects, without specifying the properties themselves. We use static analysis to automatically infer those points in the code where synchronization is needed to avoid data races under our new definition. An important benefit of this approach is that, in general, far fewer annotations are required than is the case with existing approaches such as synchronized blocks or atomic sections. Our implementation successfully inferred the appropriate synchronization for a significant subset of Java's Standard Collections framework.

A method for finding bugs in object-oriented code is presented. It is capable of checking complex user-defined structural properties - that is, of the configuration of objects on the heap - and generates counterexample traces with no false alarms. It requires no annotation beyond the specification to be checked, and is fully automatic. The method relies on a three-step translation: from code to a formula in a first-order relational logic, then to a propositional formula, and finally to conjunctive normal form. An off-the-shelf SAT solver is then used to find a solution that constitutes a counter example. This underlying scheme, presented previously, does not scale readily. In this paper, we show how a suite of optimizations results in much improved scalability. The optimizations are based on a special treatment of relations that are known to be functional, and target all steps. The effect of the optimizations is demonstrated by application to the analysis of a red-black tree implementation.