https://cppcon.org/ https://github.com/CppCon/CppCon2020 --- 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.
--- Victor Cook
Victor Cook is a Ph.D. candidate in Computer Science at the University of Central Florida. He received his Bachelor of Science in Geophysics from the Massachusetts Institute of Technology in 1987, and Master of Science in Civil Engineering from the University of Florida in 1989. Mr. Cook has spent years building software and network, primarily in the areas of medical and financial technology. Systems he architected continue to serve to this day. He has been in responsible positions with sensitive data, including five years as HIPAA compliance officer, and two years as PCI compliance officer. Mr. Cook has global experience, working four years in Latin America and 18 months in Singapore. After a 25 year career in technology, he returned to UCF to earn a doctorate in the field. Mr. Cook is researching blockchain concurrency issues of performance, correctness, progress, fairness and security.
Zachary Painter is a Ph.D. student at the University of Central Florida. His area of research includes concurrent programming, transactional data structures, and blockchain concurrency. His prior work includes a lock-free transactional adjacency list as well as a parallel Hash-Mark-Set on the Ethereum Blockchain in which he proposed a fast, lock-free algorithm for providing a read-uncommitted view of blockchain transactions. Zachary has also made contributions to blockchain related research, including a read-uncommitted view for smart contract performance. During his research, he has gained experience with several blockchain platforms including Ethereum and Stellar.
Dr. Christina Peterson is a Postdoctoral Associate at the University of Central Florida. Dr. Peterson completed her dissertation work under the supervision of Dr. Damian Dechev with a focus on correctness and progress guarantees of multiprocessor algorithms and data structures. Her published work includes the development of a durable linearizable correctness tool, concurrent correctness conditions defined in vector space, a transactional correctness tool for abstract data types, a correctness condition specification tool, a framework to verify progress guarantees, and an extension of combinatorial topology theory for wait-free computability to support the instructions Compare-And-Swap and Load-Link-Store-Conditional. She also co-authored a publication that provides a read-uncommitted view for blockchain transactions.
--- Videos Filmed & Edited by Bash Films: http://www.BashFilms.com
YouTube Channel Managed by Digital Medium Ltd https://events.digital-medium.co.uk
The CppCon YouTube Channel Is Sponsored By: JetBrains : http://jb.gg/cpptools