Ranko Lazic and Bill Roscoe April 1998, 21pp.
Our main result says that determinism of a concurrent system which uses unbounded arrays (i.e. memories) can be verified by considering an appropriate finite array size.
That is made possible by restricting the ways in which array indices and values can be used within the system. The restrictions are those of data independence: the system must not perform any operations on the indices and values, but it is only allowed to input them, store them, and output them. Equality tests between indices are also allowed.
The restrictions are satisfied by many concurrent systems which use arrays to model memories or databases. As a case study, we have vertified that a database system which allows users to lock, and write records at multiple security levels is secure.