Architectural imperatives due to the slowing of Moore's Law, the broad acceptance of relaxed semantics and the O(n!) worst case verification complexity of generating sequential histories motivate a new approach to concurrent correctness. Quantifiability is proposed as a novel correctness condition that models a system in vector space to launch a new mathematical analysis of concurrency. Analysis is facilitated with linear algebra, better supported and of much more efficient time complexity than traditional combinatorial methods.
In this talk, we present the design and implementation of a lock-free quantifiable stack (QStack) and a lock-free quantifiable queue (QQueue) in the C++ programming language. Our design achieves lock-freedom using compare_exchange_strong from the C++17 Atomic Operations Library. We depict several code snippets that illustrate how quantifiable data structures are highly scalable through use of relaxed semantics, an explicit implementation trade-off permitted by quantifiability. We explain how to reason about the correctness of quantifiable data structures and present a technique and a dynamic analysis tool developed in C++ for efficiently verifying a concurrent history as quantifiably correct, referred to as Vector Space Verification (VSV). We illustrate why it is impractical to use alternative verification techniques that compare concurrent histories to sequential histories for determining correctness for real programs.
We showcase the performance of quantifiable data structures by presenting a live demonstration that runs the QStack and QQueue and plots the results in real time. The QStack is compared with the lock-free Elimination Backoff Stack and the lock-free Treiber stack. The QQueue is compared with the lock-free LCRQ, and the wait-free Fetch-And-Add queue. The live performance demonstration illustrates how the QStack and QQueue achieve substantially higher scalability than the state-of-the-art linearizable counterparts. We also present a live demonstration of our VSV tool to dynamically check a concurrent history for the QStack and QQueue as quantifiably correct in less than O(n^2) time.
ALL TALK SESSIONS CAN BE ACCESSED FROM THE MAIN LOBBY:
https://cppcon.digital-medium.co.uk/
