Implicit Self-Adjusting Computation for Purely Functional Programs

  • Computational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Recent advances in self-adjusting computation made progress towards achieving efficient incremental computation by providing algorithmic language abstractions to express computations that respond automatically to dynamic changes in their inputs. Selfadjusting programs have been shown to be efficient for a broad range of problems via an explicit programming style, where the programmer uses specific primitives to identify, create and operate on data that can change over time. This dissertation presents implicit self-adjusting computation, a type directed technique for translating purely functional programs into self-adjusting programs. In this implicit approach, the programmer annotates the (toplevel) input types of the programs to be translated. Type inference finds all other types, and a type-directed translation rewrites the source program into an explicitly self-adjusting target program. The type system is related to information-flow type systems and enjoys decidable type inference via constraint solving. We prove that the translation outputs well-typed self-adjusting programs and preserves the source program’s input-output behavior, guaranteeing that translated programs respond correctly to all changes to their data. Using a cost semantics, we also prove that the translation preserves the asymptotic complexity of the source program. As a second contribution, we present two techniques to facilitate the processing of large and dynamic data in self-adjusting computation. First, we present a type system for precise dependency tracking that minimizes the time and space for storing dependency metadata. The type system improves the scalability of self-adjusting computation by eliminating an important assumption of prior work that can lead to recording spurious dependencies. We present a type-directed translation algorithm that generates correct selfadjusting programs without relying on this assumption. Second, we show a probabilistic-chunking technique to further decrease space usage by controlling the fundamental space-time tradeoff in self-adjusting computation. We implement implicit self-adjusting computation as an extension to Standard ML with compiler and runtime support. Using the compiler, we are able to incrementalize an interesting set of applications, including standard list and matrix benchmarks, ray tracer, PageRank, sparse graph connectivity, and social circle counts. Our experiments show that our compiler incrementalizes existing code with only trivial amounts of annotation, and the resulting programs bring asymptotic improvements to large datasets from real-world applications, leading to orders of magnitude speedups in practice.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Yan Chen
URN:urn:nbn:de:hbz:386-kluedo-54175
Advisor:Umut Acar
Document Type:Doctoral Thesis
Language of publication:English
Date of Publication (online):2018/11/15
Year of first Publication:2018
Publishing Institution:Technische Universität Kaiserslautern
Granting Institution:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2017/09/21
Date of the Publication (Server):2018/11/21
Page Number:IX, 133
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
CCS-Classification (computer science):D. Software / D.1 PROGRAMMING TECHNIQUES (E) / D.1.1 Applicative (Functional) Programming
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Creative Commons 4.0 - Namensnennung (CC BY 4.0)