ABSTRACT
Self-adjusting computation enables writing programs that can automatically and efficiently respond to changes to their data (e.g., inputs). The idea behind the approach is to store all data that can change over time in modifiable references and to let computations construct traces that can drive change propagation. After changes have occurred, change propagation updates the result of the computation by re-evaluating only those expressions that depend on the changed data. Previous approaches to self-adjusting computation require that modifiable references be written at most once during execution---this makes the model applicable only in a purely functional setting.
In this paper, we present techniques for imperative self-adjusting computation where modifiable references can be written multiple times. We define a language SAIL (Self-Adjusting Imperative Language) and prove consistency, i.e., that change propagation and from-scratch execution are observationally equivalent. Since SAIL programs are imperative, they can create cyclic data structures. To prove equivalence in the presence of cycles in the store, we formulate and use an untyped, step-indexed logical relation, where step indices are used to ensure well-foundedness. We show that SAIL accepts an asymptotically efficient implementation by presenting algorithms and data structures for its implementation. When the number of operations (reads and writes) per modifiable is bounded by a constant, we show that change propagation becomes as efficient as in the non-imperative case. The general case incurs a slowdown that is logarithmic in the maximum number of such operations. We describe a prototype implementation of SAIL as a Standard ML library.
- Martin Abadi, Butler W. Lampson, and Jean-Jacques Levy. Analysis and caching of dependencies. In Proceedings of the International Conference on Functional Programming (ICFP), pages 83--91, 1996. Google ScholarDigital Library
- Umut A. Acar, Guy E. Blelloch, and Robert Harper. Selective memoization. In Proceedings of the 30th Annual ACM Symposium on Principles of Programming Languages (POPL), 2003. Google ScholarDigital Library
- Umut A. Acar, Guy E. Blelloch, Robert Harper, Jorge L. Vittes, and Maverick Woo. Dynamizing static algorithms with applications to dynamic trees and history independence. In ACM-SIAM Symposium on Discrete Algorithms (SODA), 2004. Google ScholarDigital Library
- Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, and Kanat Tangwongsan. A library for self-adjusting computation. Electronic Notes in Theoretical Computer Science, 148(2), 2006. Also in Proceedings of the ACM-SIGPLAN Workshop on ML. 2005. Google ScholarDigital Library
- Umut A. Acar, Guy E. Blelloch, Matthias Blume, and Kanat Tangwongsan. An experimental analysis of self--adjusting computation. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2006. Google ScholarDigital Library
- Umut A. Acar, Guy E. Blelloch, and Robert Harper. Adaptive functional programming. ACM Transactions on Programming Languages and Systems (TOPLAS), 28(6):990--1034, 2006. Google ScholarDigital Library
- Umut A. Acar, Guy E. Blelloch, Kanat Tangwongsan, and Jorge L. Vittes. Kinetic algorithms via self-adjusting computation. In Proceedings of the 14th Annual European Symposium on Algorithms (ESA), pages 636--647, September 2006. Google ScholarDigital Library
- Umut A. Acar, Amal Ahmed, and Matthias Blume. Imperative self-adjusting computation. Technical Report TR-2007-18, Department of Computer Science, University of Chicago, November 2007.Google Scholar
- Umut A. Acar, Matthias Blume, and Jacob Donham. A consistent semantics of self-adjusting computation. In Proceedings of the 16th Annual European Symposium on Programming (ESOP), 2007. Google ScholarDigital Library
- Umut A. Acar, Alexander Ihler, Ramgopal Mettu, and Ozgur Sumer. Adaptive bayesian inference. In Neural Information Systems (NIPS), 2007.Google Scholar
- Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Proceedings of the 15th Annual European Symposium on Programming (ESOP), pages 69--83, 2006. Google ScholarDigital Library
- Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional programming (ICFP), pages 78--91, 2005. Google ScholarDigital Library
- Andrew W. Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(5):657--683, September 2001. Google ScholarDigital Library
- Richard Bellman. Dynamic Programming. Princeton University Press, 1957. Google ScholarDigital Library
- Nick Benton and Benjamin Leperchey. Relational reasoning in a nominal semantics for storage. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA), pages 86--101, 2005. Google ScholarDigital Library
- Nina Bohr and Lars Birkedal. Relational reasoning for recursive types and references. In Proceedings of the 4th Asian Symposium on Programming Languages and Systems (APLAS), 2006. Google ScholarDigital Library
- Magnus Carlsson. Monads for incremental computing. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional programming (ICFP), pages 26--35. ACM Press, 2002. Google ScholarDigital Library
- Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. MIT Press/McGraw-Hill, 1990. Google ScholarDigital Library
- Alan Demers, Thomas Reps, and Tim Teitelbaum. Incremental evaluation of attribute grammars with application to syntax directed editors. In Proceedings of the 8th Annual ACM Symposium on Principles of Programming Languages (POPL), pages 105--116, 1981. Google ScholarDigital Library
- P. F. Dietz and D. D. Sleator. Two algorithms for maintaining order in a list. In Proceedings of the 19th ACM Symposium on Theory of Computing (STOC), pages 365--372, 1987. Google ScholarDigital Library
- James R. Driscoll, Neil Sarnak, Daniel D. Sleator, and Robert E. Tarjan. Making data structures persistent. Journal of Computer and System Sciences, 38(1):86--124, February 1989. Google ScholarDigital Library
- Matthias Felleisen and Robert Hieb. A revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103(2):235--271, 1992. Google ScholarDigital Library
- J. Field and T. Teitelbaum. Incremental reduction in the lambda calculus. In Proceedings of the ACM '90 Conference on LISP and Functional Programming, pages 307--322, June 1990. Google ScholarDigital Library
- Allan Heydon, Roy Levin, and Yuan Yu. Caching function calls using precise dependencies. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 311--320, 2000. Google ScholarDigital Library
- Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In Proceedings of the 33rd Annual ACM Symposium on Principles of Programming Languages (POPL), 2006. Google ScholarDigital Library
- Yanhong A. Liu, Scott Stoller, and Tim Teitelbaum. Static caching for incremental computation. ACM Transactions on Programming Languages and Systems, 20(3):546--585, 1998. Google ScholarDigital Library
- John McCarthy. A Basis for a Mathematical Theory of Computation. In P. Braffort and D. Hirschberg, editors, Computer Programmingand Formal Systems, pages 33--70. North-Holland, Amsterdam, 1963.Google ScholarCross Ref
- D. Michie. 'Memo' functions and machine learning. Nature, 218:19--22, 1968.Google ScholarCross Ref
- Peter W. O'Hearn and Robert D. Tennent. Parametricity and local variables. Journal of the ACM, 42(3):658--709, May 1995. Google ScholarDigital Library
- Nicholas Pippenger. Pure versus impure lisp. ACM Transactions on Programming Languages and Systems (TOPLAS), 19(2):223--238, 1997. Google ScholarDigital Library
- Andrew M. Pitts. Reasoning about local variables with operationally--based logical relations. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS), 1996. Google ScholarDigital Library
- Andrew M. Pitts and Ian D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What's new? In Mathematical Foundations of Computer Science, volume 711 of LNCS, pages 122--141. Springer-Verlag, 1993. Google ScholarDigital Library
- William Pugh. Incremental computation via function caching. PhD thesis, Department of Computer Science, Cornell University, August 1988.Google Scholar
- William Pugh and Tim Teitelbaum. Incremental computation via function caching. In Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages (POPL), pages 315--328, 1989. Google ScholarDigital Library
- G. Ramalingam and T. Reps. A categorized bibliography on incremental computation. In Proceedings of the 20th Annual ACM Symposium on Principles of Programming Languages (POPL), pages 502--510, 1993. Google ScholarDigital Library
- Thomas Reps. Optimal-time incremental semantic analysis for syntax-directed editors. In Proceedings of the 9th Annual Symposium on Principles of Programming Languages (POPL), pages 169--176, 1982. Google ScholarDigital Library
- Marco D Santambrogio, Vincenzo Rana, Seda Ogrenci Memik, Umut A. Acar, and Donatella Sciuto. A novel SoC design methodology for combined adaptive software descripton and reconfigurable hardware. In IEEE/ACM International Conference on Computer Aided Design (ICCAD), 2007. Google ScholarDigital Library
- Ajeet Shankar and Rastislav Bodik. Ditto: Automatic incrementalization of data structure invariant checks (in Java). In Proceedings of the ACM SIGPLAN 2007 Conference on Programming language Design and Implementation (PLDI), 2007. Google ScholarDigital Library
- Kurt Sieber. New steps towards full abstraction for local variables. In ACM SIGPLAN Workshop on State in Programming Languages, 1993.Google Scholar
- Ian D. B. Stark. Names and Higher-Order Functions. Ph. D. dissertation, University of Cambridge, Cambridge, England, December 1994.Google Scholar
- R. S. Sundaresh and Paul Hudak. Incremental compilation via partial evaluation. In Conference Record of the 18th Annual ACM Symposium on Principles of Programming Languages (POPL), pages 1--13, 1991.Google Scholar
- D. M. Yellin and R. E. Strom. INC: A language for incremental computations. ACM Transactions on Programming Languages and Systems, 13(2):211--236, April 1991. Google ScholarDigital Library
Index Terms
- Imperative self-adjusting computation
Recommendations
An experimental analysis of self-adjusting computation
Recent work on adaptive functional programming (AFP) developed techniques for writing programs that can respond to modifications to their data by performing change propagation. To achieve this, executions of programs are represented with dynamic ...
Imperative self-adjusting computation
POPL '08Self-adjusting computation enables writing programs that can automatically and efficiently respond to changes to their data (e.g., inputs). The idea behind the approach is to store all data that can change over time in modifiable references and to let ...
Compiling self-adjusting programs with continuations
ICFP '08Self-adjusting programs respond automatically and efficiently to input changes by tracking the dynamic data dependences of the computation and incrementally updating the output as needed. In order to identify data dependences, previously proposed ...
Comments