{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:07Z","timestamp":1740123307970,"version":"3.37.3"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2019,12,10]],"date-time":"2019-12-10T00:00:00Z","timestamp":1575936000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,12,10]],"date-time":"2019-12-10T00:00:00Z","timestamp":1575936000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["1642042"],"award-info":[{"award-number":["1642042"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>\u00dcresin and Dubois\u2019 paper \u201cParallel Asynchronous Algorithms for Discrete Data\u201d shows how a class of synchronous iterative algorithms may be transformed into asynchronous iterative algorithms. They then prove that the correctness of the resulting asynchronous algorithm can be guaranteed by reasoning about the synchronous algorithm alone. These results have been used to prove the correctness of various distributed algorithms, including in the fields of routing, numerical analysis and peer-to-peer protocols. In this paper we demonstrate several ways in which the assumptions that underlie this theory may be relaxed. Amongst others, we (i) expand the set of schedules for which the asynchronous iterative algorithm is known to converge and (ii) weaken the conditions that users must prove to hold to guarantee convergence. Furthermore, we demonstrate that two of the auxiliary results in the original paper are incorrect, and explicitly construct a counter-example. Finally, we also relax the alternative convergence conditions proposed by Gurney based on ultrametrics. Many of these relaxations and errors were uncovered after formalising the work in the proof assistant Agda. This paper describes the Agda code and the library that has resulted from this work. It is hoped that the library will be of use to others wishing to formally verify the correctness of asynchronous iterative algorithms.<\/jats:p>","DOI":"10.1007\/s10817-019-09536-w","type":"journal-article","created":{"date-parts":[[2019,12,10]],"date-time":"2019-12-10T14:05:02Z","timestamp":1575986702000},"page":"857-877","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Relaxation of \u00dcresin and Dubois\u2019 Asynchronous Fixed-Point Theory in Agda"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2552-3671","authenticated-orcid":false,"given":"Matthew L.","family":"Daggitt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ran","family":"Zmigrod","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Timothy G.","family":"Griffin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,12,10]]},"reference":[{"unstructured":"Agda routing library. https:\/\/github.com\/MatthewDaggitt\/agda-routing\/tree\/jar2019. Accessed 09 Mar 2019","key":"9536_CR1"},{"unstructured":"Agda standard library. https:\/\/github.com\/agda\/agda-stdlib, version 0.17. Accessed 20 Oct 2018","key":"9536_CR2"},{"unstructured":"Agda tutorials (2019). https:\/\/agda.readthedocs.io\/en\/latest\/getting-started\/tutorial-list.html. Accessed 06 Feb 2019","key":"9536_CR3"},{"doi-asserted-by":"crossref","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda\u2013a functional language with dependent types. In: Wenzel, M., Nipkow, T. (eds.) Theorem Proving in Higher Order Logics, pp. 73\u201378. Springer, Berlin (2009)","key":"9536_CR4","DOI":"10.1007\/978-3-642-03359-9_6"},{"issue":"1","key":"9536_CR5","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1006\/jpdc.1999.1543","volume":"58","author":"H Casanova","year":"1999","unstructured":"Casanova, H., Thomason, M.G., Dongarra, J.J.: Stochastic performance prediction for iterative algorithms in distributed environments. J. Parallel Distrib. Comput. 58(1), 68\u201391 (1999)","journal-title":"J. Parallel Distrib. Comput."},{"issue":"4","key":"9536_CR6","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1145\/1151659.1159957","volume":"36","author":"CK Chau","year":"2006","unstructured":"Chau, C.K.: Policy-based routing with non-strict preferences. SIGCOMM Comput. Commun. Rev. 36(4), 387\u2013398 (2006)","journal-title":"SIGCOMM Comput. Commun. Rev."},{"unstructured":"Chau, M.: Algorithmes parall\u00e8les asynchrones pour la simulation num\u00e9rique. Ph.D. thesis, Institut National Polytechnique de Toulouse (2005)","key":"9536_CR7"},{"doi-asserted-by":"crossref","unstructured":"Daggitt, M.L., Gurney, A.J.T., Griffin, T.G.: Asynchronous convergence of policy-rich distributed Bellman-Ford routing protocols. In: SIGCOMM Proceedings, ACM (2018)","key":"9536_CR8","DOI":"10.1145\/3230543.3230561"},{"issue":"1","key":"9536_CR9","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/S0304-3975(02)00238-4","volume":"293","author":"B Ducourthial","year":"2003","unstructured":"Ducourthial, B., Tixeuil, S.: Self-stabilization with path algebra. Theor. Comput. Sci. 293(1), 219\u2013236 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9536_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0167-6423(02)00096-5","volume":"48","author":"SA Edwards","year":"2003","unstructured":"Edwards, S.A., Lee, E.A.: The semantics and execution of a synchronous block-diagram language. Sci. Comput. Program. 48(1), 21\u201342 (2003)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"9536_CR11","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF01407866","volume":"39","author":"MN El Tarazi","year":"1982","unstructured":"El Tarazi, M.N.: Some convergence results for asynchronous algorithms. Numer. Math. 39(3), 325\u2013340 (1982)","journal-title":"Numer. Math."},{"issue":"1","key":"9536_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0377-0427(00)00409-X","volume":"123","author":"A Frommer","year":"2000","unstructured":"Frommer, A., Szyld, D.B.: On asynchronous iterations. J. Comput. Appl. Math. 123(1), 201\u2013216 (2000)","journal-title":"J. Comput. Appl. Math."},{"unstructured":"Gurney, A.J.T.: Asynchronous iterations in ultrametric spaces. Technical report (2017). arXiv:1701.07434","key":"9536_CR13"},{"key":"9536_CR14","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.entcs.2009.10.026","volume":"255","author":"L Henrio","year":"2009","unstructured":"Henrio, L., Kamm\u00fcller, F.: Functional active objects: typing and formalisation. Electron. Notes Theor. Comput. Sci. 255, 83\u2013101 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"9536_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2010.07.004","volume":"264","author":"L Henrio","year":"2010","unstructured":"Henrio, L., Khan, M.U.: Asynchronous components with futures: semantics and proofs in Isabelle\/HOL. Electron. Notes Theor. Comput. Sci. 264(1), 35\u201353 (2010)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"9536_CR16","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/1380422.1380426","volume":"3","author":"SY Ko","year":"2008","unstructured":"Ko, S.Y., Gupta, I., Jo, Y.: A new class of nature-inspired algorithms for self-adaptive peer-to-peer computing. ACM Trans. Auton. Adapt. Syst. 3(3), 11:1\u201311:34 (2008)","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"unstructured":"Lee, H., Welch, J.L.: Applications of probabilistic quorums to iterative algorithms. In: Proceedings 21st International Conference on Distributed Computing Systems, pp. 21\u201328 (2001)","key":"9536_CR17"},{"doi-asserted-by":"crossref","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. In: International Conference on Formal Engineering Methods, pp. 303\u2013320 (2010)","key":"9536_CR18","DOI":"10.1007\/978-3-642-16901-4_21"},{"key":"9536_CR19","first-page":"353","volume":"2","author":"E Sch\u00f6rner","year":"2003","unstructured":"Sch\u00f6rner, E.: Ultrametric fixed point theorems and applications. Valuat. Theory Appl. 2, 353\u2013359 (2003)","journal-title":"Valuat. Theory Appl."},{"issue":"3","key":"9536_CR20","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1145\/79147.79162","volume":"37","author":"A \u00dcresin","year":"1990","unstructured":"\u00dcresin, A., Dubois, M.: Parallel asynchronous algorithms for discrete data. J. ACM 37(3), 588\u2013606 (1990)","journal-title":"J. ACM"},{"issue":"1","key":"9536_CR21","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1006\/jpdc.1996.0046","volume":"34","author":"A \u00dcresin","year":"1996","unstructured":"\u00dcresin, A., Dubois, M.: Effects of asynchronism on the convergence rate of iterative algorithms. J. Parallel Distrib. Comput. 34(1), 66\u201381 (1996)","journal-title":"J. Parallel Distrib. Comput."},{"issue":"8","key":"9536_CR22","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1016\/0167-8191(93)90072-S","volume":"19","author":"J Wei","year":"1993","unstructured":"Wei, J.: Parallel asynchronous iterations of least fixed points. Parallel Comput. 19(8), 887\u2013895 (1993)","journal-title":"Parallel Comput."},{"doi-asserted-by":"crossref","unstructured":"Zmigrod, R., Daggitt, M.L., Griffin, T.G.: An Agda formalization of \u00dcresin and Dubois\u2019 asynchronous fixed-point theory. In: International Conference on Interactive Theorem Proving, pp. 623\u2013639. Springer (2018)","key":"9536_CR23","DOI":"10.1007\/978-3-319-94821-8_37"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09536-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09536-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09536-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T00:35:31Z","timestamp":1607474131000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09536-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,10]]},"references-count":23,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["9536"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09536-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2019,12,10]]},"assertion":[{"value":"22 March 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 October 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 December 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}