Quantifiability: a concurrent correctness condition modeled in vector space

DOI10.1007/S00607-022-01092-3MaRDI QIDQ6161035zbMATH OpenOpenAlexFDO

Authors Victor Cook, Christina Peterson, Zachary Painter, Damian Dechev

Publication date 2 June 2023

Published in Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1905.06421

zbMATH Keywords

formal methodsconcurrent correctnessmulticore performance

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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. Desiderata for a new correctness condition are that it be independent of sequential histories, compositional, flexible as to timing, modular as to semantics and free of inherent locking or waiting. We propose Quantifiability, a novel correctness condition based on intuitive first principles. Quantifiability models a system in vector space to launch a new mathematical analysis of concurrency. The vector space model is suitable for a wide range of concurrent systems and their associated data structures. This paper formally defines quantifiability and demonstrates useful properties such as compositionality. Analysis is facilitated with linear algebra, better supported and of much more efficient time complexity than traditional combinatorial methods. We present results showing that quantifiable data structures are highly scalable due to the usage of relaxed semantics and propose entropy to evaluate the implementation trade-offs permitted by quantifiability.

Recommendations

• Concurrent correctness in vector space
• Model-checking of correctness conditions for concurrent objects
• Decidability and complexity for quiescent consistency
• Quarantining weakness. Compositional reasoning under relaxed memory models (extended abstract)
• Abstraction for concurrent objects

Cites work

• scientific article; zbMATH DE number 3614151 (Why is no real title available?)
• A scalable lock-free stack algorithm
• Abstract data types and software validation
• Abstraction for concurrent objects
• Concurrent correctness in vector space
• Counting networks
• Dynamic partial-order reduction for model checking software
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Multilevel atomicity—a new correctness criterion for database concurrency control
• Optimal dynamic partial order reduction
• Quantitative relaxation of concurrent data structures
• Relaxed schedulers can efficiently parallelize iterative algorithms
• Software for Sparse Tensor Decomposition on Emerging Computing Architectures
• Testing Shared Memories
• The serializability of concurrent database updates
• Tractable refinement checking for concurrent objects

Cited in

(2)

• Concurrent correctness in vector space
• Intermediate value linearizability: a quantitative correctness criterion

This page was built for publication: Quantifiability: a concurrent correctness condition modeled in vector space

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6161035)