Computing Publications

Publications Home » Reasoning about Concurrent Indexes

Reasoning about Concurrent Indexes

Pedro da Rocha Pinto

Master's Thesis
Imperial College London
September, 2010
Abstract

Index data structures such as B+ trees and hash tables are used widely as the core of databases and file systems. In a world where concurrent systems are common as servers and largely increasing as personal computers, we need a way to make sure concurrent implementations do not contain bugs. We use the fact that multiple implementations share a common high-level specification and use concurrent abstract predicates to prove that an implementation satisfies such a specification. This approach allows us to reuse the abstract specification and enables high-level reasoning independent from the low-level implementation.

PDF of full publication (1.5 megabytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.