Show simple item record

dc.contributor.authorDaggitt, Matthew L.
dc.contributor.authorZmigrod, Ran
dc.contributor.authorGriffin, Timothy G.
dc.date.accessioned2020-12-09T17:19:22Z
dc.date.available2020-12-09T17:19:22Z
dc.date.issued2019-12-10
dc.date.submitted2019-03-22
dc.identifier.issn0168-7433
dc.identifier.others10817-019-09536-w
dc.identifier.other9536
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/314929
dc.description.abstractAbstract: Üresin and Dubois’ paper “Parallel Asynchronous Algorithms for Discrete Data” 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.
dc.languageen
dc.publisherSpringer Netherlands
dc.rightsAttribution 4.0 International (CC BY 4.0)en
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/en
dc.subjectArticle
dc.subjectAsynchronous
dc.subjectIterative algorithms
dc.subjectFormalisation
dc.subjectAgda
dc.titleA Relaxation of Üresin and Dubois’ Asynchronous Fixed-Point Theory in Agda
dc.typeArticle
dc.date.updated2020-12-09T17:19:21Z
prism.endingPage877
prism.issueIdentifier5
prism.publicationNameJournal of Automated Reasoning
prism.startingPage857
prism.volume64
dc.identifier.doi10.17863/CAM.62038
dcterms.dateAccepted2019-10-25
rioxxterms.versionofrecord10.1007/s10817-019-09536-w
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/
dc.contributor.orcidDaggitt, Matthew L. [0000-0002-2552-3671]
dc.identifier.eissn1573-0670
pubs.funder-project-idEngineering and Physical Sciences Research Council (1642042)


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International (CC BY 4.0)
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)