SPLASH Companion 2021
2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Companion 2021)
Powered by
Conference Publishing Consulting

2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Companion 2021), October 17–22, 2021, Chicago, IL, USA

SPLASH Companion 2021 – Preliminary Table of Contents

Contents - Abstracts - Authors

Frontmatter

Title Page


Message from the Chairs



Student Research Competition

Graduate Papers

Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
Wonhyuk ChoiORCID logo
(Columbia University, USA)
While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic modulo theories (TSL-MT), a framework that unites the two approaches to synthesize a single program. In our approach, reactive synthesis and SyGuS collaborate in the synthesis process, and generate executable code that implements both reactive and data-level properties. We also present a tool, temos, that combines state-of-the-art methods in reactive synthesis and SyGuS to synthesize programs from TSL-MT specifications. We demonstrate the applicability of our approach over a set of benchmarks, and present a deep case study on synthesizing a music keyboard synthesizer.

Publisher's Version Article Search
Run-Time Data Analysis in Dynamic Runtimes
Lukas Makor ORCID logo
(JKU Linz, Austria)
Databases are typically faster in processing huge amounts of data than applications with hand-coded data access. Even though modern dynamic runtimes optimize applications intensively, they cannot perform certain optimizations that are traditionally used by database systems as they lack the required information. Thus, we propose to extend the capabilities of dynamic runtimes to allow them to collect fine-grained information of the processed data at run time and use it to perform database-like optimizations. By doing so, we want to enable dynamic runtimes to significantly boost the performance of data-processing workloads. Ideally, applications should be as fast as databases in data-processing workloads. To show the feasibility of our approach, we are implementing it in a polyglot dynamic runtime.

Publisher's Version Article Search
Run-Time Data Analysis to Drive Compiler Optimizations
Sebastian KloibhoferORCID logo
(JKU Linz, Austria)
Dynamic compilers collect a variety of information to optimize programs and achieve peak performance. Nevertheless, particularly in data-heavy applications, analysis of the processed data - data structures, metrics, relations - could enable additional optimizations in terms of access patterns and data locality. Query planning in database systems is one source of inspiration, but due to the required overhead to collect such information, it is infeasible in dynamic compilers. With this project, we propose integrating data analysis into a dynamic runtime to speed up big data applications. The goal is to use the detailed run-time information for speculative compiler optimizations based on the shape and complexion of the data to improve performance.

Publisher's Version Article Search
A Study of Call Graph Effectiveness for Framework-Based Web Applications
Madhurima ChakrabortyORCID logo
(University of California at Riverside, USA)
Modern web applications are continuously evolving and becoming increasingly reliant on web frameworks to support their ever-changing needs. This necessitates the realization of efficient static analysis methodologies for the purpose of bug finding and security auditing of such applications. Moreover, the majority of these frameworks are written in JavaScript, which is difficult to analyze due to its extremely dynamic nature. The primary goal of this work is to study the effectiveness of the present state-of-the-art call graph approaches for JavaScript and propose techniques to enhance them such that they discover more of the crucial functions and call edges in modern, framework-based JavaScript applications. Ideally, these new techniques must enhance function and call edge discovery without much impact on precision and scalability.

Publisher's Version Article Search
Avoiding Monomorphization Bottlenecks with Phase-Based Splitting
Sophie Kaleba
(University of Kent, UK)
State-of-the-art managed runtimes apply aggressive optimizations speculating that programs have low variability. However, literature shows that program behavior may evolve at run time and experience different execution phases. This variable behavior may hide optimization opportunities. Taking phases into account may thus improve performance when applied to phase-sensitive optimizations such as lookup caches, which can be monomorphization bottlenecks when they contain phase-specific entries.
In this project, we introduce phase-based splitting, an optimization that utilizes phases to guide monomorphization based on splitting. Preliminary results on a first prototype and micro-benchmarks show promising speedups ranging from 10 to 20% on average, peaking at 47.6% per phase. In our next steps, we will evaluate our approach on a richer set of benchmarks and real-world applications, and define heuristics to better guide phase-based splitting.

Publisher's Version Article Search

Undergraduate Papers

Programming-by-Example by Programming-by-Example: Synthesis of Looping Programs
Shmuel Berman
(Columbia University, USA)
Program synthesis has seen many new applications in recent years, in large part thanks to the introduction of SyGuS. However, no existing SyGuS solvers have support for synthesizing recursive functions. We introduce an multi-phase algorithm for the synthesis of recursive ``looplike'' programs in SyGuS for programming-by-example. We solve constraints individually and treat them as ``unrolled`` examples of how a recursive program would behave, and solve for the generalized recursive solution. Our approach is modular and supports any SyGuS Solver.

Publisher's Version Article Search
Edgeworth: Authoring Diagrammatic Math Problems using Program Mutation
Hwei-Shin HarrimanORCID logo
(Olin College of Engineering, USA)
Building connections between mathematical expressions and their visual representations increases conceptual understanding and flexibility. However, students rarely practice visualizing abstract mathematical relationships because developing diagrammatic problems is challenging, especially at scale. To address this issue, we introduce Edgeworth, a system that automatically generates correct and incorrect diagrams for a given question prompt. It does so by mutating declarative mathematical statements with visual semantics. We evaluated the system by recreating diagrammatic problems in a widely used geometry textbook.

Publisher's Version Article Search
Towards Decidable and Expressive DOT
Sophia Roshal
(Cornell University, USA; Carnegie Mellon University, USA)
Dependent Object Types (DOT) allows mostly object oriented languages to bring in functional features and the higher expressivity of bounds on types. However, this increase in expressivity leads to DOT systems being undecidable. While decidability may be a reasonable sacrifice to make in exchange for greatly increased expressivity, having a type checker that is guaranteed to terminate while maintaining a high degree of expressivity can be beneficial. Over the last few years there have been several papers and theses written describing decidable variants of DOT. Julian Mackay et al. present one such decidable variant in their 2020 paper. Yu Xiang Zhu presents another variant in his 2019 masters thesis describing Nominal Wyvern, a variant of the DOT based programming language Wyvern. Most practical languages use nominality for recursive types which comes with benefits such as more local error messages. Due to this, we chose to focus on increasing the expressivity of Zhu's variant for this paper. However, both Zhu's and Mackay's variants present the same challenges in limitations on expressivity.

Publisher's Version Article Search
Implementation of an End-to-End Gradual Verification System
Hemant Gouni and Conrad Zimmerman
(University of Minnesota at Twin Cities, USA; Brown University, USA)
Static verification is used to ensure the correctness of programs. While useful in critical applications, the high overhead associated with writing specifications limits its general applicability. Similarly, the run-time costs introduced by dynamic verification limit its practicality. Gradual verification validates partially specified code statically where possible and dynamically where necessary. As a result, software developers gain granular control over the trade-offs between static and dynamic verification. This paper contains an end-to-end presentation of gradual verification in action, with a focus on applying it to C0 (a safe subset of C) and implementing the required dynamic verification.

Publisher's Version Article Search
Source Code Authorship Attribution using File Embeddings
Alina Bogdanova
(Innopolis University, Russia)
The problem of source code authorship attribution is crucial for a few reasons. Security and legal issues are the most popular ones. However, this domain could also help to understand the nature of the personal code style. This type of information could be used, for instance, by IDEs to improve the developer's experience of writing the code. The goal of this study is to construct an interpretable model for source code embeddings generation. Such embeddings should represent the correspondence between the source code and its author.

Publisher's Version Article Search

proc time: 3.03