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

doi:10.11772/j.issn.1001-9081.2021111862

Journal of Computer Applications ›› 2023, Vol. 43 ›› Issue (1): 185-191.DOI: 10.11772/j.issn.1001-9081.2021111862

Special Issue: 先进计算

• Advanced computing • Previous Articles Next Articles

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

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

姜松岩, 廖晓鹃, 陈光柱

成都理工大学计算机与网络安全学院，成都 610059

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

Abstract

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)

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

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

CLC Number:

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.

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

References

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]	Runlian ZHANG, Mi ZHANG, Xiaonian WU, Rui SHU. Differential property evaluation method based on GPU for large-state cryptographic S-boxes [J]. Journal of Computer Applications, 2024, 44(9): 2785-2790.
[2]	Shaofa SHANG, Lin JIANG, Yuancheng LI, Yun ZHU. Adaptive partitioning and scheduling method of convolutional neural network inference model on heterogeneous platforms [J]. Journal of Computer Applications, 2023, 43(9): 2828-2835.
[3]	Xinming GUO, Rui LIU, Fei XIE, Deyu LIN. β-QoM target-barrier coverage construction algorithm for wireless visual sensor network [J]. Journal of Computer Applications, 2023, 43(9): 2877-2884.
[4]	Dongdong LIN, Manman LI, Shaozhen CHEN. Conditional differential cryptanalysis method of KATAN48 algorithm based on neural distinguishers [J]. Journal of Computer Applications, 2023, 43(8): 2462-2470.
[5]	Heping FANG, Shuguang LIU, Yongyi RAN, Kunhua ZHONG. Integrated scheduling optimization of multiple data centers based on deep reinforcement learning [J]. Journal of Computer Applications, 2023, 43(6): 1884-1892.
[6]	Yipeng SHI, Jie LIU, Jinyuan ZU, Tao ZHANG, Guoqun ZHANG. Compact constraint analysis of SPONGENT S-box based on mixed integer linear programming model [J]. Journal of Computer Applications, 2023, 43(5): 1504-1510.
[7]	Zhoubo XU, Puqing CHEN, Huadong LIU, Xin YANG. Deep graph matching model based on self-attention network [J]. Journal of Computer Applications, 2023, 43(4): 1005-1012.
[8]	Mingchao NING, Junbo ZHANG, Ge CHEN. Task scheduling algorithm for service-oriented architecture-based industrial software [J]. Journal of Computer Applications, 2023, 43(3): 885-893.
[9]	Fuqin DENG, Huanzhao HUANG, Chaoen TAN, Lanhui FU, Jianmin ZHANG, Tinlun LAM. Multi-robot task allocation algorithm combining genetic algorithm and rolling scheduling [J]. Journal of Computer Applications, 2023, 43(12): 3833-3839.
[10]	Qian LIU, Yangming ZHANG, Dingsheng WAN. Parallel computing algorithm of grid-based distributed Xin’anjiang hydrological model [J]. Journal of Computer Applications, 2023, 43(11): 3327-3333.
[11]	WU Renbiao, ZHANG Zhenchi, JIA Yunfei, QIAO Han. Adaptive scheduling strategy based on deadline under cloud platform [J]. Journal of Computer Applications, 2023, 43(1): 176-184.
[12]	Jingwen CAI, Yongzhuang WEI, Zhenghong LIU. GPU-based method for evaluating algebraic properties of cryptographic S-boxes [J]. Journal of Computer Applications, 2022, 42(9): 2750-2756.
[13]	Xu WANG, Yumin SHEN, Xiaoyun XIONG, Peng LI, Jinlong WANG. Data management method for building internet of things based on Hashgraph [J]. Journal of Computer Applications, 2022, 42(8): 2471-2480.
[14]	Jinquan ZHANG, Shouwei XU, Xincheng LI, Chongyang WANG, Jingzhi XU. Cloud computing task scheduling based on orthogonal adaptive whale optimization [J]. Journal of Computer Applications, 2022, 42(5): 1516-1523.
[15]	Qingqing WU, Lihua ZHOU, Xuanyi CUN, Guowang DU, Yiting JIANG. Influence maximization algorithm based on directed acyclic graph in heterogeneous information networks [J]. Journal of Computer Applications, 2022, 42(3): 895-903.

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

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

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics