Diplomová práce

Formální návrh distribuované hašovací tabulky

Formal design of distributed hash table

Bc. Jakub Senko
Anotace

Cílem práce je navrhnout distribuovanou hash tabulku a formálně ověřit její chování za chybových podmínek pomocí nástrojů pro kontrolu modelu. Model je založen na Infinispan, distribuovaném datovém úložišti typu klíč-hodnota s otevřeným zdrojovým kódem.

Abstract

The aim of the thesis is to design a distributed hash table and formally verify its behavior under failure conditions using model checking tools. The model is based on Infinispan, a distributed open-source in-memory key-value data store.

Klíčová slova
model checking PlusCal TLA+ distributed hash table Infinispan clustering
Zadání práce

The aim of this thesis is to design a distributed hash table and formally verify its behaviour under failure conditions (e.g. messages not delivered within timeout or node crash) using PlusCal/TLA+ languages, and describe limitations of this model. This design should match to the algorithms used in project Infinispan.

Infinispan is a distributed in-memory key/value data store written in Java. Its core functionality is distributed hash table that can survive failure in a part of its cluster. However, its design has not been formally verified yet.

Tasks:

  • study the basic concepts and algorithms used in Infinispan
  • study PlusCal algorithm language and TLC model checker
  • create model of non-transactional distributed cache and data storage/retrieval operations
  • using model checker, find cases when the cache fails to provide consistent data or prove that it’s always correct

References:

  • http://infinispan.org/
  • http://research.microsoft.com/en-us/um/people/lamport/tla/pluscal.html
  • http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods
  • https://diplomky.redhat.com/topic/show/355/formal-design-of-distributed-hash-table

Administrativní informace
Práce zkontrolována:
23. 5. 2017 18:06, doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
Plný text práce
183 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
19. 6. 2017
Práce nebyla obhájena

Vedoucí

doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
ITI FI MU

Oponent

doc. RNDr. Pavel Matula, Ph.D., učo 2927
KVI FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.