Concurrent Correctness in Vector Space

Correctness verification of a concurrent history is challenging and has been proven to be an NP-complete problem. The reason that verifying correctness cannot be solved in polynomial time is a consequence of the way correctness is defined. Traditional correctness conditions require a concurrent history to be equivalent to a legal sequential history. The worst case number of legal sequential histories for a concurrent history is O(n!) with respect to n methods invoked. Existing correctness verification tools improve the time complexity by either reducing the size of the possible legal sequential histories or improving the efficiency of generating the possible legal sequential histories. Further improvements to the time complexity of correctness verification can be achieved by changing the way correctness of concurrent programs is defined. In this paper, we present the first methodology to recast the correctness conditions in literature to be defined in vector space. The concurrent histories are represented as a set of method call vectors, and correctness is defined as properties over the set of vectors. The challenge with defining correctness in vector space is accounting for method call ordering and data structure semantics. We solve this challenge by incorporating a priority assignment scheme to the values of the method call vectors. Using our new definitions of concurrent correctness, we design a dynamic analysis tool that checks the vector space correctness of concurrent data structures in \(O(n^2)\) with respect to n method calls, a significant improvement over O(n!) time required to analyze legal sequential histories. We showcase our dynamic analysis tool by using it to check the vector space correctness of a variety of queues, stacks, and hashmaps.