research-article

A simple abstraction for complex concurrent indexes

Authors:

Pedro da Rocha Pinto,

Thomas Dinsdale-Young,

Philippa Gardner,

Mark WheelhouseAuthors Info & Claims

OOPSLA '11: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications

Pages 845 - 864

https://doi.org/10.1145/2048066.2048131

Published: 22 October 2011 Publication History

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.

References

[1]

Blelloch, G. E. Programming parallel algorithms. Commun. ACM 39 (March 1996), 85--97.

Digital Library

[2]

Boyland, J. Checking interference with fractional permissions. In Static Analysis (2003).

Digital Library

[3]

Calcagno, C., Gardner, P., and Zarfaty, U. Context Logic and tree update. In POPL (2005), ACM.

Digital Library

[4]

da Rocha Pinto, P. Reasoning about Concurrent Indexes. Master's thesis, Imperial College London, Sept. 2010.

[5]

da Rocha Pinto, P., Dinsdale-Young, T., Dodds, M., Gardner, P., and Wheelhouse, M. A simple abstraction for complex concurrent indexes. Tech. rep., Imperial College London, 2011.

[6]

Dillig, I., Dillig, T., and Aiken, A. Precise reasoning for programs using containers. SIGPLAN Not. 46 (2011).

Digital Library

[7]

Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M., and Vafeiadis,V. Concurrent abstract predicates. In ECOOP (2010).

Digital Library

[8]

Dinsdale-Young, T., Gardner, P., and Wheelhouse, M. Abstraction and Refinement for Local Reasoning. In VSTTE (2010).

Digital Library

[9]

Dodds, M., Feng, X., Parkinson, M., and Vafeiadis, V. Deny-guarantee reasoning. In ESOP (2009).

Digital Library

[10]

Feng, X., Ferreira, R., and Shao, Z. On the relationship between concurrent separation logic andassume-guarantee reasoning. In ESOP (2007).

Digital Library

[11]

Filipovic, I., O'Hearn, P., Rinetzky, N., and Yang, H. Abstraction for concurrent objects. In ESOP (2010).

Digital Library

[12]

Herlihy, M. P., and Wing, J. M. Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12 (July 1990), 463--492.

Digital Library

[13]

Hoare, C. A. R. Proof of a structured program: 'The sieve of Eratosthenes'. The Computer Journal 15, 4 (1972), 321--325.

[14]

Kuncak, V., Lam, P., Zee, K., and Rinard, M. C. Modular pluggable analyses for data structure consistency. IEEE Trans. Softw. Eng. 32 (December 2006), 988--1005.

Digital Library

[15]

Malecha, G., Morrisett, G., Shinnar, A., and Wisnesky, R. Toward a verified relational database management system. In POPL (2010).

Digital Library

[16]

O'Hearn, P. W. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375 (April 2007), 271--307.

Digital Library

[17]

Parkinson, M., and Bierman, G. Separation logic and abstraction. In POPL (2005).

Digital Library

[18]

Philippou, A., and Walker, D. A process-calculus analysis of concurrent operations on b-trees. J. Comput. Syst. Sci. 62, 1 (2001), 73--122.

Digital Library

[19]

Reynolds, J. Separation logic: a logic for shared mutable data structures. In LICS (2002).

Digital Library

[20]

Sagiv, Y. Concurrent operations on B*-trees with overtaking. Journal of Computer and System Sciences 33 (October 1986).

Digital Library

[21]

Sexton, A., and Thielecke, H. Reasoning about B-trees with operational semantics and separationlogic. ENTCS 218 (2008).

Digital Library

[22]

Turon, A. J., and Wand, M. A separation logic for refining concurrent objects. In POPL (2011).

Digital Library

[23]

Vafeiadis, V., and Parkinson, M. A marriage of rely/guarantee and separation logic. CONCUR (2007).

Digital Library

Cited By

