Calculating Preconditions for Parallel Workflows

We study the problems of race condition and process synchronization, commonly found in concurrent programming, in the context of information systems. These systems hold large quantities of business data constrained by complex structural and semantic rules. We assume that operations are equipped with guards against any violation of the data integrity, and that workflows (i.e. complex patterns of interactions) operate upon a shared, sequential data component. Updates via parallel workflows, through interleaving their operations, may lead to a state where the integrity is maintained but a goal property is not satisfied. Given workflows to be run in parallel, we calculate a precondition for establishing a state property upon their termination. Our calculation is efficient, using dynamic programming, and is based on the weakest precondition semantics of individual operations, we prove its correctness via a structural induction on the data structure: a 2-dimensional matrix.