NJR: a Normalized Java Resource

We are on the cusp of a major opportunity: software tools that take advantage of Big Code. Specifically, Big Code will enable novel tools in areas such as security enhancers, bug finders, and code synthesizers. What do researchers need from Big Code to make progress on their tools? Our answer is an infrastructure that consists of 100,000 executable Java programs together with a set of working tools and an environment for building new tools. This Normalized Java Resource (NJR) will lower the barrier to implementation of new tools, speed up research, and ultimately help advance research frontiers. Researchers get significant advantages from using NJR. They can write scripts that base their new tool on NJR's already-working tools, and they can search NJR for programs with desired characteristics. They will receive the search result as a container that they can run either locally or on a cloud service. Additionally, they benefit from NJR's normalized representation of each Java program, which enables scalable running of tools on the entire collection. Finally, they will find that NJR's collection of programs is diverse because of our efforts to run clone detection and near-duplicate removal. In this paper we describe our vision for NJR and our current prototype.

Concurrency with Specified Orders

The need for concurrent programming is growing, especially after the multi-core revolution. This project aims to help concurrent programmers be more productive and produce software of higher quality. This will be of paramount importance for society's software infrastructure. The project will develop general techniques that are easily applicable to many mainstream programming languages such as C++, Java, and Scala. The project's novelties are a notion of specified orders along with a program logic and machine-checked proofs of well-known concurrent algorithms. The project's impacts are approaches to concurrent programming that allow programmers to write once, prove once, and run efficiently anywhere. The investigator will work with a PhD student on the project and will teach the results to students in an undergraduate course and a graduate course.

For concurrent programs, programmers often face a mismatch between their assumptions about execution and the memory model of a specific architecture. For example, a programmer may need two instructions to execute in order for the program to be correct, yet most architectures execute out of order. This project will enable programmers to specify such assumptions, prove correctness, and run efficiently on a wide variety of architectures. Specified orders are easier to understand, reason with, and optimize than existing mechanisms such as barriers (assembly language), atomic orderings (C++), and volatiles (Java, Scala).

Synergistic Software Customization

Object-oriented languages such as C++, C#, and Java have brought us software libraries that are large, well tested, and easy to re-use. However, we have reached a point where many applications are dwarfed by the libraries they import. As programmers continue to develop layers of useful libraries, programmers can work at higher and higher levels of abstraction. The trade-off for a programmer is straightforward: if 10 lines of code that rely on massive, well-tested libraries can do the same as 100 lines of code, most programmers will write the 10 lines of code. As the size and power of libraries increase, the security and efficiency of application software decrease. The problem is that the massive libraries usually add complexity and bloat to even simple tasks. Thus, we pay for the high programmer productivity with software that has a large attack surface and inefficient execution. The overarching goal of the proposed project is to exploit synergy of static and dynamic program analysis techniques to tackle the security and inefficiency problems in modern software systems.