Krishna SPatel NShasha DWies TDonaldson ATorlak E(2020)Verifying concurrent search structure templatesProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386029(181-196)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3386029
Krishna SShasha DWies T(2017)Go with the flow: compositional abstractions for concurrent data structuresProceedings of the ACM on Programming Languages10.1145/31581252:POPL(1-31)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158125
Fernández JKirrane SPolleres ASteyskal S(2017)Self-Enforcing Access Control for Encrypted RDFThe Semantic Web10.1007/978-3-319-58068-5_37(607-622)Online publication date: 16-May-2017
https://doi.org/10.1007/978-3-319-58068-5_37
Show More Cited By

Index Terms

A simple abstraction for complex concurrent indexes
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

A simple abstraction for complex concurrent indexes
OOPSLA '11

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 ...
Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
Lightweight Latches for B-Trees to Cope with High Contention
Database and Expert Systems Applications
Abstract
B-trees are ubiquitous for many users to store and retrieve large amounts of data concurrently. Concurrency control protocols are introduced to guarantee the physical consistency of B-trees and a high degree of parallelism without any deadlocks. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA '11: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications

October 2011

1104 pages

ISBN:9781450309400

DOI:10.1145/2048066

General Chair:
Cristina Videira Lopes
University of California, Irvine, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

ACM SIGPLAN Notices Volume 46, Issue 10
OOPSLA '11
October 2011
1063 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2076021
Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '11

Sponsor:

SIGPLAN

SPLASH '11: Conference on Systems, Programming, and Applications: Software for Humanity

October 22 - 27, 2011

Oregon, Portland, USA

Acceptance Rates

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
218
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)3

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Krishna SPatel NShasha DWies TDonaldson ATorlak E(2020)Verifying concurrent search structure templatesProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386029(181-196)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3386029
Krishna SShasha DWies T(2017)Go with the flow: compositional abstractions for concurrent data structuresProceedings of the ACM on Programming Languages10.1145/31581252:POPL(1-31)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158125
Fernández JKirrane SPolleres ASteyskal S(2017)Self-Enforcing Access Control for Encrypted RDFThe Semantic Web10.1007/978-3-319-58068-5_37(607-622)Online publication date: 16-May-2017
https://doi.org/10.1007/978-3-319-58068-5_37
Sergey INanevski ABanerjee ADelbianco G(2016)Hoare-style specifications as correctness conditions for non-linearizable concurrent objectsACM SIGPLAN Notices10.1145/3022671.298399951:10(92-110)Online publication date: 19-Oct-2016
https://dl.acm.org/doi/10.1145/3022671.2983999
Sergey INanevski ABanerjee ADelbianco GVisser ESmaragdakis Y(2016)Hoare-style specifications as correctness conditions for non-linearizable concurrent objectsProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2983990.2983999(92-110)Online publication date: 19-Oct-2016
https://dl.acm.org/doi/10.1145/2983990.2983999
Dodds MJagannathan SParkinson MSvendsen KBirkedal L(2016)Verifying Custom Synchronization Constructs Using Higher-Order Separation LogicACM Transactions on Programming Languages and Systems10.1145/281863838:2(1-72)Online publication date: 4-Jan-2016
https://dl.acm.org/doi/10.1145/2818638
Ntzik GGardner P(2015)Reasoning about the POSIX file system: local update and global pathnamesACM SIGPLAN Notices10.1145/2858965.281430650:10(201-220)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2858965.2814306
Ntzik GGardner PAldrich JEugster P(2015)Reasoning about the POSIX file system: local update and global pathnamesProceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2814270.2814306(201-220)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2814270.2814306
Jones CHayes IColvin R(2015)Balancing expressiveness in formal approaches to concurrencyFormal Aspects of Computing10.1007/s00165-014-0310-227:3(475-497)Online publication date: 1-May-2015
https://dl.acm.org/doi/10.1007/s00165-014-0310-2
Rocha Pinto PDinsdale-Young TGardner P(2014)TaDAProceedings of the 28th European Conference on ECOOP 2014 --- Object-Oriented Programming - Volume 858610.1007/978-3-662-44202-9_9(207-231)Online publication date: 1-Aug-2014
https://dl.acm.org/doi/10.1007/978-3-662-44202-9_9
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents