Affiliations: National Research University Higher School of Economics, 3 Kochnovsky Proezd, 125319 Moscow, Russia. valdus@yandex.ru
Correspondence:
[*]
Support from the Basic Research Program of the National Research University Higher School of Economics is gratefully acknowledged. Address for correspondence: National Research University Higher School of Economics, 3 Kochnovsky Proezd, 125319 Moscow, Russia
Abstract: 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 ab and ba lead to the same result. A statement b is (left-)absorptive for a statement a, if the execution of sequences ab 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.
Keywords: program models, equivalence checking, semigroups, commutativity, left absorption
