Efficient algorithms for checking the equivalence of programs in interrupt handling models

The problem of equivalence of interrupt handling programs in two algebraic models is studied. Program operators are divided into two classes, namely, the classes of basic operators and interrupt handling operators. The first model obeys the absorption law, i. e., each basic operator suppresses the result of application of any interrupt handling operator. This means that, if the interrupt handling is successfully finished and the control is passed to basic operators, then the result of interrupt handling has no influence on the program output. An algorithm that solves the problem of equivalence in the above model in O(n 2log n) operations is suggested. The other model obeys the absorption law and satisfies the commutative property for basic operators. For this model, we also propose an algorithm that checks the equivalence of programs in O(n 4log n) operations. © 2008 Allerton Press, Inc.