SPLASH Companion 2020: Companion Proceedings of the 2020 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

There are two broad ways to construct computer systems: (1) Programming and (2) Learning. Programming makes sense when there is a clear mathematical specification, and a provably correct program to realize the specification, even though we might never write these down formally. Examples of these class of systems include databases, operating systems and tax processing systems. Learning makes sense when it is hard to write a mathematical specification, or provable implementations, even if we were to spend time and energy to write these down formally. Examples of these class of systems include image classification, NLP sentiment understanding, and language translation. In these cases, it is natural to specify intent using examples and learn a model that inductively generalizes from the examples. In this talk we consider situations where the two approaches can be combined, producing better results than using either approach in isolation. We conclude with opportunities in using programming language techniques to make ML models efficient, robust, interpretable, and verifiable.

The reliability of software that has a Deep Neural Network (DNN) as a component is urgently important today given the increasing number of critical applications being deployed with DNNs. The need for reliability raises a need for rigorous testing of the safety and trustworthiness of these systems. In the last few years, there have been a number of research efforts focused on testing DNNs. However, the test generation techniques proposed so far lack a check to determine whether the test inputs they are generating are valid, and thus invalid inputs are produced. To illustrate this situation, we explored three recent DNN testing techniques. Using deep generative model based input validation, we show that all the three techniques generate significant number of invalid test inputs. We further analyzed the test coverage achieved by the test inputs generated by the DNN testing techniques and showed how invalid test inputs can falsely inflate test coverage metrics. To overcome the inclusion of invalid inputs in testing, we propose a technique to incorporate the valid input space of the DNN model under test in the test generation process. Our technique uses a deep generative model-based algorithm to generate only valid inputs. Results of our empirical studies show that our technique is effective in eliminating invalid tests and boosting the number of valid test inputs generated.

In this talk, I will try to make a case that more computer systems researchers, including those working on programming languages and software systems, should look for new research opportunities in the field of Digital Agriculture. I will start by describing briefly several examples of broad computing challenges in this field. I will then drill deeper into a few specific examples of past or ongoing software systems projects, both from our research and that of other research groups, where new research was needed to solve important digital agriculture challenges. I will briefly discuss a wide range of federal funding opportunities available for collaborative research spanning Computer Science and many different aspects of agriculture. The key observation is that digital agriculture raises difficult and interesting research challenges for Computer Science researchers in general, and software systems researchers in particular.

Optimizing compilers use - often hand-crafted - heuristics to control optimizations such as inlining or loop unrolling. These heuristics are based on data such as size and structure of the parts to be optimized. A compilation, however, produces much more (platform specific) data that one could use as input. We thus propose the use of machine learning (ML) to derive better optimization decisions from this wealth of data and to tackle the shortcomings of hand-crafted heuristics. Ultimately, we want to shed light on the quality and performance of optimizations by using empirical data with automated feedback and updates in a production compiler.

Data confidentiality is critical but cumbersome to ensure. To help in the task, we propose a gradual, value-dependent approach to information flow control targeting a small imperative language similar to existing low-level languages. With a hybrid approach, we seek to lessen the flaws of standalone static and dynamic analyses and heighten their advantages.

The manual refactoring between APIs is a tedious and error prone task. We introduce Synthesis for Open-Source API Refactoring (SOAR), a novel technique that requires no training data to achieve API migration and refactoring. SOAR relies only on the documentation that is readily available at the release of the library to learn API representations and mapping between libraries. Using program synthesis, SOAR automatically computes the correct configuration of arguments to the APIs and any glue code that is required to invoke those APIs.

SASIL is a domain-specific language to describe and execute the specification of scheduling systems. The language interpreter operates on time-dependent behaviors and reactive events to simulate the described system. Furthermore, the interpreter is capable of selecting the appropriate actions needed to automatically schedule necessary components of the system to resolve requests. The DSL was tested by implementing an elevator control system, which is defined as a series of button requests and the requirements needed to complete each request. A multi-elevator system described using the language allowed the interpreter to complete requests 1.04 times faster on average than the traditional elevator algorithm.

Blockchains host smart contracts for voting, tokens, and other purposes. Vulnerabilities in contracts are common, often leading to the loss of money. Psamathe is a new language we are designing around a new flow abstraction, reducing asset bugs and making contracts more concise than in existing languages. We present an overview of Psamathe, and discuss two example contracts in Psamathe and Solidity.

Performance has a major impact on the overall quality of software projects. Performance bugs---bugs that substantially decrease run-time---have long been studied in software engineering, and yet they remain incredibly difficult for developers to handle. Because these bugs do not cause fail-stop errors, they are both harder to discover and to fix. As a result, techniques to help programmers detect and reason about performance are needed for managing performance bugs. Here we propose a static, probabilistic embedding technique to provide developers with useful information about potential performance bugs at the statement level. Using Leetcode samples scraped from real algorithms challenges, we use DeepWalk to embed data dependency graphs in Euclidean space. We then describe how these graph embeddings can be used to detect which statements in code are likely to contribute to performance bugs.

Erroneous software systems have led to accidents in the past. To prevent accidents, software must be tested rigorously before deployment. However, the environment that the software operates in can deviate beyond the test cases that developers evaluated the system for. An inflexible system cannot account for environmental deviations, so the goal of our research project is to improve the flexibility of software systems. Our research falls under the umbrella of formal methods. Finite state automata can be used to model the discrete actions and states that a software system can be in. We introduce consolidation, a technique that maximises permissiveness (number of paths a user can use to execute actions) while still keeping the user safe.

The static prediction of types for dynamic programming languages is a challenging and important problem. Some success for Python was demonstrated by analyzing docstrings, still, a large portion of code comes without thorough documentation. To target this problem in this work we attempt to predict return type annotations for Python functions by looking at function usage patterns. We analyzed a collection of Python packages and created a graph that captures global relationships between source code elements such as imports, calls, and definitions. Moreover, we train embeddings for functions and evaluate how the performance of predicting return types is affected by removing one of the relationship types from the dataset.

Heterogeneity, resource constraints, and scalability are obstacles to making the IoT approachable for non-specialist programmers. To be successful and appealing in these environments, library systems must be as space-efficient and flexible as possible without fundamentally changing the process of creating and maintaining shared software. Existing library frameworks emphasize some but not all of these attributes and rely on a monolithic model that preserves mutable state. We propose a finer-grained approach to software libraries that allows developers to use multiple components of a library concurrently at disjoint versions. This model defines a library as a set of independent functions with immutable global state to avoid maintaining distributed mutable state in dataflow environments. Library code is stored in a data dependency graph, which is traversed to produce a minimal copy of the library containing only what is necessary for a program. This design addresses the constraints of distributed systems and allows developers to quickly customize dependencies for their unique deployment situations.

Static program verification requires a large number of user-provided specifications, resulting in a significant upfront verification cost. One method for reducing this burden is gradual verification, a novel approach that enables developers to deal with the cost of verification incrementally — statically where possible and dynamically where necessary. In this paper, we discuss our work designing and implementing the static portion of a gradual verification tool.