SpaceWire-D的调度表生成方法

姜宏，杨孟飞，刘波，* ，刘鸿瑾，龚健

1.北京控制工程研究所，北京 100190

2.中国空间技术研究院，北京 100094

随着国内外航天技术的快速发展，航天电子系统的复杂度不断增大，对数据总线、网络的传输速率和实时性提出了更高的要求。传统的1553B［1］、TTCAN 等航天总线，虽然具有较好的时间确定性，但是传输速率低;而 SpaceWire［2］、以太网、FC等网络技术，虽然传输速率高，但是实时性较差。SpaceWire-D［3］是由英国邓迪大学(Dundee University)的ESA空间技术中心(Space Technology Centre)设计的，是针对标准SpaceWire的时间确定性扩展协议。SpaceWire-D使用标准SpaceWire的远程存储器访问协议(Remote Memory Access Protocol，RMAP)提供基本的通信机制。为了确保数据传输的时间确定性，网络带宽被划分为一系列的时间槽(time slots)，然后网络通信的所有发起者(initiator)按照一定的调度表在规定的时间槽内发送一组事务(transaction)。由于每个发起者都是独占时间槽，不会与其他发起者产生竞争网络资源的冲突，从而避免了资源竞争导致的不确定性传输时延，提高了实时性。

调度表生成的核心是调度［4-5］问题，目前主流的设计方法基于SMT(Satisfiability Modulo Theory，可满足性模理论)求解器(SMT-Solver)。其中，TTTech公司的调度表生成技术［6］最为成熟。该公司采用内嵌SRI(斯坦福国际研究所)开发的SMT求解器Yices［7］推出了商业化调度工具 TTE-Plan，可应用于时间触发以太网(TTEthernet)。德国慕尼黑大学的静态调度方法基于Z3 SMT求解器［8］，用于时间触发片上网络(TTNoC)。澳大利亚IST的时间触发调度方法［9］同样基于Z3 SMT求解器，用于失效链路的交换网络，但是流量模型较简单，不能用于实际航天网络系统。另外，还有一些不依赖于SMT求解器的方法［10-11］，但是这些方法针对的也是TTEthernet网络，并且网络和调度模型不够明确。

综上，SpaceWire-D是一种实时、可靠的航天网络技术，但是现有文献没有针对高速SpaceWire-D调度表生成的有效方法，本文的研究工作根据高速SpaceWire-D网络的特点将贪婪算法与SMT方法相结合，使得生成的调度表具有良好的分布均匀性且生成速度较快，弥补了现有方法的不足。

1 网络模型

SpaceWire-D的底层基础是 SpaceWire网络。一个SpaceWire网络系统通常由路由器、终端节点和链路构成。高速SpaceWire网络将标准SpaceWire的传输介质变为光纤，并对路由器和节点的设计做了改进，使网络速率明显高于传统 SpaceWire 的 200 Mbit/s［12］。本文采用高速SpaceWire网络，最大数据传输率为1Gbit/s，并包含3个路由器和16个终端节点，如图1所示。

图1 高速SpaceWire网络模型Fig.1 Network model of high-speed SpaceWire

图1中的3个路由器用R1、R2和R3表示，16个终端节点用N1，N2，…，N16表示。节点和路由器之间通过全双工链路连接，可同时进行数据收发，链路由 L1，L1'，…，L18，L18'表示。SpaceWire路由器的各个端口通过Crossbar交换阵列进行互联。通常认为Crossbar的内部是无阻塞的，因此只要输出端口不同就不会发生竞争冲突。

2 传输帧模型

在高速SpaceWire网络系统中，由任意节点Vi(1≤i≤M，M为节点个数)发起的到达任意节点Vj(1≤j≤M)的一个周期性传输帧Fij可被描述为一个四元组 M=( αij，βij，γij，δij)。其中，αij为传输的周期，βij为周期偏移值，γij为传输占用时间，δij为传输链路信息。

