Fairness, Resources, and Separation

AbstractFair interleaving plays a fundamental rôle in denotational semantic models for shared-memory parallel programs, beginning with Park's trace semantics, based on a fairmerge relation designed so that (α,β,γ)∈fairmerge if and only if γ can be obtained by interleaving α and β. Park's formulation of fairmerge used nested greatest and least fixed points of monotone functions over traces, but he remarked that fixed point induction principles seem unsuitable for proving natural algebraic properties such as associativity. Such properties are needed to validate intuitive laws of program equivalence and to support hierarchical analysis of programs. Recent models and logics for shared-memory programs with mutable state and pointers build on and extend Park's foundations, with emphasis on resources and logical rules that embody separation principles. For example, concurrent separation logic is based on a race-detecting, resource-sensitive variant of fairmerge. For the kinds of interleaving employed in these models, and other more sophisticated variants of fairmerge, the algebraic difficulties are exacerbated. Rather than search for ad hoc techniques, we develop here a general framework for defining k-ary fairmerge operators, parameterized first by a choice of a resource model and then refined by a choice of a conflict or interference relation. Our formulation avoids nested fixed points, and supports inductive reasoning based on the length of finite prefixes of a trace. We prove a generalized associativity property, and obtain associativity proofs for prior models as a by-product