ATTENTION/WARNING - NE PAS DÉPOSER ICI/DO NOT SUBMIT HERE

Ceci est la version de TEST de DIAL.mem. Veuillez ne pas soumettre votre mémoire sur ce site mais bien à l'URL suivante: 'https://thesis.dial.uclouvain.be'.
This is the TEST version of DIAL.mem. Please use the following URL to submit your master thesis: 'https://thesis.dial.uclouvain.be'.
 

A formal proof for Speculative Snapshot Isolation

d'Oreye de Lantremange, Sébastien
(2017)

Files

dOreye_72101100_2017.pdf
  • Open access
  • Adobe PDF
  • 297.35 KB
Download

Details

Supervisors
Van Roy, Peter
Faculty
Ecole polytechnique de Louvain
Degree label
Master [60] en sciences informatiques
Abstract
This work presents a formal proof for a speculative consistency model called Speculative Snapshot Isolation (SPSI). It states the SPSI properties in a formal way, proves SPSI correctness by showing that any speculative execution can be mapped to a correct, non-speculative one and shows that this mapping does not violate any SI property.