Model checking data-independent systems with arrays

We say a program is data-independent with respect to a data type X if the operations it can perform on values of type X are restricted to just equality testing, although the system may also input, store and move around (via assignment) values of type X within its variables. This property can be exploited to give procedures for the automatic verification, called model checking, of such programs independently of the instance for the type X. This thesis considers data-independent programs with arrays, which are useful for modelling memory systems such as cache protocols. The main question of interest is the following parameterised model-checking problem: whether a program satisfies its specification for all non-empty finite instances of its types. In order to obtain these results, we present a UNITY-like programming language with arrays that is suited to the study of decidability of various modelchecking problems, whilst being useful for prototyping memory systems such as caches. Its semantics are given in terms of transition systems, and we use the modal μ-calculus, a branching-time temporal logic with recursion, as our specification language. We describe a model-checking procedure for programs that use arrays indexed by one data-independent type X and storing values from another Y. This allows us to prove properties about parameterised systems: for example, that memory systems can be verified independently of memory size and data values. This decidability result is shown to extend to data-independent programs with many types and multidimensional arrays which are acyclic, meaning it is not possible to form loops of types in the 'indexed by' relation. Conversely, it is shown that even reachability model-checking problems are undecidable for classes of programs that allow cyclic-array programs. We give practical motivation for these decidability results by demonstrating how one could verify a fault-tolerant interface on a set of unreliable memories, and the cache protocol in the Pentium Pro processor. Significantly, the verifications are performed independently of many of these systems' parameters. These case studies suggest two extensions to the language: an array reset instruction, which sets every element of an array to a particular value, and an array assignment or copy instruction. Both are shown to restrict decidability of model checking problems; however we can obtain some interesting decidability results for arrays with reset by restricting the number of arrays to just one, or by allowing the arrays only to store fixed finite types, such as the booleans.