Bakalářská práce

Relaxed Memory Models in DiVinE

Vojtěch Havel, učo 359437
Anotace

V této práci navrhujeme rozšíření nástroje DiVinE, které umožní verifikaci modelů specifikovaných v modelovacím jazyce DVE pod slabším paměťovým modelem než je tzv. Sequential Consistency (CS). Dále v práci navrhujeme proceduru na syntézu pozic zápisů do paměti, které je potřeba provést atomicky, aby byl program korektní nad SC korektní i nad tímto slabším paměťovým modelem.

Abstract

In this thesis we suggest an extension of the DiVinE model checker which allows verification of models written in the DVE modelling language under a weaker memory model than the Sequential Consistency (SC) memory model. On the top of this extension we devise a synthesis procedure that can compute a set of positions of writes which should be atomised in order to repair a parallel program correct on SC, but not on the weaker memory model.

Klíčová slova
model checking memory model TSO PSO DVE DiVinE
Zadání práce
DiVinE model checker verifies parallel programs written in DVE modelling language under the Sequential Consistency memory model. The goal of the thesis is to extend the workflow of the model checking procedure to allow for LTL verification of DVE models under weaker memory model. The extension should offer an algorithmic procedure to synthesise position of synchronisation primitives (atomic writes) with respect to the desired LTL specification.
Administrativní informace
Práce zkontrolována:
24. 5. 2012 14:04, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
339 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
18. 6. 2012
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponent

RNDr. Petr Ročkai, Ph.D., učo 139761
KPSK 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
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Vojtěch Havel FI B-IN PDS, učo 359437 yrkfl/7
Kryštofová, H.
23. 4. 2012
Složky
Soubory
Anotace anglicky annotation_english.txt
Havel, V.
20. 5. 2012
Anotace česky annotation.txt
Havel, V.
20. 5. 2012
Klíčová slova keywords.txt
Havel, V.
20. 5. 2012
Plný text práce bc.tmp.pdf
Havel, V.
20. 5. 2012
Posudek oponenta havel_cdwhiuei.pdf
Ročkai, P.
11. 6. 2012
Příloha attachment.tar.gz
Havel, V.
20. 5. 2012

  • 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.