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

doi:10.11772/j.issn.1001-9081.2021111862

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

所属专题：先进计算

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

姜松岩, 廖晓鹃, 陈光柱

成都理工大学计算机与网络安全学院，成都 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

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）.

摘要/Abstract

摘要： 在一组相同处理器上调度带有通信延迟的任务图以实现其最短的执行时间，这在并行计算的调度理论和实践中具有重要的意义。针对具有通信延迟的任务图调度问题，提出一种基于可满足性模理论（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)

中图分类号:

姜松岩, 廖晓鹃, 陈光柱. 基于可满足性模理论的多处理机通信延迟优化任务调度方法[J]. 计算机应用, 2023, 43(1): 185-191.

JIANG Songyan, LIAO Xiaojuan, CHEN Guangzhu. Optimal task scheduling method based on satisfiability modulo theory for multiple processors with communication delay[J]. Journal of Computer Applications, 2023, 43(1): 185-191.

参考文献

1 GRAHAM R L， LAWLER E L， LENSTRA J K， et al. Optimization and approximation in deterministic sequencing and scheduling： a survey［M］// HAMMER P L， JOHNSON E L， KORTE B H. Annals of Discrete Mathematics， Volume 5： Discrete Optimization Ⅱ. Amsterdam： Elsevier， 1979： 287-326. 10.1016/s0167-5060(08)70356-x
2 SARKAR V. Partitioning and scheduling parallel programs for execution on multiprocessors［D］. Stanford： Stanford University， 1987：12-27. 10.21236/ada177641
3 ORR M， SINNEN O. Optimal task scheduling benefits from a duplicate-free state-space［J］. Journal of Parallel and Distributed Computing， 2020， 146： 158-174. 10.1016/j.jpdc.2020.07.005
4 张架鹏，倪志伟，倪丽萍，等. 基于改进离散人工蜂群算法的同类机调度优化［J］. 计算机应用， 2020， 40（3）：689-697. 10.11772/j.issn.1001-9081.2019071203 ZHANG J P， NI Z W， NI L P， et al. Parallel machine scheduling optimization based on improved discrete artificial bee colony algorithm［J］. Journal of Computer Applications， 2020， 40（3）：689-697. 10.11772/j.issn.1001-9081.2019071203
5 翟文正，胡越黎，冉峰. 异构多核DAG任务模型的微粒群优化调度算法［J］. 计算机工程与设计， 2016， 37（7）：1831-1835. 10.16208/j.issn1000-7024.2016.07.025 ZHAI W Z， HU Y L， RAN F. PSO scheduling algorithm for heterogeneous multi-core DAG task model［J］. Computer Engineering and Design， 2016， 37（7）：1831-1835. 10.16208/j.issn1000-7024.2016.07.025
6 马晓梅，何非. 基于改进遗传算法的标签印刷生产调度技术［J］. 计算机应用， 2021， 41（3）：860-866. 10.11772/j.issn.1001-9081.2020060833 MA X M， HE F， Label printing production scheduling technology based on improved genetic algorithm［J］. Journal of Computer Applications， 2021， 41（3）：860-866. 10.11772/j.issn.1001-9081.2020060833
7 杨小东，康雁，柳青，等. 求解作业车间调度问题的混合帝国主义竞争算法［J］. 计算机应用， 2017， 37（2）：517-522， 552. 10.11772/j.issn.1001-9081.2017.02.0517 YANG X D， KANG Y， LIU Q， et al. Hybrid imperialist competitive algorithm for solving job-shop scheduling problem［J］. Journal of Computer Applications， 2017， 37（2）：517-522， 552. 10.11772/j.issn.1001-9081.2017.02.0517
8 YING K C， CHENG C Y， LIN S W， et al. Comparative analysis of mixed integer programming formulations for single-machine and parallel-machine scheduling problems［J］. IEEE Access， 2019， 7： 152998-153011. 10.1109/access.2019.2947685
9 MENG L L， ZHANG C Y， REN Y P， et al. Mixed-integer linear programming and constraint programming formulations for solving distributed flexible job shop scheduling problem［J］. Computers and Industrial Engineering， 2020， 142： No.106347. 10.1016/j.cie.2020.106347
10 HUNG H C， LIN B M T， POSNER M E， et al. Preemptive parallel-machine scheduling problem of maximizing the number of on-time jobs［J］. Journal of Scheduling， 2019， 22（4）： 413-431. 10.1007/s10951-018-0584-y
11 LIU W C， GU Z H， XU J， et al. Satisfiability modulo graph theory for task mapping and scheduling on multiprocessor systems［J］. IEEE Transactions on Parallel and Distributed Systems， 2011， 22（8）： 1382-1389. 10.1109/tpds.2010.204
12 KOSHIMURA M， NABESHIMA H， FUJITA H， et al. Solving open job-shop scheduling problems by SAT encoding［J］. IEICE Transactions on Information and Systems， 2010， E93-D（8）： 2316-2318. 10.1587/transinf.e93.d.2316
13 MALIK A， WALKER C， O’SULLIVAN M， et al. Satisfiability Modulo Theory （SMT） formulation for optimal scheduling of task graphs with communication delay［J］. Computers and Operations Research， 2018， 89： 113-126. 10.1016/j.cor.2017.08.012
14 WANG S M， LIAO X J， WANG M， et al. An improved SMT-based scheduling for overloaded real-time systems［J］. Engineering Letters， 2020， 28（1）：112-122.
15 TANG Q， ZHU L H， LIAN J， et al. An efficient multi-functional duplication-based scheduling framework for multiprocessor systems［J］. The Journal of Supercomputing， 2020， 76（11）：9142-9167. 10.1007/s11227-020-03208-y
16 王翀，吕荫润，陈力，等. SMT求解技术的发展及最新应用研究综述［J］. 计算机研究与发展， 2017， 54（7）：1405-1425. 10.7544/issn1000-1239.2017.20160303 WANG C， LYU Y R， CHEN L， et al. Survey on development of solving methods and state-of-the-art applications of satisfiability modulo theories［J］. Journal of Computer Research and Development， 2020， 54（7）：1405-1425. 10.7544/issn1000-1239.2017.20160303
17 金继伟，马菲菲，张健. SMT求解技术简述［J］. 计算机科学与探索， 2015， 9（7）：769-780. JIN J W， MA F F， ZHANG J. Brief introduction to SMT solving［J］. Journal of Frontiers of Computer Science and Technology， 2015， 9（7）：769-780.
18 任胜兵，吴斌，张健威，等. 基于可满足性模理论求解器的程序路径验证方法［J］. 计算机应用， 2016， 36（10）：2806-2810. 10.11772/j.issn.1001-9081.2016.10.2806 REN S B， WU B， ZHANG J W， et al. Method of program path validation based on satisfiability modulo theory solver［J］. Journal of Computer Applications， 2016， 36（10）：2806-2810. 10.11772/j.issn.1001-9081.2016.10.2806
19 VENUGOPALAN S， SINNEN O. ILP formulations for optimal task scheduling with communication delays on parallel systems［J］. IEEE Transactions on Parallel and Distributed Systems， 2015， 26（1）： 142-151. 10.1109/tpds.2014.2308175
20 DE MOURA L， BJ?RNER N. Z3： an efficient SMT solver［C］// Proceedings of the 2008 International Conference on Tools and Algorithms for the Construction and Analysis of Systems， LNCS 4963. Berlin： Springer， 2008： 337-340.
21 Gurobi Optimization， LLC. Gurobi optimizer reference manual［EB/OL］. ［2021-06-10］.https：//www.gurobi.com/documentation/9.5/refman/index.html.
22 CANON L C， EL SAYAH M， HéAM P C. A comparison of random task graph generation methods for scheduling problems［C］// Proceedings of the 2019 European Conference on Parallel Processing， LNCS 11725. Cham： Springer， 2019： 61-73.

