带时钟的分布式对象的定时演算

### 带时钟的分布式对象的定时演算 #### 1. 引言 分布式系统由多个通过具有固有延迟的通信网络松散耦合的处理器组成。并发面向对象计算的概念被认为是设计和开发分布式系统的有力手段，因为对象是通过消息传递相互交互的逻辑自包含的活动实体。近年来，基于这一概念开发了许多用于分布式系统的编程语言。 通信延迟是分布式系统最显著的特征，它使得对象无法在所有处理器之间共享全局时钟。许多分布式系统需要实时功能来管理时间关键的响应以及与现实世界的交互，这些功能必须由本地处理器上的时钟来实现，而不是共享的全局时钟。然而，这些时钟的运行速率永远不可能相同，时钟之间不可忽略的相对差异可能导致本地处理器之间的协作失败。因此，我们需要一个理论模型来描述和分析分布式面向对象计算的本地时间属性和功能行为属性。 目前已经提出了许多基于时态逻辑、自动机和进程演算的计算模型来描述和验证分布式系统，但大多数模型只能对分布式计算的行为方面进行建模，缺乏表示时间属性的能力；其他模型则只能基于全局时间来管理时间属性，而全局时间在分布式系统中本质上是无法实现的，因此它们无法对分布式系统中的本地时间概念进行建模。 本文的目标是开发一种形式化方法，用于推理分布式面向对象计算，特别是计算中的本地时间属性。该形式化方法基于现有的进程演算 CCS，因为 CCS 具有强大的表达能力，可以轻松地对并发对象的许多特征进行建模。但 CCS 本质上缺乏本地时间的概念，因此需要对其进行扩展。作者之前曾引入了一种名为 RtCCS 的定时扩展进程演算，用于实时并发（但非分布式）面向对象计算，但 RtCCS 基于全局时间，无法表示分布式系统中的本地时间概念。在本文中，我们通过将 CCS 扩展为具有本地时间概念，开发了一种名为 DtCCS（分布式定时通信系统演算）的进程演算，以便明确描述和分析分布式面向对象计算中基于本地时间的时间属性和行为属性，并在此基础上开发分布式对象的理论证明技术。 #### 2. 基本框架 ##### 2.1 分布式计算中的时间 在介绍我们的形式化方法之前，我们先介绍对本地时间进行建模的基本思想。如果所有处理器的相对运动可以忽略不计，根据爱因斯坦的相对论，每个处理器中物理时间的流逝速率是相同的。但每个本地时钟以自己的速率运行，时钟速率彼此不同，并且这些速率可能在一定范围内变化。因此，我们可以将本地时钟设想为：每个实际的本地时钟根据自己的测量速率将全局时间的流逝转换为自己的时间坐标，从而读取自己的当前时间。所以，尽管时钟共享相同的全局时间，但由不同时钟测量的本地时间可能彼此不同。总结以上讨论，我们给出分布式计算中关于时间的两个基本假设： 1. 分布式系统中的所有处理器共享概念上的全局时间。 2. 每个处理器的本地时钟根据自己的时间单位和精度来测量全局时间。 我们将以给定恒定速率运行的时钟称为恒定时钟，将以在给定范围内动态漂移的速率运行的时钟称为可变时钟。 ##### 2.2 CCS 的扩展 根据上述假设，我们使用基于 CCS 的语言开发了一种形式化方法，用于推理分布式对象的行为和时间属性。为了表示分布式系统的时间属性，我们需要扩展 CCS，使其具有表示分布式系统中本地时间属性的能力。为此，我们引入了三个时间原语：定时行为、全局时间和本地时钟，具体如下： - **定时行为**：分布式系统的行为依赖于时间的流逝，如延迟处理和超时处理。在分布式系统中，超时处理是通信网络和其他处理器中故障检测的关键部分。因此，我们引入了一个具有超时处理语义的特殊二元运算符，记为 `( , )t`，称为超时运算符。例如，`(P, Q)t` 在 `P` 能在 `t` 个时间单位内执行初始转换时表现为 `P`，在 `P` 在 `t` 个时间单位内未执行任何动作时表现为 `Q`。 - **全局时间**：我们假设所有处理器共享概念上的全局时间，全局时间的流逝表示为一个特殊动作，这是一个对所有对象的同步广播消息，对应于全局时间一个单位的流逝，记为 `d`，称为滴答动作。需要注意的是，在我们的形式化方法中，全局时间的存在并不意味着存在实际的全局时钟，它只是提供了每个本地时钟可以测量的时间。 - **本地时钟**：本地时钟是从本地时间的时间点到全局时间中对应时间点的特殊映射，根据其自身的时间单位和精度定义。该映射定义了本地时间中一个时间单位的长度对应于全局时间中的多少个时间点。反之，每个处理器上的本地时间是可以通过该映射转换为全局时间的所有时间点的集合。为了表示可变时钟，时钟可以表示为非确定性映射。 在我们的形式化方法中，关于本地时间的对象描述被转换为全局时间的描述，并仅基于全局时间进行解释。这样，我们获得了一种统一的方法来轻松分析具有各自本地时间的分布式对象，并且可以使用许多基于全局时间的定时进程演算的良好属性，包括之前提出的 RtCCS 的证明技术。 #### 3. 定义 ##### 3.1 时间域 在我们的形式化方法中，时间表示为一个由时间点组成的时间域。一个时间点表示从初始时间开始的一个时间间隔，我们将时间点限制为离散的，而不是连续的。每个时间域对应于一个本地时钟测量的本地时间，我们假设存在一个特殊的时间域，它是所有本地时间的最精细和绝对的参考时间基础，称为全局时间域。 定义 3.1：设 `T` 表示包含 0 的正整数集合，即 `T = N ∪ {0}`，其中 `N` 是自然数集合，我们称 `T` 为一个时间域。特别地，全局时间域表示为 `TG`。 所有本地时间域上的任何时间点的出现都对应于全局时间域中的时间点，本地时间域和全局时间域之间的联系由以下映射给出。 定义 3.2：设 `z` 是一个本地时间域，`6,in` 和 `6,maz` 属于 `TG`，且 `0 < 6,in ≤ 6,maz`，时钟映射 `θ : z → TG` 定义如下： \[ \theta(t) = \begin{cases} 0, & \text{if } t = 0 \\ \theta(t - 1) + \delta, & \text{if } t > 0 \end{cases} \] 其中 `δ ∈ {δ ∈ TG | 6,in ≤ δ ≤ 6,maz}`。我们称 `θ` 为时钟映射，或简称为时钟。我们用 `{θ(t)}` 表示 `{tG | ∀tG ∈ TG : tG = θ(t)}`。特别地，如果 `6,in = 6,maz`，我们称 `θ` 为恒定时钟，此后有时会将 `θ(t)` 简记为 `θ(t) ≈ δt`。 在上述定义中，`δ` 对应于根据全局时间域，本地时间域上一个时间单位的间隔