Proving the safety of highly-available distributed objects (Extended version)
| Autor: | Nair, Sreeja, Petri, Gustavo, Shapiro, Marc |
|---|---|
| Přispěvatelé: | DistributEd aLgorithms and sYStems (DELYS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), ARM Research [Cambridge], LIP6, Sorbonne Université, Inria, Paris, France, Arm Research, Cambridge, UK, ANR-16-CE25-0013,RainbowFS,Cohérence modulaire et conception conjointe d'un système de fichiers massif(2016), European Project: 732505,H2020,LightKone(2017), Nair, Sreeja, Cohérence modulaire et conception conjointe d'un système de fichiers massif - - RainbowFS2016 - ANR-16-CE25-0013 - AAPG2016 - VALID, Lightweight Computation for Networks at the Edge - LightKone - - H20202017-01-01 - 2019-12-31 - 732505 - VALID |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Replicated objects Tool support Distributed application design [INFO.INFO-DC] Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] Consistency [INFO.INFO-DC]Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] Automatic verification [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL] |
| Zdroj: | [0] LIP6, Sorbonne Université, Inria, Paris, France; Arm Research, Cambridge, UK. 2020 [Other] LIP6, Sorbonne Université, Inria, Paris, France; Arm Research, Cambridge, UK. 2020 |
| Popis: | To provide high availability in distributed systems, object replicas allow concurrent updates. Although replicas eventually converge, they may diverge temporarily, for instance when the network fails. This makes it difficult for the developer to reason about the object's properties , and in particular, to prove invariants over its state. For the sub-class of state-based distributed systems, we propose a proof methodology for establishing that a given object maintains a given invariant, taking into account any concurrency control. Our approach allows reasoning about individual operations separately. We demonstrate that our rules are sound, and we illustrate their use with some representative examples. We automate the rule using Boogie, an SMT-based tool. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|