SPLASH Companion Companion '20: "Why Digital Agriculture Is ..."
Why Digital Agriculture Is Fertile Ground for Software Systems Research (Keynote)
Vikram S. Adve
(University of Illinois at Urbana-Champaign, USA)
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.
@InProceedings{SPLASH Companion20p3,
author = {Vikram S. Adve},
title = {Why Digital Agriculture Is Fertile Ground for Software Systems Research (Keynote)},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {3--3},
doi = {10.1145/3426430.3434072},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Consolidation: A Technique ..."
Consolidation: A Technique for Improving Permissiveness of Human-Machine Interfaces
Sang Heon Choi
(Rose-Hulman Institute of Technology, USA)
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.
@InProceedings{SPLASH Companion20p22,
author = {Sang Heon Choi},
title = {Consolidation: A Technique for Improving Permissiveness of Human-Machine Interfaces},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {22--24},
doi = {10.1145/3426430.3428133},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Gradual Value-Dependent Information ..."
Gradual Value-Dependent Information Flow Control
Eduardo Geraldo
(NOVA-LINCS, Portugal; Nova University of Lisbon, Portugal)
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.
@InProceedings{SPLASH Companion20p7,
author = {Eduardo Geraldo},
title = {Gradual Value-Dependent Information Flow Control},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {7--9},
doi = {10.1145/3426430.3429452},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Design and Implementation ..."
Design and Implementation of a Gradual Verifier
Mona Zhang and Jacob Gorenburg
(Columbia University, USA; Haverford College, USA)
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.
@InProceedings{SPLASH Companion20p31,
author = {Mona Zhang and Jacob Gorenburg},
title = {Design and Implementation of a Gradual Verifier},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {31--33},
doi = {10.1145/3426430.3428137},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Detecting Performance Patterns ..."
Detecting Performance Patterns with Deep Learning
Sophia Kolak
(Columbia University, USA)
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.
@InProceedings{SPLASH Companion20p19,
author = {Sophia Kolak},
title = {Detecting Performance Patterns with Deep Learning},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {19--21},
doi = {10.1145/3426430.3428132},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "SASIL: A Domain-Specific Language ..."
SASIL: A Domain-Specific Language for Simulating Declarative Specifications of Scheduling Systems
Gahwon Lee
(University of Texas at Austin, USA)
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.
@InProceedings{SPLASH Companion20p13,
author = {Gahwon Lee},
title = {SASIL: A Domain-Specific Language for Simulating Declarative Specifications of Scheduling Systems},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {13--15},
doi = {10.1145/3426430.3428130},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "A Software Library Model for ..."
A Software Library Model for the Internet of Things
Ian C. McCormack
(University of Wisconsin-Eau Claire, USA)
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.
@InProceedings{SPLASH Companion20p28,
author = {Ian C. McCormack},
title = {A Software Library Model for the Internet of Things},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {28--30},
doi = {10.1145/3426430.3428136},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Machine Learning to Ease Understanding ..."
Machine Learning to Ease Understanding of Data Driven Compiler Optimizations
Raphael Mosaner
(JKU Linz, Austria)
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.
@InProceedings{SPLASH Companion20p4,
author = {Raphael Mosaner},
title = {Machine Learning to Ease Understanding of Data Driven Compiler Optimizations},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {4--6},
doi = {10.1145/3426430.3429451},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Psamathe: A DSL for Safe Blockchain ..."
Psamathe: A DSL for Safe Blockchain Assets
Reed Oei
(University of Illinois at Urbana-Champaign, USA)
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.
@InProceedings{SPLASH Companion20p16,
author = {Reed Oei},
title = {Psamathe: A DSL for Safe Blockchain Assets},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {16--18},
doi = {10.1145/3426430.3428131},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Models and Programs: Better ..."
Models and Programs: Better Together (Keynote)
Sriram K. Rajamani
(Microsoft Research, India)
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.
@InProceedings{SPLASH Companion20p1,
author = {Sriram K. Rajamani},
title = {Models and Programs: Better Together (Keynote)},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/3426430.3434070},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Evaluating Importance of Edge ..."
Evaluating Importance of Edge Types When Using Graph Neural Network for Predicting Return Types of Python Functions
Vitaly Romanov
(Innopolis University, Russia)
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.
@InProceedings{SPLASH Companion20p25,
author = {Vitaly Romanov},
title = {Evaluating Importance of Edge Types When Using Graph Neural Network for Predicting Return Types of Python Functions},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {25--27},
doi = {10.1145/3426430.3428135},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Testing Deep Neural Networks ..."
Testing Deep Neural Networks (Keynote)
Mary Lou Soffa
(University of Virginia, USA)
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.
@InProceedings{SPLASH Companion20p2,
author = {Mary Lou Soffa},
title = {Testing Deep Neural Networks (Keynote)},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {2--2},
doi = {10.1145/3426430.3434071},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "SOAR: Synthesis for Open-Source ..."
SOAR: Synthesis for Open-Source API Refactoring
Aidan Z. H. Yang
(Queen's University, Canada; Carnegie Mellon University, USA)
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.
@InProceedings{SPLASH Companion20p10,
author = {Aidan Z. H. Yang},
title = {SOAR: Synthesis for Open-Source API Refactoring},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {10--12},
doi = {10.1145/3426430.3428129},
year = {2020},
}
Publisher's Version
SPLASH Companion Companion '20: "Design and Implementation ..."
Design and Implementation of a Gradual Verifier
Mona Zhang and Jacob Gorenburg
(Columbia University, USA; Haverford College, USA)
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.
@InProceedings{SPLASH Companion20p31,
author = {Mona Zhang and Jacob Gorenburg},
title = {Design and Implementation of a Gradual Verifier},
booktitle = {Proc.\ SPLASH Companion},
publisher = {ACM},
pages = {31--33},
doi = {10.1145/3426430.3428137},
year = {2020},
}
Publisher's Version