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 defined time bounds, is a central aspect of predictable performance. In this paper, we focus on timeliness using the DELTA-Q Systems Development paradigm (DELTA-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 behaviour of the basic operations, DELTA-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 DELTA-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. On our way for disproving 8 of those distributivity results, we develop a technique called properisation, which gives rise to the first body of maths for improper random variables. Finally, we also prove 14 equivalences that have been used in the past in the practice of DELTA-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 DELTA-QSD. The ability to rewrite outcome expressions is essential for efficient tool support.
翻译:设计在高负载下具有可预测性能的分布式系统因资源耗尽、非线性和随机行为而困难重重。时效性,即在规定时间范围内交付结果,是可预测性能的核心方面。本文聚焦于利用DELTA-Q系统开发范式(DELTA-QSD,由PNSol开发)实现的时效性,该范式通过观测性建模系统,采用所谓的结果表达式来计算时效性。结果表达式是基于基本操作对系统观测行为的组合式定义。给定基本操作的行为后,DELTA-QSD能高效计算整个系统的随机行为,包括其时序特性。本文正式证明了结果表达式在时效性方面的有用代数性质。我们证明了结果表达式集合与不同DELTA-QSD算子构成的多种代数结构,并论证了为何这些算子无法形成更丰富的结构。我们证明或否定了结果表达式上所有可能的分配律结果。在否定其中8个分配律结果的过程中,我们开发了一种称为"适正化"的技术,这为非适当随机变量奠定了首个数学基础。最后,我们还证明了DELTA-QSD实践中曾使用的14个等价关系。其直接益处是可在已建立的时效性等价关系下用于设计探索的重写规则。本研究是正在进行的DELTA-QSD推广与工具支持构建项目的一部分。重写结果表达式的能力对于高效工具支持至关重要。