Algebraic Reasoning About Timeliness

Designing distributed systems to have predictable performance under high load is difficult because of resource exhaustion, non-linearity, and stochastic behaviour. Timeliness, i.e., delivering results within the required time bounds, makes a major contribution to the predictability of performance. In this paper, we focus on timeliness using the ΔQ Systems Development paradigm (ΔQSD, developed by PNSol), which computes timeliness by modelling systems observationally using so-called outcome expressions. An outcome expression is a compositional definition of a system’s observed behaviour in terms of its basic operations. Given the stochastic behaviour of the basic operations, ΔQSD efficiently computes the stochastic behaviour of the whole system including its timeliness.

This paper formally proves useful algebraic properties of outcome expressions w.r.t. timeliness: We prove the different algebraic structures the set of outcome expressions form with the different ΔQSD operators and demonstrate why those operators do not form richer structures. We prove or disprove the set of all possible distributivity results on outcome expressions. We prove 14 equivalences that have been used in the past in the practice of ΔQSD.

An immediate benefit is rewrite rules that can be used for design exploration under established timeliness equivalence. This work is part of an ongoing project to disseminate and build tool support for ΔQSD. The ability to rewrite outcome expressions is essential for efficient tool support.