{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:31:12Z","timestamp":1781076672467,"version":"3.54.1"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>\n            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\n            <jats:italic toggle=\"yes\">logical synchrony<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1145\/3763794","type":"journal-article","created":{"date-parts":[[2025,8,26]],"date-time":"2025-08-26T11:26:21Z","timestamp":1756207581000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Timetide: A Programming Model for Logically Synchronous Distributed Systems"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0923-0307","authenticated-orcid":false,"given":"Logan","family":"Kenwright","sequence":"first","affiliation":[{"name":"Electrical, Computer, and Software Engineering, University of Auckland","place":["Auckland, New Zealand"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9654-5678","authenticated-orcid":false,"given":"Partha","family":"Roop","sequence":"additional","affiliation":[{"name":"Electrical, Computer, and Software Engineering, University of Auckland","place":["Auckland, New Zealand"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7876-819X","authenticated-orcid":false,"given":"Nathan","family":"Allen","sequence":"additional","affiliation":[{"name":"Engineering, Computer and Mathematical Sciences, Auckland University of Technology","place":["Auckland, New Zealand"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2780-6763","authenticated-orcid":false,"given":"Calin","family":"Cascaval","sequence":"additional","affiliation":[{"name":"Google DeepMind","place":["Auckland, New Zealand"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7524-8292","authenticated-orcid":false,"given":"Avinash","family":"Malik","sequence":"additional","affiliation":[{"name":"Electrical, Computer, and Software Engineering, University of Auckland","place":["Auckland, New Zealand"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,9,26]]},"reference":[{"key":"e_1_3_4_2_2","unstructured":"Precision Clock Synchronization Protocol for Networked Measurement and Control Systems. 2004. IEEE standard in IEC\/IEEE 61588-2021 (2021) 1\u2013504."},{"key":"e_1_3_4_3_2","volume-title":"PRET-C: A New Language for Programming Precision Timed Architectures","author":"Andalam Sidharta","year":"2009","unstructured":"Sidharta Andalam, Partha Roop, Alain Girault, and Claus Traulsen. 2009. PRET-C: A New Language for Programming Precision Timed Architectures. Ph. D. Dissertation. INRIA."},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2006.06.006"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15234-4_17"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90001-E"},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44798-9_10"},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.945302"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111054"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491245"},{"key":"e_1_3_4_13_2","doi-asserted-by":"crossref","unstructured":"Stephen A. Edwards. 2018. On determinism. In Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday (2018) M. Lohstroh P. Derler and M. Sirjani (Eds.). 240\u2013253.","DOI":"10.1007\/978-3-319-95246-8_14"},{"key":"e_1_3_4_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/IECON.2018.8591550"},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10479-005-3446-x"},{"issue":"471","key":"e_1_3_4_16_2","first-page":"15","article-title":"The semantics of a simple language for parallel programming","volume":"74","author":"Gilles Kahn","year":"1974","unstructured":"Kahn Gilles. 1974. The semantics of a simple language for parallel programming. Information Processing 74, 471\u2013475 (1974), 15\u201328.","journal-title":"Information Processing"},{"key":"e_1_3_4_17_2","unstructured":"Alain Girault. 2005. A survey of automatic distribution method for synchronous programs. International Workshop on Synchronous Languages Applications and Programs (SLAP 2005)."},{"key":"e_1_3_4_18_2","doi-asserted-by":"crossref","unstructured":"M. G\u00fcnzel K.-H. Chen N. Ueter G. von der Br\u00fcggen M. D\u00fcrr and J.-J. Chen. 2021. Timing analysis of asynchronized distributed cause-effect chains. In 2021 IEEE 27th RTAS. IEEE 40\u201352.","DOI":"10.1109\/RTAS52030.2021.00012"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_4_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45449-7_12"},{"key":"e_1_3_4_21_2","doi-asserted-by":"crossref","unstructured":"Charles Antony Richard Hoare. 1978. Communicating sequential processes. Communications of the ACM 21 8 (1978) 666\u2013677.","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_4_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2024.3411017"},{"key":"e_1_3_4_23_2","doi-asserted-by":"crossref","unstructured":"Christoph M. Kirsch and Ana Sokolova. 2012. The logical execution time paradigm. In Advances in Real-Time Systems S. Chakraborty and J. Ebersp\u00e4cher (Eds.). Springer Berlin Heidelberg 103\u2013120.","DOI":"10.1007\/978-3-642-24349-3_5"},{"key":"e_1_3_4_24_2","first-page":"389","volume-title":"20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014","author":"Kroening Daniel","year":"2014","unstructured":"Daniel Kroening and Michael Tautschnig. 2014. CBMC\u2013C bounded model checker: (Competition contribution). In 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014. Springer, 389\u2013391."},{"key":"e_1_3_4_25_2","doi-asserted-by":"crossref","unstructured":"Sanjay Lall C\u0103lin Ca\u015fcaval Martin Izzard and Tammo Spalink. 2024. Logical synchrony and the bittide mechanism. IEEE Transactions on Parallel and Distributed Systems 35 11 (2024) 1936\u20131948.","DOI":"10.1109\/TPDS.2024.3444739"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.23919\/ACC53348.2022.9867698"},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453652"},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3609119"},{"key":"e_1_3_4_29_2","unstructured":"Yuliang Li Gautam Kumar Hema Hariharan Hassan Wassel Peter Hochschild Dave Platt Simon Sabato et\u00a0al. 2020. Sundial: Fault-tolerant clock synchronization for datacenters. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 1171\u20131186."},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3615357"},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3448128"},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13321-3_17"},{"key":"e_1_3_4_33_2","first-page":"197","volume-title":"International Conference on Concurrency","author":"Milner Robin","year":"1984","unstructured":"Robin Milner. 1984. Lectures on a calculus for communicating systems. In International Conference on Concurrency. Springer, 197\u2013220."},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.009"},{"key":"e_1_3_4_35_2","volume-title":"ERTS 2022-Embedded Real Time Systems","author":"Siron Fabien","year":"2022","unstructured":"Fabien Siron, Dumitru Potop-Butucaru, Robert De Simone, Damien Chabrol, and Amira Methni. 2022. The synchronous logical execution time paradigm. In ERTS 2022-Embedded Real Time Systems."},{"key":"e_1_3_4_36_2","volume-title":"Formal Semantics of the PsyC Language","author":"Siron Fabien","year":"2023","unstructured":"Fabien Siron, Dumitru Potop-Butucaru, Robert De Simone, Damien Chabrol, and Amira Methni. 2023. Formal Semantics of the PsyC Language. Ph. D. Dissertation. Inria-Sophia Antipolis."},{"key":"e_1_3_4_37_2","unstructured":"Tyler Treat. 2015. comcast. (November 2011). Retrieved Feb. 6 2025 from https:\/\/github.com\/tylertreat\/comcast"},{"key":"e_1_3_4_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.81"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763794","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T14:29:07Z","timestamp":1759933747000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,26]]},"references-count":37,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3763794"],"URL":"https:\/\/doi.org\/10.1145\/3763794","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,26]]},"assertion":[{"value":"2025-08-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-19","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}