[1]	林东东, 李曼曼, 陈少真. 基于神经区分器的KATAN48算法条件差分分析方法[J]. 《计算机应用》唯一官方网站, 2023, 43(8): 2462-2470.
[2]	方和平, 刘曙光, 冉泳屹, 钟坤华. 基于深度强化学习的多数据中心一体化调度优化[J]. 《计算机应用》唯一官方网站, 2023, 43(6): 1884-1892.
[3]	石一鹏, 刘杰, 祖锦源, 张涛, 张国群. 基于混合整数线性规划模型的SPONGENT S盒紧凑约束分析[J]. 《计算机应用》唯一官方网站, 2023, 43(5): 1504-1510.
[4]	徐周波, 陈浦青, 刘华东, 杨欣. 基于自注意力网络的深度图匹配模型[J]. 《计算机应用》唯一官方网站, 2023, 43(4): 1005-1012.
[5]	宁明超, 张俊勃, 陈戈. 基于面向服务架构的工业软件的任务调度算法[J]. 《计算机应用》唯一官方网站, 2023, 43(3): 885-893.
[6]	吴仁彪, 张振驰, 贾云飞, 乔晗. 云平台下基于截止时间的自适应调度策略[J]. 《计算机应用》唯一官方网站, 2023, 43(1): 176-184.
[7]	蔡婧雯, 韦永壮, 刘争红. 基于GPU的密码S盒代数性质评估方法[J]. 《计算机应用》唯一官方网站, 2022, 42(9): 2750-2756.
[8]	王旭, 申玉民, 熊晓芸, 李鹏, 王金龙. 基于哈希图的建筑物联网数据管理方法[J]. 《计算机应用》唯一官方网站, 2022, 42(8): 2471-2480.
[9]	张金泉, 徐寿伟, 李信诚, 王重洋, 徐景芝. 基于正交自适应鲸鱼优化的云计算任务调度[J]. 《计算机应用》唯一官方网站, 2022, 42(5): 1516-1523.
[10]	吴晴晴, 周丽华, 寸轩懿, 杜国王, 姜懿庭. 异质信息网络中基于有向无环图的影响力最大化算法[J]. 《计算机应用》唯一官方网站, 2022, 42(3): 895-903.
[11]	邱鑫源, 叶泽聪, 崔翛龙, 高志强. 联邦学习通信开销研究综述[J]. 《计算机应用》唯一官方网站, 2022, 42(2): 333-342.
[12]	徐启迪, 刘争红, 郑霖. 基于GPU的低密度奇偶校验码译码加速技术[J]. 《计算机应用》唯一官方网站, 2022, 42(12): 3841-3846.
[13]	解文博, 韦永壮, 刘争红. 基于CUDA的SKINNY加密算法并行实现与分析[J]. 计算机应用, 2021, 41(4): 1136-1141.
[14]	姜琨, 刘征, 朱磊, 李晓星. 基于有向无环图的倒排链等字长划分压缩算法[J]. 计算机应用, 2021, 41(3): 727-732.
[15]	杨先凤, 贵红军, 傅春常. 统一计算设备架构下的F-X域预测滤波并行算法[J]. 计算机应用, 2021, 41(2): 486-491.

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

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

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics