A Core Calculus for Static Latency Tracking with Placement Types

TL;DR

This paper introduces a core calculus that makes latency explicit in programming languages, enabling the extraction of provably correct latency bounds for geo-distributed applications.

Contribution

It presents a novel language design with placement types that explicitly track latency, facilitating correctness guarantees for distributed computations.

Findings

Enables static analysis of latency bounds

Provides a foundation for correctness in geo-distributed applications

Outlines future work for practical implementation

Abstract

Developing efficient geo-distributed applications is challenging as programmers can easily introduce computations that entail high latency communication. We propose a language design which makes latency explicit and extracts type-level bounds for a computation's runtime latency. We present our initial steps with a core calculus that enables extracting provably correct latency bounds and outline future work.