αij和βij用于描述帧的周期特性，都以时间槽T为单位。αij的取值通常为小周期的整数倍。βij的取值范围是0～N－1，N为大周期包含的时间槽个数。小周期(基本周期)等于所有帧周期的最大公约数，大周期(矩阵周期)等于所有帧周期的最小公倍数［13］(如图2所示)。

γij描述的是某个帧所占据的调度表的时间长度。该值有可能取得较大值，甚至会超过小周期，此时需要将长帧拆分成多个短帧。在图2中，C帧的传输时间为6，大于小周期长度5，于是被拆分成C1、C2和C3。长帧的拆分使调度表的设计既具有较大的灵活性，同时也增加了难度，当终端节点数量较多时很难由手工完成。

δij用于记录从Vi到Vj经过的所有链路组成的集合，例如:V1到V12经过的链路集为{L1，L6，L12，L14'}。当网络系统中的两个链路集的交为空集时，它们之间不存在公共链路，从而不会发生因竞争链路发送权而导致的冲突。反之，两个链路集有公共链路，从而存在竞争冲突，此时称这两个链路集处于同一个竞争区域(Competition Area，CA)内。

3 约束条件

由于SMT求解器在理论上已经比较完善，并且在工程上也有了较好的应用，因此本文基于SMT求解器开展研究工作。在调用SMT求解器前，需要先根据高速SpaceWire网络的特点设定好关于自由变量βij的约束集。

3.1 调度周期约束

每个周期性传输帧Fij都有其传输周期αij。如果一个大周期包含多个Fij周期，即:(N/αij)=K，K＞1，则在调度表中会有多个Fij的周期偏移值，记为 βij1，βij2，…，βijK，表示Fij帧头部开始传输时的时间槽。βij1，βij2，…，βijK应符合如下的周期约束:

式(1)表明:Fij在调度表中应按固定周期排列，相邻两个周期的偏移值之差应恰好为αij。

3.2 顺序约束

当Fij为占用多个时间槽传输的长帧时，要将Fij拆分为短帧(本文称之为分片)处理，当Fij只占用1个时间槽时则无需分片，因此下文按两种情况讨论顺序约束。

3.2.1 不分片的情况

当帧Fij在调度表中只出现一次时，显然其起始位置应不小于0，结束位置应不大于N，即:

当帧Fij在调度表中多次出现时，其多个周期偏移值满足下式所示的约束条件:

3.2.2 分片的情况

(1)对分片先后顺序的约束

Fij的各个分片具有固定的先后顺序关系，若Fij在调度表中只出现1次，则可表示为如下的约束:

式中:(βij)s+1为帧Fij第s+1个分片在调度表的起始位置;(βij)s为帧Fij第s个分片在调度表的起始位置，1≤s＜S，S为Fij在一个周期内的分片个数;(γij)s为第s个分片占用的时间槽个数。

若帧Fij在调度表中多次出现，则应满足的约束条件为:

式中:(βrij)s+1为在调度表中，Fij第r次被调度时，第s+1个分片的起始位置;第r次被调度时，第s个分片的起始位置。

式(4)和(5)表明:Fij的两个相邻分片在调度表中的起始位置的距离不小于前一个分片占用的时间槽个数。

(2)对首分片和尾分片的约束

当Fij在调度表中只出现1次时，该帧第一个分片(首分片)和最后一个分片(尾分片)的位置应在如下约束规定的范围内。

当Fij在一个大周期内被调度K次时，该帧第一次被调度时的首分片和第K次被调度时的尾分片的位置应符合下式规定。

式(6)和(7)表明:所有帧的所有分片的起始位置应不小于0，且结束位置应不大于N。

3．3 链路约束

Fij的链路信息δij有助于将整个网络系统划分为多个竞争区(CA)。当根据链路信息发现多个帧处于相同的CA时，必须保证它们之间不会在同一时刻传输数据。根据这一原则，并结合Fij在一个大周期内是否被分片，设定如下的链路约束。

(1)Fij不分片

当帧Fij在调度表中只出现一次时，约束条件为:

式中:βuv为任意帧Fuv在调度表中的偏移值;γuv为该帧占用时间槽的个数，这是Fuv被调度一次，且不分片的情况为任意帧Fuv被调度多次时，第r次出现在调度表中的偏移值，γuv仍然是该帧的传输时间;为任意帧Fuv被调度多次且分片，第s个分片第r次出现时所处的偏移位置，(γuv)s为第s个分片的传输时间。

当任意帧Fij在调度表中多次出现时，约束条件为:

式(9)中的各变量含义同式(8)，只是为了区分，将βij和βuv的上标分别写成r1和r2。

(2)Fij被分片

当帧Fij在调度表中只出现一次时，约束条件为:

当帧Fij在调度表中多次出现时，约束条件如下:

式(10)和式(11)中各变量含义与式(8)和式(9)相同，上下标的差异是为了变量的区分。

式(8)～式(11)表明:对于任意的两个帧Fij和Fuv(δij≠δuv)，当二者处于同一个 CA 中时，不论在调度表中出现几次，也不论是否被分片，占用的时间槽都不能发生重叠，即调度区间的交集为空。

4 基于SMT的调度表生成方法

由上文可知，对任意帧进行分片为调度表的生成带来了较大的复杂性，而SMT求解器内部并不能自主完成对长帧的分片，只能针对已分好片的各个帧及约束条件计算出可满足性，当可满足时再给出每个帧或帧的分片在调度表中的偏移值，具体的分片方案需要由外部提供。

本文的调度表生成方法在处理分片问题时基于以下分片原则:同一个帧的各个分片应均匀分布于调度表的大周期。上述原则使得网络流量尽量均匀，传输过程更加平顺，有利于降低数据传输过程中存储区的数据存取压力。为实现均匀分片，使生成的调度表在确保可调度的前提下的分布均匀性达到最优，本文设计了基于贪婪(greedy)算法［14］的全局优化方法。该算法的设计思想是:首先按分布最均匀的情况对各个帧进行分片并设置约束，然后将约束条件作为参数输入给SMT求解器进行可满足性检查。若检查的结果为可满足，则SMT求解器输出的模型即为所求最优解，否则将分布均匀条件放松，重新分片并更新约束条件再输送给SMT求解器。这一过程迭代执行，直到得到最终的结果。

4.1 算法描述

具体实现算法如图3所示，共分6个步骤:步骤1:预处理，根据链路信息划分冲突域，计算小周期、大周期和时间槽长度，并确定各个帧的分片长度，然后转入步骤2。

图3 全局优化算法Fig.3 Algorithm of global optimization

步骤2:按各个分片均匀分布的情况设置约束并调用SMT求解器，若计算结果为可满足，则执行步骤5，否则执行步骤3。

步骤3:对于每个帧，从第1个小周期开始，依次移动1个、2个、…、δ(δ为某个帧的帧周期包含的小周期个数)个分片到其他小周期，再设置约束并调用SMT求解器，检查可满足性，若可满足则执行步骤5，否则执行步骤4。

步骤4:对于所有帧，当帧周期的每个小周期都已尝试过分片移动，但仍未找到可满足的解，则执行步骤6，若还有帧或帧的小周期未开展分片移动，则回到步骤3。

步骤5:返回的模型即为最优解。

步骤6:未找到可满足的解，当前条件无法生成调度表。

4.2 算法说明

(1)SMT求解器的输入和输出

SMT求解器的输入参数通常为一系列断言式［15］组成的约束条件集合。根据这些约束条件，SMT求解器能够做出可满足性判定。如果可满足，则输出的模型即为使所有断言式都成立的解。

对于调度表生成算法，如果输出为可满足(执行到步骤5)，说明算法成功找到了一组关于所有帧和帧的分片在调度表中的偏移值;如果输出为不可满足(执行到步骤6)，说明在同一个CA中的所有帧或帧的分片无法不重叠地出现在调度表中，即该CA中的帧的集合是不可调度的。

(2)设置时间槽大小

时间槽大小的一种较简便计算方法是取所有帧传输时间的最大值(也被称为光栅)［16］，但是这种设定方法不利于网络流量的均匀分布。本文的方法是:

1)首先根据高速SpaceWire网络的数据传输率，计算每个帧的传输时间并以微秒(μs)为单位向上取整，然后计算取整后的所有传输时间的最大公约数T1;

