Imperative self-adjusting computation

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.

REFERENCES

• 1: Martín Abadi , Butler Lampson , Jean-Jacques Lévy, Analysis and caching of dependencies, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.83-91, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 2: Umut A. Acar , Guy E. Blelloch , Robert Harper, Selective memoization, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 15-17, 2003, New Orleans, Louisiana, USA
• 3: Umut A. Acar , Guy E. Blelloch , Robert Harper , Jorge L. Vittes , Shan Leung Maverick Woo, Dynamizing static algorithms, with applications to dynamic trees and history independence, Proceedings of the fifteenth annual ACM-SIAM symposium on Discrete algorithms, January 11-14, 2004, New Orleans, Louisiana
• 4: 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.
• 5: Umut A. Acar , Guy E. Blelloch , Matthias Blume , Kanat Tangwongsan, An experimental analysis of self-adjusting computation, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 6: Umut A. Acar , Guy E. Blelloch , Robert Harper, Adaptive functional programming, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.990-1034, November 2006 [doi>10.1145/1186632.1186634]
• 7: Umut A. Acar , Guy E. Blelloch , Kanat Tangwongsan , Jorge L. Vittes, Kinetic algorithms via self-adjusting computation, Proceedings of the 14th conference on Annual European Symposium, p.636-647, September 11-13, 2006, Zurich, Switzerland [doi>10.1007/11841036_57]
• 8: 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.
• 9: 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.
• 10: Umut A. Acar, Alexander Ihler, Ramgopal Mettu, and Ozgur Sumer. Adaptive bayesian inference. In Neural Information Systems (NIPS), 2007.
• 11: 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.
• 12: Amal Ahmed , Matthew Fluet , Greg Morrisett, A step-indexed model of substructural state, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 13: Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
• 14: Richard Ernest Bellman, Dynamic Programming, Dover Publications, Incorporated, 2003
• 15: 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.
• 16: 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.
• 17: Magnus Carlsson, Monads for incremental computing, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.26-35, October 04-06, 2002, Pittsburgh, PA, USA
• 18: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 19: Alan Demers , Thomas Reps , Tim Teitelbaum, Incremental evaluation for attribute grammars with application to syntax-directed editors, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-116, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567544]
• 20: P. Dietz , D. Sleator, Two algorithms for maintaining order in a list, Proceedings of the nineteenth annual ACM symposium on Theory of computing, p.365-372, January 1987, New York, New York, United States [doi>10.1145/28395.28434]
• 21: James R. Driscoll , Neil Sarnak , Daniel D. Sleator , Robert E. Tarjan, Making data structures persistent, Journal of Computer and System Sciences, v.38 n.1, p.86-124, February 1989 [doi>10.1016/0022-0000(89)90034-2]
• 22: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 23: John Field , Tim Teitelbaum, Incremental reduction in the lambda calculus, Proceedings of the 1990 ACM conference on LISP and functional programming, p.307-322, June 27-29, 1990, Nice, France [doi>10.1145/91556.91679]
• 24: Allan Heydon , Roy Levin , Yuan Yu, Caching function calls using precise dependencies, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.311-320, June 18-21, 2000, Vancouver, British Columbia, Canada
• 25: Vasileios Koutavas , Mitchell Wand, Small bisimulations for reasoning about higher-order imperative programs, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.141-152, January 11-13, 2006, Charleston, South Carolina, USA
• 26: Yanhong A. Liu , Scott D. Stoller , Tim Teitelbaum, Static caching for incremental computation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.3, p.546-585, May 1998 [doi>10.1145/291889.291895]
• 27: 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.
• 28: D. Michie. 'Memo' functions and machine learning. Nature, 218:19--22, 1968.
• 29: P. W. O'Hearn , R. D. Tennent, Parametricity and local variables, Journal of the ACM (JACM), v.42 n.3, p.658-709, May 1995 [doi>10.1145/210346.210425]
• 30: Nicholas Pippenger, Pure versus impure Lisp, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.223-238, March 1997 [doi>10.1145/244795.244798]
• 31: A. M. Pitts, Reasoning about local variables with operationally-based logical relations, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.152, July 27-30, 1996
• 32: Andrew M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
• 33: William Pugh. Incremental computation via function caching. PhD thesis, Department of Computer Science, Cornell University, August 1988.
• 34: W. Pugh , T. Teitelbaum, Incremental computation via function caching, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.315-328, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75305]
• 35: G. Ramalingam , Thomas Reps, A categorized bibliography on incremental computation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.502-510, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158710]
• 36: Thomas Reps, Optimal-time incremental semantic analysis for syntax-directed editors, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.169-176, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582172]
• 37: Marco D. Santambrogio , Seda Ogrenci Memik , Vincenzo Rana , Umut A. Acar , Donatella Sciuto, A novel SoC design methodology combining adaptive software and reconfigurable hardware, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
• 38: Ajeet Shankar , Rastislav Bodík, DITTO: automatic incrementalization of data structure invariant checks (in Java), Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 39: Kurt Sieber. New steps towards full abstraction for local variables. In ACM SIGPLAN Workshop on State in Programming Languages, 1993.
• 40: Ian D. B. Stark. Names and Higher-Order Functions. Ph. D. dissertation, University of Cambridge, Cambridge, England, December 1994.
• 41: 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.
• 42: Daniel M. Yellin , Robert E. Strom, INC: a language for incremental computations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.211-236, April 1991 [doi>10.1145/103135.103137]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

General Terms:
Algorithms, Design, Languages

Keywords:
change propagation, imperative programming, incremental computation, memoization, mutable state, self-adjusting computation, step-indexed logical relations