Timetide: A programming model for logically synchronous distributed systems

TL;DR

Timetide introduces a novel multiclock synchronous programming model for distributed systems that achieves deterministic execution without relying on physical clock synchronization, enabling scalable and verifiable distributed applications.

Contribution

It presents the first multiclock synchronous language, Timetide, that supports distribution and formal verification without physical clock synchronization.

Findings

Timetide effectively models distributed systems with logical clocks.

The language enables formal verification of distributed programs.

Timetide removes the need for physical clock synchronization.

Abstract

Massive strides in deterministic models have been made using synchronous languages. They are mainly focused on centralised applications, as the traditional approach is to compile away the concurrency. Time triggered languages such as Giotto and Lingua Franca are suitable for distribution albeit that they rely on expensive physical clock synchronisation, which is both expensive and may suffer from scalability. Hence, deterministic programming of distributed systems remains challenging. We address the challenges of deterministic distribution by developing a novel multiclock semantics of synchronous programs. The developed semantics is amenable to seamless distribution. Moreover, our programming model, Timetide, alleviates the need for physical clock synchronisation by building on the recently proposed logical synchrony model for distributed systems. We discuss the important aspects of distributing computation, such as network communication delays, and explore the formal verification of Timetide programs. To the best of our knowledge, Timetide is the first multiclock synchronous language that is both amenable to distribution and formal verification without the need for physical clock synchronisation or clock gating.