2)取T1与小周期长度的最大公约数，即为最终的时间槽大小T。

(3)分片准则

本文根据帧的传输周期采取如下策略确定是否分片，及分片的长度:

1)若帧的调度周期等于小周期，则该帧不需要被分片;

2)不满足1)的所有帧，分片长度都等于1个时间槽。

(4)划分冲突域

根据链路信息划分冲突域，比较各个帧的链路集合。如果两个帧有相同的链路存在，则这两个帧同处于一个CA，否则处于不同的CA。当所有帧的链路信息都比较后，冲突域划分完毕。

5 试验条件和结果

5．1 试验条件

本文采用斯坦福的开源SMT求解器Yices开展试验。试验的硬件平台是联想ThinkCentre PC机，处理器主频2.66 GHz，内存为2 Gbyte。软件开发环境是Visual Studio 2010，采用C++语言实现算法。

试验条件根据高速SpaceWire网络的1Gbit/s数据传输率和图1所示的拓扑结构进行了设置。

待调度的帧一共有16个，这些帧的信息如表1所示。

表1 各个帧的相关信息Table 1 Related information of all frames

续表1Table 1 Continued

5.2 试验结果

根据表1中各个帧的信息、图1的网络拓扑结构以及1Gbit/s的数据传输率执行本文算法，共试验了20次，每次的运行时间见表2。

