A carregar...
Publicação
Verifying and Enforcing Application Constraints in Antidote SQL
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 7.31 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
Geo-replicated storage systems are currently a fundamental piece in the development of large-scale
applications where users are distributed across the world. To meet the high requirements regarding la-
tency and availability of these applications, these database systems are forced to use weak consistency
mechanisms. However, under these consistency models, there is no guarantee that the invariants are
preserved, which can jeopardise the correctness of applications. The most obvious alternative to solve
this problem would be to use strong consistency, but this would place a large burden on the system.
Since neither of these options was feasible, many systems have been developed to preserve the
invariants of the applications without sacrificing low latency and high availability. These systems,
based on the analysis of operations, make it possible to increase the guarantees of weak consistency
by introducing consistency at the level of operations that are potentially dangerous to the invariant.
Antidote SQL is a database system that, by combining strong with weak consistency mechanisms,
attempts to guarantee the preservation of invariants at the data level. In this way, and after defining
the concurrency semantics for the application, any operation can be performed without coordination
and without the risk of violating the invariant. However, this approach has some limitations, namely
the fact that it is not trivial for developers to define appropriate concurrency semantics.
In this document, we propose a methodology for the verification and validation of defined prop-
erties, such as invariants, for applications using Antidote SQL. The proposed methodology uses a
high-level programming language with automatic verification features called VeriFx and provides
guidelines for programmers who wish to implement and verify their own systems and specifications
using this tool.
Os sistemas de armazenamento geo-replicados são atualmente uma peça fundamental no desenvolvi- mento de aplicações de grande escala em que os utilizadores se encontram espalhados pelo mundo. Com o objetivo de satisfazer os elevados requisitos em relação à latência e à disponibilidade destas aplicações, estes sistemas de bases de dados vêem-se obrigados a recorrer a mecanismos de consistên- cia fracos. No entanto, sob estes modelos de consistência não existe qualquer tipo de garantia de que os invariantes são preservados, o que pode colocar em causa a correção das aplicações. A alternativa mais óbvia para resolver este problema passaria por utilizar consistência forte, no entanto esta incutiria uma grande sobrecarga no sistema. Sendo que nenhuma destas opções é viável, muitos sistemas foram desenvolvidos no sentido de preservar os invariantes das aplicações, sem contudo, abdicar de baixas latências e alta disponibilidade. Estes sistemas, baseados na análise das operações, permitem aumentar as garantias de consistência fraca com a introdução de consistência ao nível das operações potencialmente perigosas para o invari- ante. O Antidote SQL é um sistema de base de dados que através da combinação de mecanismos de consistência fortes com mecanismos de consistência fracos tenta garantir a preservação dos invariantes ao nível dos dados. Desta forma, e depois de definidas as semânticas de concorrência para a aplicação, qualquer operação pode ser executada sem coordenação e sem perigo de quebra do invariante. No entanto esta abordagem apresenta algumas limitações nomeadamente o facto de não ser trivial para os programadores definirem as semânticas de concorrência adequadas. Neste documento propomos uma metodologia para a verificação e validação de propriedades defi- nidas, como os invariantes, para aplicações que usam o Antidote SQL. A metodologia proposta utiliza uma linguagem de programação de alto nível com capacidade de verificação automática designada por VeriFx, e fornece as diretrizes a seguir para que o programador consiga implementar e verificar os seus próprios sistemas e especificações, utilizando a ferramenta.
Os sistemas de armazenamento geo-replicados são atualmente uma peça fundamental no desenvolvi- mento de aplicações de grande escala em que os utilizadores se encontram espalhados pelo mundo. Com o objetivo de satisfazer os elevados requisitos em relação à latência e à disponibilidade destas aplicações, estes sistemas de bases de dados vêem-se obrigados a recorrer a mecanismos de consistên- cia fracos. No entanto, sob estes modelos de consistência não existe qualquer tipo de garantia de que os invariantes são preservados, o que pode colocar em causa a correção das aplicações. A alternativa mais óbvia para resolver este problema passaria por utilizar consistência forte, no entanto esta incutiria uma grande sobrecarga no sistema. Sendo que nenhuma destas opções é viável, muitos sistemas foram desenvolvidos no sentido de preservar os invariantes das aplicações, sem contudo, abdicar de baixas latências e alta disponibilidade. Estes sistemas, baseados na análise das operações, permitem aumentar as garantias de consistência fraca com a introdução de consistência ao nível das operações potencialmente perigosas para o invari- ante. O Antidote SQL é um sistema de base de dados que através da combinação de mecanismos de consistência fortes com mecanismos de consistência fracos tenta garantir a preservação dos invariantes ao nível dos dados. Desta forma, e depois de definidas as semânticas de concorrência para a aplicação, qualquer operação pode ser executada sem coordenação e sem perigo de quebra do invariante. No entanto esta abordagem apresenta algumas limitações nomeadamente o facto de não ser trivial para os programadores definirem as semânticas de concorrência adequadas. Neste documento propomos uma metodologia para a verificação e validação de propriedades defi- nidas, como os invariantes, para aplicações que usam o Antidote SQL. A metodologia proposta utiliza uma linguagem de programação de alto nível com capacidade de verificação automática designada por VeriFx, e fornece as diretrizes a seguir para que o programador consiga implementar e verificar os seus próprios sistemas e especificações, utilizando a ferramenta.
Descrição
Palavras-chave
Antidote SQL Invariants Static analysis Weak consistency