Fairness for Non-Interleaving Concurrency

Fairness in a non-interleaving semantic model for concurrency has been investigated. In contrast to the interleaving approach, which reduces non-sequential behaviours to a nondeterministic choice between possible interleavings of activities of concurrent processes, concurrency and causality were assumed as primitive notions. Mazurkiewicz's trace languages were chosen as behavioural representations of systems and Shields' asynchronous transition systems as their acceptors. The notion central to these two formalisms is one of causal independency, which determines trace equivalence (congruence) in the monoid of strings. Equivalence classes of strings are called traces. The quotient monoid of traces forms a poset with trace prefix ordering. First, trace languages have been enhanced to allow for infmite traces; this was achieved by introducing trace preorder relation on possibly infinite strings. It has been shown that the extension gives rise to the domain of traces and an infinitary monoid, which specializes to the domain and the infinitary monoid of strings of Nivat's, Asynchronous transition systems have been equipped with a notion of a process structure; a variety of process structures ordered by refinement relation are possible for a given system. Each process structure determines projective preorder and equivalence relations in the monoid of strings, which are shown to coincide with the trace preorder and trace equivalence. In this setting, a topological characterization of behavioural properties which includes safety, progress and fairness properties has been provided. Fairness properties form a subclass of infinitary progress properties that is closed under arbitrary union. Unconditional process fairness properties that are determined by process structures have been distinguished; they form a lattice with inclusion ordering. Finally, strength predicates were incorporated to allow for a variety of specific fairness properties such as weak and strong process fairness as well as equifairness and state fairness