Efficient recognition of trace languages defined by repeat-until loops

A sequence of operations may be validly reordered, provided that only pairs of independent operations are commuted. Focusing on a program scheme, idealized as a local finite automaton, we consider the problem of checking whether a given string is a valid permutation of a word recognized by the automaton. Within the framework of trace theory, this is the word membership problem for rational trace languages. Existing general algorithms, although time-polynomial, have unbounded degree related to some properties of the dependence graph. Here we present two original linear-time solutions. A straightforward algorithm is suitable for any local finite automaton such that any two successors of an operation are dependent or not mutually reachable. The second approach is currently restricted to nested repeat-until loops. Using integer compositions to represent loop iterations, the algorithm constructs the loop nesting syntax tree by exploiting newly introduced functions on integer compositions. The result may be relevant for checking dependencies of rescheduled programs on parallel processors.