Timetide: A Programming Model for Logically Synchronous Distributed Systems
Date
Supervisor
Item type
Journal Article
Degree name
Journal Title
Journal ISSN
Volume Title
Publisher
Association for Computing Machinery (ACM)
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 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.Description
Keywords
4613 Theory Of Computation, 4606 Distributed Computing and Systems Software, 46 Information and Computing Sciences, 4612 Software Engineering, 0803 Computer Software, 0805 Distributed Computing, 1006 Computer Hardware, Computer Hardware & Architecture, 4006 Communications engineering, 4606 Distributed computing and systems software
Source
ACM Transactions on Embedded Computing Systems, ISSN: 1539-9087 (Print); 1558-3465 (Online), Association for Computing Machinery (ACM). doi: 10.1145/3763794
DOI
Publisher's version
Rights statement
Copyright © 2025 Copyright held by the owner/author(s). This work is licensed under Creative Commons Attribution International 4.0.