cda-group / arc

Programming Language for Continuous Deep Analytics
https://cda-group.github.io/arc/
44 stars 6 forks source link

Optimisation: Rate Types #331

Closed segeljakt closed 1 year ago

segeljakt commented 2 years ago

I'm putting this here for the future so I don't forget it.

Bartenstein, T.W. and Liu, Y.D., 2014, October. Rate types for stream programs. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications (pp. 213-232).

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.433.5636&rep=rep1&type=pdf

We introduce RATE TYPES, a novel type system to reason about and optimize data-intensive programs. Built around stream languages, RATE TYPES centers around static reasoning about stream rates — the frequency of data items in a stream being consumed, processed, and produced — a critical performance characteristic previously addressed by numerous experimental approaches but few foundational efforts. Our work is built upon a key insight that, even though streams are fundamentally dynamic, two essential concepts of stream rate control — throughput ratio and natural rate — are intimately related to the program structure itself. We define a type system to reason about these two concepts, and formally prove type soundness over a time aware and parallelism-aware operational semantics. We further demonstrate the usefulness of our formal framework in applications such as energy-efficient computing and CPU allocation on multi-core architectures.