2. 北京神州航天软件技术有限公司, 北京 100094
MPSoC已广泛用于通信、消费类电子产品等领域, 其体系结构更为复杂。如何进行可调度性分析, 使之既能控制分析的成本, 又能保证结果的准确性, 已成为MPSoC设计中迫切需要解决的问题。
传统可调度性分析方法可分为理论证明和模拟测试2类, 理论证明能保证结果的正确性, 但都过于保守[1]; 而模拟测试成本较高, 且不能保证结果的完备性。近几年的发展使模型检测方法提高了分析效率并可保证结果的完备性, 文献[2]对AADL模型用工具Cheddar进行了可调度性验证, 但结果不够精确; 文献[3]提出了分区调度系统的组件分析方法, 采用随机供应商时间自动机模拟资源的供给, 但没有对系统功耗建模。
本文针对MPSoC的任务抢占、任务依赖和处理器功耗等特性, 对其调度系统采用价格时间自动机建模, 在模型检测工具UPPAAL中, 估算任务不可调度的概率。
1 问题描述MPSoC由多种可编程处理器和专用处理器组成, 其体系结构如图 1所示。
|
| 图 1 MPSoC体系结构图 |
周期任务模型是实时任务模型的基础, 抽象层次较高, 适合作为MPSoC可调度性分析的任务模型。周期任务模型上的调度策略分为分组调度、全局调度等, 其中全局调度可以充分利用多个处理器, 更具有研究意义。故本文对全局FP调度的周期任务模型进行了可调度性分析, 即任务周期性触发, 具有固定优先级, 并可以在所有处理器间迁移。MPSoC模型设定如下:
1) 对数量为n的处理器, 用集合P={ρ1, ρ2, …, ρn}表示, 数量为m的任务用集合T={τ1, τ2, …, τm}表示;
2) 任务的计算量服从正态分布N(μ, σ2), 用二维数组calculation[m][2]存储, 其中calculation[j][0]、calculation[j][1]分别为任务τj(j≤m, τj∈T) 计算量的期望μj、方差σj2;
3) 处理器执行任务的速率用二维数组exeRate[n][m]存储, exeRate[i][j]表示处理器ρi(i≤n, ρi∈P) 执行任务τj的速率; 处理器执行任务的功率用二维数组dynPower[n][m]存储, dynPower[i][j]表示处理器ρi执行任务τj时的功率;
4) 任务间的依赖关系通过二维数组Dep[m][m]存储, Dep[j][j′]=1表示任务j依赖任务j′, 当所有被依赖任务执行完成以后, 该任务才能开始执行。
2 MPSoC价格时间自动机根据上面对MPSoC模型的描述, 本节在UPPAAL中构建MPSoC可调度性分析的价格时间自动机模型。
2.1 价格时间自动机理论价格时间自动机 (PTA) 是在时间自动机的基础上, 扩展价格元素的模型, 它的时钟可以在不同位置以不同速率增加, 能够描述不同任务的计算速率和处理器功率。
定义1 PTA定义为形如A=(L, l0, X, Σ, E, R, I) 的七元组, 其中:
1) L表示位置的集合;
2) l0(l0∈L) 为初始位置;
3) X表示时钟的集合, 时钟默认从0开始, 不断自增, 但可以在任意时刻被重新赋值;
4) Σ表示输入输出动作的集合;
5) E表示边的集合, E⊆L×L(X)×Σ×2X×L, ×为笛卡儿积运算符;
6) R:L→INX对每个位置分配相应的时钟增长速率;
7) I:L→u(X) 对每个位置分配不变量;
价格时间自动机网络 (NPTA) 由多个相关PTA组成, 它们之间通过广播通道和共享变量交互, 可以表示由多个模块组成的系统。
2.2 MPSoC调度系统MPSoC调度系统由程序, 运行平台及调度管理模块组成。程序包括一组周期任务, 运行平台包括多个不同种类的处理器, 调度管理模块则调度任务的运行。
调度系统的价格时间自动机网络可表示为任务价格时间自动机和调度管理模块价格时间自动机的并行组合。处理器只有执行状态和挂起状态, 故不单独建模。下文具体给出任务和调度管理模块的建模方法。
2.3 任务建模任务属性根据MPSoC配置。任务价格时间自动机通过初始化任务价格时间自动机模板 (如图 2所示) 得到。就绪任务存储在全局队列ReadyTask[n]中。任务使用2个时钟变量记录周期中的时间属性:周转时间TAtime记录从周期开始到任务完成的时间, 创建时间CTtime记录周期开始后的时间, CTtime持续增长并在周期结束后重置。此外, 每个任务使用时钟变量c, 表示已完成的计算量。不同处理器的执行速率不同, 用c′==exeRate[twp[tid]][tid]表示, 其中c′为c增加的速率, exeRate[twp[tid]][tid]为处理器执行任务的速率。
|
| 图 2 MPSoC任务的价格时间自动机 |
初始时, 任务在Init位置等待创建, 在initial-offset时刻创建, 并开始第一个周期的执行; 任务首先迁移到WaitingOffset位置等待分派, 分派后迁移到WaitingDepedency位置; 若收到依赖任务完成信号finish-notify, 则迁移到CheckDepedency位置检查是否还有未完成的依赖任务; 若有, 则返回到WaitingDepedency位置继续等待依赖任务执行完成; 若所有依赖任务都执行完成, 则迁移到Ready位置等待分配处理器; 当收到信号run, 表示已获得处理器, 并迁移到Running位置开始执行; 执行过程中, 若有其它任务抢占该处理器, 即收到preempt信号, 则返回Ready位置, 再次等待分配处理器; 如果任务执行完成前CTtime大于截止时间, 则迁移到Error位置, 表示任务不可调度; 如果任务执行完成, 则迁移到Complete位置, 并向所有依赖它的任务发送信号finish-notify; 最后迁移到PeriodDone位置, 等待下一周期的开始。
2.4 调度管理模块建模调度管理模块的价格时间自动机通过初始化调度管理模块价格时间自动机模板 (如图 3所示) 得到, 它根据全局FP策略调度任务。
|
| 图 3 MPSoC调度管理模块的价格时间自动机 |
调度管理模块停留在初始位置等待任务就绪或执行完成, 并根据当前处理器功率更新系统总功耗及各处理器功耗, 用数组r[n]存储处理器当前功率。
当有任务就绪时, 即接收到信号ready[i], 其中i为就绪任务编号, 调度管理模块将其插入就绪队列waitQueue中, 并调用函数IdlePE () 返回空闲处理器编号pid1, 然后迁移到TaskRun位置。若pid1值不小于0, 说明当前有空闲处理器, 则向就绪任务发送执行信号run, 并从waitQueue中移除; 若pid1值小于0, 说明当前没有空闲处理器, 则调用函数prmptPE () 返回可以被抢占的处理器编号pid2并迁移到TaskWait位置。若pid2值小于0, 表示没有可以抢占的处理器, 则就绪任务在waitQueue中继续等待; 若pid2值不小于0, 表示有可以抢占的处理器, 则抢占该处理器并迁移到TaskPrmpt位置, 向就绪任务发送信号run, 并从waitQueue中移除。
当有任务执行完成时, 即接收到信号finished[i], 其中i为完成任务的编号, 调用函数waitTask () 返回waitQueue中优先级最高任务的编号tid, 若tid小于0, 表示没有就绪任务, 若tid不小于0, 表示有就绪任务, 则将空闲处理器分配给该任务。
3 MPSoC模型可调度性分析MPSoC有严格的实时性和功耗要求, 当任务未在预定的截止时间前完成, 或总功耗超过阈值时, 都认为不可调度。本文使用统计模型检测引擎, 对MPSoC价格时间自动机模型进行可调度性分析, 它监测价格时间自动机模型的模拟过程, 并采用一些如Cross-Entropy的方法, 保证稀有情况被模拟到。最后使用统计学知识, 以一定置信度给出系统满足特定属性的概率。本文分析MPSoC的不可调度概率, 验证语句如下:Pr[≤t](＜＞exists (i:tid-t) Task (i).Error‖tatal-energy>=e)。它估算前t个时间单位内, MPSoC存在任务超时或总功耗超过e的概率, 并可以设置2个参数, 用以控制估算结果的置信度及精确性:
1) α用于控制估算结果的置信度;
2) ε用于控制估算结果的精确性;
另一种可调度性分析需求, 是判断不可调度概率是否小于某一阈值, 验证语句如下:Pr[≤t](＜＞exists (i:tid-t) Task (i).Error‖tatal-energy>=e)＜=p, 其中p∈[0, 1]。它验证前t个时间单位内, 系统不可调度的概率是否小于p。
4 实验验证为验证本文所提出模型的有效性, 以家族中ARM测试芯片TC2为平台原型, 采用音频解码器的任务模型作为任务实例, 如图 4所示。使用UPPAAL 4.1.19建模并估算任务不可调度的概率。
|
| 图 4 实例模型 |
Cortex-A15处理器最快处理速度为2.5 GHz, 平均功率为2 W, Cortex-A7处理器最快处理速度为1 GHz, 平均功率约为Cortex-A15的1/7。任务依赖图中的节点代表任务, 有向边代表任务间的依赖关系。执行过程中所有任务的创建时间为0, 睡眠时间为50单位, 任务周期和相对截止时间为100单位, 并要求1 000个时间单位中总功耗不超过800, 相关属性见表 1。表中CAL为任务计算量, P为任务优先级。该实例经过实际测试是可调度的。下面通过构建的价格时间自动机模型来验证实例的可调度性。
| Task | CAL | P | Cortex-A15 | Cortex-A7 | ||
| Rexe | Rdyn | Rexe | Rdyn | |||
| τ0 | 32;0.1 | 4 | 8.1 | 2.1 | 1.1 | 0.32 |
| τ1 | 24;0.1 | 3 | 8.1 | 2.1 | 1.1 | 0.32 |
| τ2 | 24;0.1 | 3 | 8.1 | 2.1 | 1.1 | 0.32 |
| τ3 | 16;0.1 | 2 | 8 | 2 | 1 | 0.3 |
| τ4 | 16;0.1 | 2 | 8 | 2 | 1 | 0.3 |
| τ5 | 8;0.1 | 1 | 7.9 | 1.9 | 0.9 | 0.27 |
| τ6 | 8;0.1 | 1 | 7.9 | 1.9 | 0.9 | 0.27 |
| τ7 | 16;0.1 | 2 | 8.2 | 2.2 | 1.2 | 0.33 |
| τ8 | 8;0.1 | 1 | 8 | 2 | 1 | 0.3 |
| τ9 | 8;0.1 | 1 | 8 | 2 | 1 | 0.3 |
| τ10 | 16;0.1 | 2 | 8.1 | 2.1 | 1.1 | 0.32 |
| τ11 | 16;0.1 | 2 | 8.1 | 2.1 | 1.1 | 0.32 |
| τ12 | 16;0.1 | 2 | 8 | 2 | 1 | 0.31 |
| τ13 | 16;0.1 | 2 | 8 | 2 | 1 | 0.31 |
| τ14 | 16;0.1 | 2 | 8.2 | 2.2 | 1.1 | 0.32 |
| τ15 | 16;0.1 | 2 | 8.2 | 2.2 | 1.1 | 0.32 |
| τ16 | 48;0.1 | 5 | 8.3 | 2.3 | 1.3 | 0.35 |
在UPPAAL中使用属性验证语句Pr[＜=1 000](＜＞exists (i:tid-t) Task (i).Error‖total-energy>=800) 估算实例在1 000个时间单位内不可调度概率, 设置不同α和ε值得到结果如表 2所示。
| 参数 | 概率 | 时间/s | 常驻内存/虚拟内存 |
| α=0.05, ε=0.05 | [0, 0.097 393 8] | 115.938 | 15 436/43 988 |
| α=0.05, ε=0.01 | [0, 0.019 956 0] | 607.783 | 18 152/49 932 |
| α=0.01, ε=0.01 | [0, 0.019 944 1] | 874.615 | 20 988/52 036 |
表中不同统计参数值对应的概率区间下限都为0, 说明UPPAAL模拟过程中未找到使MPSoC不可调度的情况, 并且看出较小的统计参数值得到的概率区间上限更小, 这是因为该实例已确定可调度, 故更高的精确度得到的结果上限将进一步趋于0。
若要求实例在1 000个时间单位中总功耗不超过500, 即验证Pr[＜=1000](＜＞exists (i:tid-t) Task (i).Error‖total-energy>=500), 在99%的置信度及1%概率不确定性下得到任务不可调度的概率区间为[0.902 606, 1], 说明实例不可调度, UPPAAL还生成了不可调度的概率密度分布图，如图 5所示。
|
| 图 5 α=0.01, ε=0.05时结果的概率密度分布图 |
图 5描述了模拟过程中不同时间段的不可调度概率, 其中出现不可调度情况的时间期望为658.13。
5 结论本文所提出的价格时间自动机模型, 对任务抢占、迁移、依赖及处理器功耗等特性, 都进行了建模, 更全面地描述了MPSoC调度系统; 统计模型检测方法使用较少的内存和时间, 对MPSoC进行可调度性分析, 准确地给出了属性满足的概率区间, 可分析复杂的MPSoC模型。未来我们将对总线通信, 数据传输等特性建模, 以形成一套更完整的MPSoC可调度性分析的价格时间自动机模型。
| [1] | Baker T P. An Analysis of Fixed-Priority Schedulability on a Multiprocessor[J]. Real-Time Systems, 2006, 32(1): 49–71. |
| [2] | Singhoff F, Legrand J, Nana L, et al. Scheduling and Memory Requirements Analysis with AADL[C]//ACM SIGAda International Conference on Ada:the Engineering of Correct and Reliable Software for Real-Time & Distribute Systems Using Ada and Related Technologies 2005, Atlanta, GA, USA, 2005:1-10 |
| [3] | Boudjadar A, David A, Jin H K, et al. Hierarchical Scheduling Framework Based on Compositional Analysis Using UPPAAL[C]//Proceedings of FACS 2013, 2013:61-78 |
2. Beijing Shenzhou Aerospace Software Technology Co.Ltd, Beijing 100094, China
