Dissertação
Formal Specification and Verification of the Lazy JellyFish Skip List: A Case Study in Iris on the Verification of Concurrent Maps with Version Control EVALUATED
As skip lists concorrentes mais utilizadas em aplicações de armazenamento de dados permitem apenas inserções, de modo a manter múltiplas versões dos dados com diferentes timestamps, ao invés de remover informação desatualizada. Uma implementação para este género de skip lists é a JellyFish, que consegue mitigar a perda de desempenho que se observa em outras implementações devido à não-remoção de nós. A JellyFish obtém esta melhoria ao guardar em cada nó uma lista representando a linha cronológica dos valores associados à chave, em vez de inserir novos nós na lista. Neste trabalho, apresentamos uma variante da JellyFish baseada em trincos, usando uma estratégia de sincronização lazy, e verificamos formalmente a sua correção funcional. Mostramos ainda que a estrutura de dados satisfaz a especificação de um mapa concorrente. Para raciocinar sobre atualizações concorrentes a valores do mapa, definimos uma nova álgebra de recursos sobre domínios com timestamps. Usando o operador argmax para esta álgebra, conseguimos provar que escritas concorrentes no mapa mantêm cada chave associada ao seu valor mais recente. Mostramos também que estas escritas preservam a consistência da história de valores do nó atualizado. As provas estão mecanizados em Coq através da lógica de separação concorrente do Iris.
novembro 25, 2022, 14:30
Publicação
Obra sujeita a Direitos de Autor
Orientação
ORIENTADOR
João Fernando Peixoto Ferreira
Departamento de Engenharia Informática (DEI)
Professor Auxiliar