基于可满足性模理论的多处理机通信延迟优化任务调度方法  

Optimal task scheduling method based on satisfiability modulo theory for multiple processors with communication delay

作　　者：姜松岩 廖晓鹃 陈光柱[1] JIANG Songyan;LIAO Xiaojuan;CHEN Guangzhu(College of Computer Science and Cyber Security,Chengdu University of Technology,Chengdu Sichuan 610059,China)

机构地区：[1]成都理工大学计算机与网络安全学院,成都610059

出　　处：《计算机应用》2023年第1期185-191,共7页journal of Computer Applications

基　　金：国家自然科学基金资助项目(61806171);四川省科技计划重点研发项目(2022YFG0198)。

摘　　要：在一组相同处理器上调度带有通信延迟的任务图以实现其最短的执行时间,这在并行计算的调度理论和实践中具有重要的意义。针对具有通信延迟的任务图调度问题,提出一种基于可满足性模理论(SMT)的改进SMT方法。首先,将处理器映射约束和任务执行顺序等约束条件进行编码,将任务图调度问题转化为SMT问题;然后,调用SMT求解器对可行解空间进行搜索,以确定问题最优解。在约束编码阶段,使用整型变量表示任务和处理器的映射关系,从而降低处理器约束编码的复杂程度;在求解器调用阶段,通过添加独立任务的约束条件减小求解器的搜索空间,进一步提升最优解的查找效率。实验结果表明,与原始SMT方法相比,改进SMT方法在20 s和1 min超时实验中的平均求解时间分别减少了65.9%与53.8%,并且在处理器数量较多时取得了更大的效率优势。改进的SMT方法可以有效求解带通信延迟的任务图调度问题,尤其适用于处理器数量较多的调度场景。It is of great significance in the scheduling theory and practice of parallel computing to achieve the minimum execution time of task graphs with communication delays on homogeneous multiple processors. For the task graph scheduling problem with communication delay, an optimization method based on Satisfiability Modulo Theory(SMT) was proposed.Firstly, constraints such as processor mapping constraints and task execution order were encoded, thus the task graph scheduling problem was transformed into an SMT problem. Then, the SMT solver was called to search the feasible solution space to determine the optimal solution of the problem. In the constraint encoding phase, integer variables were introduced to represent the mapping relationships between tasks and processors, thereby reducing the complexity of processor constraint encoding. In the solver calling phase, the constraints of independent tasks were added to reduce the search space of the solver and further improve the search efficiency of the optimal solution. Experimental results show that compared with the original SMT method, the improved SMT method reduces the average solving time by 65. 9% and 53. 8% in timeout experiments of 20 seconds and 1 minute, respectively, and achieves a greater efficiency advantage when the number of processors is relatively large. The improved SMT method can effectively solve the task graph scheduling problem with communication delay, especially be suitable for scheduling scenarios with a large number of processors.

关 键 词：并行计算 任务调度 可满足性模理论 线性规划 有向无环图 

分 类 号：TP332[自动化与计算机技术—计算机系统结构] TP301.6[自动化与计算机技术—计算机科学与技术]