A simple abstraction for complex concurrent indexes

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.
2. Boyland, J. Checking interference with fractional permissions. In Static Analysis (2003).
3. Calcagno, C., Gardner, P., and Zarfaty, U. Context Logic and tree update. In POPL (2005), ACM.
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).
7. Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M., and Vafeiadis,V. Concurrent abstract predicates. In ECOOP (2010).
8. Dinsdale-Young, T., Gardner, P., and Wheelhouse, M. Abstraction and Refinement for Local Reasoning. In VSTTE (2010).
9. Dodds, M., Feng, X., Parkinson, M., and Vafeiadis, V. Deny-guarantee reasoning. In ESOP (2009).
10. Feng, X., Ferreira, R., and Shao, Z. On the relationship between concurrent separation logic andassume-guarantee reasoning. In ESOP (2007).
11. Filipovic, I., O'Hearn, P., Rinetzky, N., and Yang, H. Abstraction for concurrent objects. In ESOP (2010).
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.
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.
15. Malecha, G., Morrisett, G., Shinnar, A., and Wisnesky, R. Toward a verified relational database management system. In POPL (2010).
16. O'Hearn, P. W. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375 (April 2007), 271--307.
17. Parkinson, M., and Bierman, G. Separation logic and abstraction. In POPL (2005).
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.
19. Reynolds, J. Separation logic: a logic for shared mutable data structures. In LICS (2002).
20. Sagiv, Y. Concurrent operations on B*-trees with overtaking. Journal of Computer and System Sciences 33 (October 1986).
21. Sexton, A., and Thielecke, H. Reasoning about B-trees with operational semantics and separationlogic. ENTCS 218 (2008).
22. Turon, A. J., and Wand, M. A separation logic for refining concurrent objects. In POPL (2011).
23. Vafeiadis, V., and Parkinson, M. A marriage of rely/guarantee and separation logic. CONCUR (2007).

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods