A Simple Abstraction for Complex Concurrent Indexes
File(s)a-simple-abstraction-for-complex-concurrent-indexes.pdf (622.55 KB)
Submitted version
Author(s)
da Rocha Pinto, P
Dinsdale-Young, T
Dodds, M
Gardner, PA
Wheelhouse, M
Type
Conference Paper
Abstract
Indexes are ubiquitous. Examples include associative arrays, dictionaries, maps and hashes used in applications such as databases, file systems and dynamic languages. Abstractly, a sequential index can be viewed as a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. Whilst appealingly simple, this abstract specification is insufficient for reasoning about indexes accessed concurrently. We present an abstract specification for concurrent indexes. We verify several representative concurrent client applications using our specification, demonstrating that clients can reason abstractly without having to consider specific underlying implementations. Our specification would, however, mean nothing if it were not satisfied by standard implementations of concurrent indexes. We verify that our specification is satisfied by algorithms based on linked lists, hash tables and B-Link trees. The complexity of these algorithms, in particular the B-Link tree algorithm, can be completely hidden from the client's view by our abstract specification.
Date Issued
2011-10-22
Date Acceptance
2011-10-22
Citation
OOPSLA '11 Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications, 2011, pp.845-864
ISBN
978-1-4503-0940-0
Publisher
Association for Computing Machinery
Start Page
845
End Page
864
Journal / Book Title
OOPSLA '11 Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications
Copyright Statement
©2011 ACM New York, NY, USA. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in OOPSLA '11 Proceedings, (2011) http://doi.acm.org/10.1145/2048066.2048131
Identifier
http://www.doc.ic.ac.uk/~pg/
Source
2011 ACM international conference on Object oriented programming systems languages and applications
Subjects
Science & Technology
Technology
Computer Science, Information Systems
Computer Science, Software Engineering
Computer Science
Concurrency
Indexes
B-Trees
Separation Logic
Start Date
2011-10-22
Finish Date
2011-10-27
Coverage Spatial
Portland, OR