《计算机应用》唯一官方网站 ›› 2023, Vol. 43 ›› Issue (1): 185-191.DOI: 10.11772/j.issn.1001-9081.2021111862

所属专题： 先进计算

• 先进计算 • 上一篇    下一篇

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

姜松岩, 廖晓鹃, 陈光柱   

  1. 成都理工大学 计算机与网络安全学院，成都 610059
  • 收稿日期:2021-11-05 修回日期:2022-05-07 发布日期:2023-01-12
  • 通讯作者: 廖晓鹃（1986—），女，四川成都人，副教授，博士，CCF会员，主要研究方向：智能调度、自动推理、形式化方法及其应用liaoxiaojuan18@cdut.edu.cn
  • 作者简介:姜松岩（1997—），男，河北秦皇岛人，硕士研究生，主要研究方向：数学规划、智能调度；陈光柱（1972—），男，四川内江人，教授，博士，CCF会员，主要研究方向：图像与视觉、智能调度、工业互联网；
  • 基金资助:
    国家自然科学基金资助项目（61806171）；四川省科技计划重点研发项目（2022YFG0198）。

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

JIANG Songyan, LIAO Xiaojuan, CHEN Guangzhu   

  1. College of Computer Science and Cyber Security， Chengdu University of Technology， Chengdu Sichuan 610059， China
  • Received:2021-11-05 Revised:2022-05-07 Online:2023-01-12
  • Contact: LIAO Xiaojuan， born in 1986， Ph. D.， associate professor. Her research interests include intelligent scheduling， automatic reasoning， formal method and its applications.
  • About author:JIANG Songyan， born in 1997， M. S. candidate. His research interests include mathematical planning， intelligent scheduling；CHEN Guangzhu， born in 1972， Ph. D.， professor. His research interests include image and vision， intelligent scheduling， industrial Internet；
  • Supported by:
    This work is partially supported by National Natural Science Foundation of China （61806171）， Key Research and Development Project of Sichuan Province Science and Technology Plan （2022YFG0198）.

RichHTML

PDF

摘要： 在一组相同处理器上调度带有通信延迟的任务图以实现其最短的执行时间，这在并行计算的调度理论和实践中具有重要的意义。针对具有通信延迟的任务图调度问题，提出一种基于可满足性模理论（SMT）的改进SMT方法。首先，将处理器映射约束和任务执行顺序等约束条件进行编码，将任务图调度问题转化为SMT问题；然后，调用SMT求解器对可行解空间进行搜索，以确定问题最优解。在约束编码阶段，使用整型变量表示任务和处理器的映射关系，从而降低处理器约束编码的复杂程度；在求解器调用阶段，通过添加独立任务的约束条件减小求解器的搜索空间，进一步提升最优解的查找效率。实验结果表明，与原始SMT方法相比，改进SMT方法在20 s和1 min超时实验中的平均求解时间分别减少了65.9%与53.8%，并且在处理器数量较多时取得了更大的效率优势。改进的SMT方法可以有效求解带通信延迟的任务图调度问题，尤其适用于处理器数量较多的调度场景。

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

Abstract: 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.

Key words: parallel computing, task scheduling, Satisfiability Modulo Theory (SMT), linear programming, Directed Acyclic Graph (DAG)

中图分类号: 

版权所有 © 2021 四川计算机应用杂志社有限公司
蜀ICP备 05010208 号-3　新出网证(川)字026号
技术支持：北京玛格泰克科技发展有限公司
访问总数：
今日访问：