Framework for Analyzing Highly Concurrent Algorithms in SPIN

Abstract: Human beings have gradually become dependent on computers, and more specifically, the software that they are working with. Most skillful programmers are working hard and spend much time testing or debugging their programs in order to make their software reliable. Verification techniques have been developed to find bugs as much as possible in the early stages of development or implementation of the software. Model checking is one of the verification techniques which requires a simplified model of the system. It will test automatically whether this model accommodates the given system’s specification or not. One of the most successful tools for automatic verification is the SPIN Model Checker. It is a general tool for verifying the correctness of distributed software models, parallel algorithms and data structures. The input language of SPIN is Promela. Promela does not support some features such as pointer declarations, dynamic memory allocation, or garbage collection in order to be a simple modeling language and decrease the size of the state space. This master thesis presents a framework in Promela for verifying safety and liveness properties of highly concurrent algorithms in the SPIN model checker. We present some macros in Promela which are independent from the specific behavior of a particular algorithm. These macros can be used in most concurrent algorithms which are verified by SPIN. In this work also we used some techniques for memory management. Some macros are created which do garbage collection and dynamic memory allocation themselves in our framework in a way that the behavior of the original algorithm is preserved maximally. We have applied our approach to some concurrent deque algorithms and evaluated the results.