表2 算法的运行时间Table 2 Running time of the algorithm

上述试验数据中，最大运行时间为268 ms，最小运行时间为 187 ms，平均运行时间为201.65ms。

虽然多次运行的时间有所差异，但是每次试验生成的调度表是一致的，具体见图4。

图4的结果共展示了4个冲突域的帧的调度情况。CA1包含帧A、B、C、D;CA2包含帧D、E、F、G;CA3 包含帧 H、I、J、K;CA4 包含帧 L、M、N、O、P。

在 CA1 中，C 帧被拆分为 Ca、Cb、Cc、Cd共 4个分片;D帧被拆分为 Da、Db、Dc共3个分片。CA1和CA2中都有D帧，这是因为D帧与这两个冲突域中的帧都存在链路竞争。在CA3和CA4中，I帧、K帧、N帧和P帧都被拆分为两个分片。

图4 调度表生成结果Fig.4 Generated schedule

观察图4可发现，全部16个帧和分片在调度表大周期的分布比较均匀，因此获得了很好的效果。

6 结束语

针对高速SpaceWire-D提出了一种调度表生成方法。该方法基于SMT求解器并结合贪婪算法。贪婪算法是本文方法的主体，用于将帧的分片在各个小周期进行调整，使各分片在调度表上尽量均匀分布。SMT求解器是本文方法的重要工具，在算法中设定了关于调度表的调度周期约束、顺序约束和链路约束，并作为SMT求解器的输入参数，然后调用求解器对输入参数的可满足性进行判定，如果可满足则返回的模型即为所求的调度表。此外，本文还提出了设置分片长度、确定时间槽大小以及划分冲突域的策略，使整个方法可以完整实现。在试验部分，使用本文方法生成了一组帧的调度表，结果验证了该方法的有效性，适用于航天高速SpaceWire-D网络。本文方法目前应用范围有限，后续需要针对更多应用案例进行验证，并且为应对大规模的调度表生成问题，在未来的工作中还将改进分片策略，以进一步缩短算法的收敛时间。