Bringing hybrid consistency closer to programmers

Gonçalo Marcelino, Valter Balegas, Carla Ferreira

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

Hybrid consistency is a new consistency model that tries to combine the benefits of weak and strong consistency. To implement hybrid consistency, programmers have to identify conflicting operations in applications and instrument them, which is a difficult and error prone task. More recent approaches automatize the process through the use of static analysis over a specification of the application. In this paper we present a new tool that is under development that tries to make the technology more accessible for programmers. Our tool is based on the same well-founded principles of existing work, but uses an intermediate verification language, Boogie, that improves the tool usability and scope in a number of ways. Using a general language for writing specifications makes specifications easier to write and improves expressiveness. Also, we leverage the language to add a library of CRDTs, which allows the programmer to solve conflicts without coordination. We discuss the features that we have already implemented and how they contribute to improve the technology.

Original languageEnglish
Title of host publicationProceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017
PublisherAssociation for Computing Machinery, Inc
Number of pages4
ISBN (Electronic)978-1-4503-4933-8
DOIs
Publication statusPublished - 23 Apr 2017
Event3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Belgrade, Serbia
Duration: 23 Apr 201726 Apr 2017

Conference

Conference3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017
CountrySerbia
CityBelgrade
Period23/04/1726/04/17

Fingerprint

Technical writing
Specifications
Static analysis

Keywords

  • Integrity invariants
  • Replication
  • Static verification

Cite this

Marcelino, G., Balegas, V., & Ferreira, C. (2017). Bringing hybrid consistency closer to programmers. In Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017 [3064896] Association for Computing Machinery, Inc. https://doi.org/10.1145/3064889.3064896
Marcelino, Gonçalo ; Balegas, Valter ; Ferreira, Carla. / Bringing hybrid consistency closer to programmers. Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017. Association for Computing Machinery, Inc, 2017.
@inproceedings{8418b55568b74341be83e9a2fb75d0d6,
title = "Bringing hybrid consistency closer to programmers",
abstract = "Hybrid consistency is a new consistency model that tries to combine the benefits of weak and strong consistency. To implement hybrid consistency, programmers have to identify conflicting operations in applications and instrument them, which is a difficult and error prone task. More recent approaches automatize the process through the use of static analysis over a specification of the application. In this paper we present a new tool that is under development that tries to make the technology more accessible for programmers. Our tool is based on the same well-founded principles of existing work, but uses an intermediate verification language, Boogie, that improves the tool usability and scope in a number of ways. Using a general language for writing specifications makes specifications easier to write and improves expressiveness. Also, we leverage the language to add a library of CRDTs, which allows the programmer to solve conflicts without coordination. We discuss the features that we have already implemented and how they contribute to improve the technology.",
keywords = "Integrity invariants, Replication, Static verification",
author = "Gon{\cc}alo Marcelino and Valter Balegas and Carla Ferreira",
note = "partially supported by FCT-MCTES-PT NOVA LINCS project (UID/CEC/04516/2013), FCT/MCT SFRH/BD/87540/2012, EU FP7 SyncFree project (609551), and EU H2020 LightKone project (732505)",
year = "2017",
month = "4",
day = "23",
doi = "10.1145/3064889.3064896",
language = "English",
booktitle = "Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017",
publisher = "Association for Computing Machinery, Inc",

}

Marcelino, G, Balegas, V & Ferreira, C 2017, Bringing hybrid consistency closer to programmers. in Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017., 3064896, Association for Computing Machinery, Inc, 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017, Belgrade, Serbia, 23/04/17. https://doi.org/10.1145/3064889.3064896

Bringing hybrid consistency closer to programmers. / Marcelino, Gonçalo; Balegas, Valter; Ferreira, Carla.

Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017. Association for Computing Machinery, Inc, 2017. 3064896.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Bringing hybrid consistency closer to programmers

AU - Marcelino, Gonçalo

AU - Balegas, Valter

AU - Ferreira, Carla

N1 - partially supported by FCT-MCTES-PT NOVA LINCS project (UID/CEC/04516/2013), FCT/MCT SFRH/BD/87540/2012, EU FP7 SyncFree project (609551), and EU H2020 LightKone project (732505)

PY - 2017/4/23

Y1 - 2017/4/23

N2 - Hybrid consistency is a new consistency model that tries to combine the benefits of weak and strong consistency. To implement hybrid consistency, programmers have to identify conflicting operations in applications and instrument them, which is a difficult and error prone task. More recent approaches automatize the process through the use of static analysis over a specification of the application. In this paper we present a new tool that is under development that tries to make the technology more accessible for programmers. Our tool is based on the same well-founded principles of existing work, but uses an intermediate verification language, Boogie, that improves the tool usability and scope in a number of ways. Using a general language for writing specifications makes specifications easier to write and improves expressiveness. Also, we leverage the language to add a library of CRDTs, which allows the programmer to solve conflicts without coordination. We discuss the features that we have already implemented and how they contribute to improve the technology.

AB - Hybrid consistency is a new consistency model that tries to combine the benefits of weak and strong consistency. To implement hybrid consistency, programmers have to identify conflicting operations in applications and instrument them, which is a difficult and error prone task. More recent approaches automatize the process through the use of static analysis over a specification of the application. In this paper we present a new tool that is under development that tries to make the technology more accessible for programmers. Our tool is based on the same well-founded principles of existing work, but uses an intermediate verification language, Boogie, that improves the tool usability and scope in a number of ways. Using a general language for writing specifications makes specifications easier to write and improves expressiveness. Also, we leverage the language to add a library of CRDTs, which allows the programmer to solve conflicts without coordination. We discuss the features that we have already implemented and how they contribute to improve the technology.

KW - Integrity invariants

KW - Replication

KW - Static verification

UR - http://www.scopus.com/inward/record.url?scp=85019217259&partnerID=8YFLogxK

U2 - 10.1145/3064889.3064896

DO - 10.1145/3064889.3064896

M3 - Conference contribution

BT - Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017

PB - Association for Computing Machinery, Inc

ER -

Marcelino G, Balegas V, Ferreira C. Bringing hybrid consistency closer to programmers. In Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2017 - Co-located with European Conference on Computer Systems, EuroSys 2017. Association for Computing Machinery, Inc. 2017. 3064896 https://doi.org/10.1145/3064889.3064896