An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements

For many program analysis problems it is useful to have means to efficiently prove that given programs have similar (equivalent) behaviors. Unfortunately, in most cases to prove the behavioral equivalence is an undecidable problem. A common way to overcome such undecidability is to consider a model of programs with an abstract semantics based on the real one, in which only some simple properties are captured, and to provide an efficient equivalence-checking algorithm for the model. We focus on two kinds of properties of data-modifying statements of imperative programs. Statements a and b are commutative, if the execution of sequences a b and b a lead to the same result. A statement b is (left-) absorptive for a statement a, if the execution of sequences a b and b lead to the same result. We consider propositional program models in which commutativity and absorption properties are caprtured (CA-models). Formally, data states for a CA-model are elements of a monoid over the set of statement symbols, defined by an arbitrary set of relations of the form ab = ba (for commutativity) and ab = b (for absorption). We propose an equivalence-checking algorithm for CA-models based on (what we call) progressive monoids. The algorithm terminates in time polynomial in size of programs. As a consequence, we prove a polynomial-time decidability for the equivalence problem in such CA-models.