Reasoning about Concurrent Indexes
Pedro da Rocha Pinto · 2010
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.