Intensional and Extensional Characterisation of Global Progress in the Pi-Calculus

Luca Fossati

We introduce an observational theory of a linear pi-calculus for a rigorous behavioural characterisation of global progress properties such as non-blockingness and wait-freedom. On the basis of typed asynchronous transitions, we introduce a general framework to capture global progress through a combination of fair transitions and partial failures, the latter to represent stalling activities in a fair transition sequence, and show how we can rigorously capture representative global progress properties such as non-blockingness and wait-freedom, both extensionally and intensionally. The intensional characterisations offer a faithful formalisation of the intuitive notions, while the extensional characterisations offer their counterpart capturing a wider class of properties solely based on external observables independent from internal implementations. We introduce a fairness-enriched bisimilarity which preserves these progress properties and which is a congruence, and demonstrate its usage through semantic characterisation and separation results for some of the representative concurrent data structures.