Document Open Access Logo

Incremental Computing by Differential Execution

Authors Prashant Kumar , André Pacak , Sebastian Erdweg

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.20.pdf
  • Filesize: 1.12 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Software and its engineering → Formal language definitions
  • Software and its engineering → Formal methods
  • Software and its engineering → Incremental compilers
Keywords
  • Incremental computing
  • differential semantics
  • programming language design
  • formal verification
  • big-step semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Incremental computing offers the potential for significant performance gains by efficiently updating computations in response to changing data. However, traditional approaches are either problem-specific or use an inefficient all-or-nothing strategy of rerunning affected computations entirely. This paper presents differential semantics, a novel approach that directly embeds the propagation of changes into the semantics of a general-purpose programming language. Given a precise description of input changes, differential semantics rules define how these changes are tracked and propagated through core language constructs like assignments, conditionals, and loops to produce corresponding output changes. We formalize differential semantics and verify key properties, including correctness, using the Rocq proof assistant. We also develop and formally prove a set of optimizations, particularly for loop handling, that enable asymptotic performance improvements. An implementation of the semantics as a differential interpreter achieves order-of-magnitude speedups over recomputation on the Bellman-Ford shortest path algorithm.

Cite As Get BibTex

Prashant Kumar, André Pacak, and Sebastian Erdweg. Incremental Computing by Differential Execution. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.20

Author Details

Prashant Kumar
  • JGU Mainz, Germany
André Pacak
  • JGU Mainz, Germany
Sebastian Erdweg
  • JGU Mainz, Germany

Funding

This work is supported by ERC grant AutoInc (https://doi.org/10.3030/101125325).

Supplementary Materials

References

  1. Martín Abadi, Butler Lampson, and Jean-Jacques Lévy. Analysis and caching of dependencies. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 83-91, 1996. URL: https://doi.org/10.1145/232627.232638.
  2. U. A. Acar, A. Ahmed, and M. Blume. Imperative self-adjusting computation. SIGPLAN Not., 43(1):309-322, 2008. Google Scholar
  3. U. A. Acar, G. Blelloch, R. Ley-Wild, K. Tangwongsan, and D. Turkoglu. Traceable data types for self-adjusting computation. SIGPLAN Not., 45(6):483-496, 2010. URL: https://doi.org/10.1145/1806596.1806650.
  4. Umut A. Acar. Self-Adjusting Computation. PhD thesis, Carnegie Mellon University, 2005. Google Scholar
  5. Umut A. Acar, Guy E. Blelloch, and Robert Harper. Adaptive functional programming. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 247-259, 2002. URL: https://doi.org/10.1145/503272.503296.
  6. Richard Bellman. On a routing problem. Quarterly of applied mathematics, 16(1):87-90, 1958. Google Scholar
  7. John A. Blakeley, Per-Åke Larson, and Frank Wm. Tompa. Efficiently updating materialized views. In Proceedings of the 1986 ACM SIGMOD International Conference on Management of Data, pages 61-71, 1986. Google Scholar
  8. Gerth Stølting Brodal and Riko Jacob. Dynamic planar convex hull. In Proceedings of the 43rd Annual Symposium on Foundations of Computer Science, pages 617-626, 2002. URL: https://doi.org/10.1109/SFCS.2002.1181985.
  9. Yan Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. A theory of changes for higher-order languages: Incrementalizing lambda-calculi by static differentiation. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 145-155, 2014. Google Scholar
  10. Allan Demers, Thomas Reps, and Tim Teitelbaum. Incremental evaluation for attribute grammars with application to syntax-directed editors. In Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 105-116, 1981. URL: https://doi.org/10.1145/567532.567544.
  11. Paolo G. Giarrusso, Yann Régis-Gianas, and Philipp Schuster. Incremental lambda-calculus in cache-transfer style: Static memoization by program transformation. In Proceedings of the 28th European Symposium on Programming, pages 553-580, 2019. Google Scholar
  12. Ashish Gupta, Inderpal Singh Mumick, and V. S. Subrahmanian. Maintaining views incrementally. In Proceedings of the 1993 ACM SIGMOD International Conference on Management of Data, pages 157-166, 1993. URL: https://doi.org/10.1145/170035.170066.
  13. Michael A. Hammer, Kyle Y. J. Phang, Michael Hicks, and Jeffrey S. Foster. Adapton: Composable, demand-driven incremental computation. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 156-166, 2014. Google Scholar
  14. Monika Rauch Henzinger and Valerie King. Algorithmic aspects of dynamic graph connectivity. Algorithmica, 22(1-2):119-146, 1998. Google Scholar
  15. Herbert W. Hethcote. The mathematics of infectious diseases. SIAM Review, 42(4):599-653, 2000. URL: https://doi.org/10.1137/S0036144500371907.
  16. Jacob Holm, Kristian de Lichtenberg, and Mikkel Thorup. Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity. J. ACM, 48:723-760, 2001. URL: https://doi.org/10.1145/502090.502095.
  17. Frank McSherry, Derek G. Murray, Rebecca Isaacs, and Michael Isard. Differential dataflow. In Proceedings of the 6th Biennial Conference on Innovative Data Systems Research, pages 1-11, 2013. Google Scholar
  18. Boris Motik, Yavor Nenov, Robert Piro, and Ian Horrocks. Incremental update of datalog materialisation: The backward/forward algorithm. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, pages 1560-1568, 2015. Google Scholar
  19. Mark H. Overmars. The Design of Dynamic Data Structures. Springer-Verlag, 1983. Google Scholar
  20. Mark H. Overmars and Jan van Leeuwen. Maintenance of configurations in the plane. Journal of Computer and System Sciences, 23(2):166-204, 1981. URL: https://doi.org/10.1016/0022-0000(81)90012-X.
  21. William Pugh and Tim Teitelbaum. Incremental computation via function caching. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 315-328, 1989. URL: https://doi.org/10.1145/75277.75305.
  22. Ganesan Ramalingam and Thomas Reps. A categorized bibliography on incremental computation. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 502-510, 1993. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact