Quantifiability: a concurrent correctness condition modeled in vector space

DOI10.1007/S00607-022-01092-3zbMATH Open1519.68157arXiv1905.06421OpenAlexW4281642035MaRDI QIDQ6161035FDOQ6161035

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

Publication date: 2 June 2023

Published in: Computing (Search for Journal in Brave)

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.

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

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

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)

Cites Work

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

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)