Verification of Work-stealing Deque Implementation

Abstract: Software verification is the process of checking a software system to make sure it meets its specifications. A software system can be either of sequential or concurrent type. The most important part in a sequential system from the verification point of view is the relationship between the system’s inputs and outputs. More formally, verification of a sequential system can be expressed in the following form: If a program starts in a specific state which satisfies a certain condition(precondition), then it eventually terminates and the program variables at the final state satisfy some given relation with the corresponding values at the beginning of the execution [20]. But the story in verification of concurrent software is different. Many concurrent software use parallelism in order to make calculations more efficient. Parallelism is used to distribute a large amount of computations between different processing units to finish them in a shorter time. Input and output values are still enough for specifying the behavior of these sequential processes but are absolutely not enough for specifying the behaviors of the concurrent system. This is mainly because of the interactions between processes which can not only be expressed with the help of inputs and outputs. One important aspect in verification of concurrent programs is to directly verify them against an abstract specification of overall functionality. For example, a concurrent implementation of a familiar data type abstraction, such as a queue, could be verified to conform to a simple abstract specification of such a data type. This has been accomplished for finite-state programs and some verification tools like SPIN [3, 13] are already supporting it, but to our knowledge there are no approaches for handling unbounded data domains in specifications and implementations as is the case for a work-stealing double ended queue(deque) implementation. In this project we present a technique for automatically verifying that a concurrent workstealing deque conforms to an abstract specification of its functionality and we mathematically prove our technique's correctness. We also demonstrate its use by applying it to a famous implementation of a work-stealing deque data structure presented by Arora, et al. [2]