Quantifiability: a concurrent correctness condition modeled in vector space

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 that 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 that quantifiability is compositional and non-blocking and that it implies observational refinement. Analysis is facilitated with linear algebra, better supported and of much more efficient time complexity than traditional combinatorial methods.