TR-IIS-02-010    PDF format

Pointer is a very convenient device for constructing dynamic networks and passing parameters in complex software. But with bugs like dirty pointers, it also creates challenges in maintaining system functionality. We formally define the model of software with pointer data structures. Model checking such software may cost tremendous resources because of the dynamic data structure. We developed symbolic algorithms for the manipulation of conditions and assignments with indirect operands for verification with BDD-like data-structures. We rely on two techniques, including inactive variable elimination and process-symmetry reduction in the network configuration, to contain the time and memory complexity. We argue for the indispensability of process-symmetry reduction in model-checking such systems and laid the theoretical groundwork for the discussion of symmetry reduction. We propose the efficient technique of IbSINC ( Incomplete but Sound Isomorphism of Network Configuration ) reduction to avoid the expensive but complete symmetry reduction. We then identify the anomaly of image false reachability of the IbSINC reduction and also define a useful class of symmetric systems, for which the efficient IbSINC reduction works well without the anomaly problem. We implemented the techniques in the RED tool and tested it against the Mellor-Crummy and Scottˇ¦s locking algorithms and several other benchmarks. The performance comparison with tool SMC shows that for the special class of pointer-data-structure concurrent systems, our technique can lead to significant performance improvement.

Keywords: symmetry, symbolic model-checking , pointers, data-structures