×

zbMATH — the first resource for mathematics

Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay. (English) Zbl 1391.90290
Summary: In scheduling theory and practise for parallel computing, representing a program as a task graph with communication delays is a popular model, due to its general nature, its expressiveness and relative simplicity. Unfortunately, scheduling such a task graph on a set of processors in such a way that it achieves its shortest possible execution time (\(P|\mathrm{pred}, c_{ij}| C_{\max}\) in \(\alpha|\beta|\gamma\) notation) is a strong NP-hard optimization problem without any known guaranteed approximation algorithm. Hence, many heuristics have been researched and are used in practise. However, in many situations it is necessary to obtain optimal schedules, for example, in the case of time-critical systems or for the evaluation of heuristics. Recent years have seen some advances in optimal algorithms for this scheduling problem, based on smart exhaustive state-space search or MILP (mixed integer linear programming) formulations. This paper proposes a novel approach based on SMT (satisfiability modulo theory). We propose an elegant SMT formulation of the scheduling problem that only needs one decision variable and is very compact and comprehensible in comparison to the state-of-the-art MILP formulations. This novel optimal scheduling approach is extensively evaluated in experiments with more than a thousand task graphs. We perform experimental comparison with the best known MILP formulations, with attempts to further improve them, and deeply analyse the behaviour of the different approaches with respect to size, structure, number of processors, etc. Our proposed SMT-based approach in general outperforms the MILP-formulations and still possesses great potential for further optimization, from which MILP formulations have benefited in the past.
MSC:
90B35 Deterministic scheduling theory in operations research
68M14 Distributed systems
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
90C11 Mixed integer programming
Software:
GXL; z3; JaCoP; KAAPI; StarPU; Gurobi
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Augonnet, C.; Thibault, S.; Namyst, R.; Wacrenier, P.-A., Starpu: a unified platform for task scheduling on heterogeneous multicore architectures, Concurr. Comput., 23, 2, 187-198, (2011)
[2] Barrett, C. W.; Sebastiani, R.; Seshia, S. A.; Tinelli, C., Satisfiability modulo theories., Handb. Satisf., 185, 825-885, (2009)
[3] Bender, A., MILP based task mapping for heterogeneous multiprocessor systems, in Proceedings European Design Automation Conference, 190-197, (1996), IEEE
[4] Board, O.A.R., 2013. OpenMP application program interface, version 4.0. http://www.openmp.org/mp-documents/OpenMP4.0.0.pdf.
[5] Bosilca, G.; Bouteiller, A.; Danalis, A.; Faverge, M.; Herault, T.; Dongarra, J. J., Parsec: exploiting heterogeneity for enhancing scalability, Comput. Sci. Eng., 15, 6, 36-45, (2013)
[6] Chapter 3 parallel machines - Linear programming and enumerative algorithms, Ann. Oper. Res. 1986, 7, 99-132 doi: 10.1007/BF02186435.
[7] Chrétienne, P., Task scheduling over distributed memory machines, Proc. of the Int. Workshop on Parallel and Distributed Algorithms. North-Holland, Amsterdam, (1989)
[8] Cirou, B.; Jeannot, E., Triplet: a clustering scheduling algorithm for heterogeneous systems, Proc. of Workshop on Scheduling and Resource Management for Cluster Computing (ICPP 2001), 231-236, (2001), IEEE Press Valencia, Spain
[9] Coll, P. E.; Ribeiro, C. C.; de Souza, C. C., Multiprocessor scheduling under precedence constraints: polyhedral results, Discr. Appl. Math., 154, 5, 770-801, (2006) · Zbl 1120.90070
[10] Daoud, M. I.; Kharma, N., A hybrid heuristic genetic algorithm for task scheduling in heterogeneous processor networks, J. Parallel Distrib. Comput., 71, 11, 1518-1531, (2011)
[11] Davare, A.; Chong, J.; Zhu, Q.; Densmore, D.; Sangiovanni-Vincentelli, A., Classification, customization, and characterization: using MILP for task allocation and scheduling, Technical Report, UCB/EECS-2006-166, (2006), University of California, Berkeley
[12] Davare, A.; Chong, J.; Zhu, Q.; Densmore, D. M.; Sangiovanni-Vincentelli, A. L., Classification, customization, and characterization: using MILP for task allocation and scheduling, Technical Report, UCB/EECS-2006-166, (2006), EECS Department, University of California, Berkeley
[13] Davidović, T.; Crainic, T. G., Benchmark-problem instances for static scheduling of task graphs with communication delays on homogeneous multiprocessor systems, Comput. Oper. Res., 33, 8, 2155-2177, (2006) · Zbl 1086.90021
[14] Davidović, T.; Liberti, L.; Maculan, N.; Mladenović, N., Mathematical programming-based approach to scheduling of communicating tasks, Technical Report, (2004)
[15] Davidović, T.; Liberti, L.; Maculan, N.; Mladenović, N., Towards the optimal solution of the multiprocessor scheduling problem with communication delays, In Proc. 3rd Multidisciplinary Int. Conf. on Scheduling: Theory and Application (MISTA), 128-135, (2007)
[16] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun. ACM, 5, 7, 394-397, (1962) · Zbl 0217.54002
[17] De Moura, L.; Bjørner, N., Z3: an efficient smt solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340, (2008), Springer
[18] Drozdowski, M., Scheduling for parallel processing, (2009), Springer · Zbl 1187.68090
[19] El Cadi, A. A.; Atitallah, R. B.; Hanafi, S.; Mladenović, N.; Artiba, A., New mip model for multiprocessor scheduling problem with communication delays, Optim. Lett., 1-17, (2014)
[20] El-Rewini, H.; Ali, H. H., On considering communication in scheduling task graphs on parallel processors, J. Parallel Algo. Appl., 3, 177-191, (1994) · Zbl 1049.68528
[21] Floudas, C. A.; Lin, X., Mixed integer linear programming in process scheduling: modeling, algorithms, and applications, Ann. Oper. Res., 139, 1, 131-162, (2005) · Zbl 1091.90055
[22] Friedman, J.; Hastie, T.; Tibshirani, R., The elements of statistical learning, Vol. 1, (2001), Springer series in statistics Springer, Berlin
[23] Gautier, T.; Besseron, X.; Pigeon, L., KAAPI: a thread scheduling runtime system for data flow computations on cluster of multi-processors, International Workshop on Parallel Symbolic Computation, 15-23, (2007)
[24] Gurobi Optimization, I., 2015. Gurobi optimizer reference manual. URL http://www.gurobi.com.
[25] Hu, T., Parallel sequencing and assembly line problems, Oper. Res., 9, 6, 841-848, (1961)
[26] Hwang, J. J.; Chow, Y. C.; Anger, F. D.; Lee, C. Y., Scheduling precedence graphs in systems with interprocessor communication times, ‎SIAM J. Sci. Comput., 18, 2, 244-257, (1989) · Zbl 0677.68026
[27] Kadamuddi, D.; Tsai, J. J.P., Clustering algorithm for parallelizing software systems in multiprocessor environment, ‎IEEE Trans. Softw. Eng., 26, 4, (2000)
[28] Kafil, M.; Ahmad, I., Optimal task assignment in heterogeneous distributed computing systems, IEEE Concurr., 6, 42-51, (1998)
[29] Kianzad, V.; Bhattacharyya, S. S., Efficient techniques for clustering and scheduling onto embedded multiprocessors, IEEE Trans. Parallel Distrib. Syst., 17, 7, 667-680, (2006)
[30] Kuchcinski, K., Constraints-driven scheduling and resource assignment, ACM Trans. Des. Autom. Electron. Syst., 8, 3, 355-383, (2003)
[31] Kwok, Y.-K.; Ahmad, I., On multiprocessor task scheduling using efficient state space approaches, J. Parallel Distrib. Comput., 65, 1515-1532, (2005) · Zbl 1103.68406
[32] Liu, G. Q.; Poh, K. L.; Xie, M., Iterative List scheduling for heterogenous computing, J. Parallel Distrib. Comput., 65, 5, 654-665, (2005) · Zbl 1101.68420
[33] Liu, W.; Gu, Z.; Xu, J.; Wu, X.; Ye, Y., Satisfiability modulo graph theory for task mapping and scheduling on multiprocessor systems, IEEE Trans. Parallel Distrib. Syst., 22, 8, 1382-1389, (2011)
[34] Macey, B. S.; Zomaya, A. Y., A performance evaluation of CP List scheduling heuristics for communication intensive task graphs, Parallel Processing Symposium, 1998. Proc. of IPPS/SPDP 1998, 538-541, (1998)
[35] Maculan, N.; Porto, S. C.S.; Ribeiro, C. C.; de Souza, C. C.; Cid, R.; Souza, C., A new formulation for scheduling unrelated processors under precedence constraints, RAIRO Oper. Res., 33, 87-91, (1997) · Zbl 0958.90046
[36] Mallach, S., 2016. Improved mixed-integer programming models for multiprocessor scheduling with communication delays. Tech. rep., Institut fur Informatik Universitat zu Koln, 50923 Koln, Germany.
[37] Mcnemar’s hypothesis results. https://anon1980.bitbucket.io/McNemar_results.html. Accessed: 2017-06-15.
[38] McNemar, Q., Note on the sampling error of the difference between correlated proportions or percentages, Psychometrika, 12, 2, 153-157, (1947)
[39] Omara, F. A.; Arafa, M. M., Genetic algorithms for task scheduling problem, J. Parallel Distrib. Comput., 70, 13-22, (2010) · Zbl 1233.68077
[40] Orr, M.; Sinnen, O., A duplicate-free state-space model for optimal task scheduling, Proc. of 21st Int. European Conference on Parallel and Distributed Computing (Euro-Par 2015). Vol. 9233 of Lecture Notes in Computer Science, (2015), Springer Vienna, Austria
[41] Planas, J.; Badia, R. M.; Ayguadé, E.; Labarta, J., Hierarchical task-based programming with starss, IJHPCA, 23, 3, 284-299, (2009)
[42] Sarkar, V., Partitioning and scheduling parallel programs for execution on multiprocessors, Technical Report, (1987), Stanford Univ., CA (USA)
[43] Shahul, A. Z.S.; Sinnen, O., Scheduling task graphs optimally with A*, J. Supercomput., 51, 3, 310-332, (2010)
[44] Sinnen, O., Task scheduling for parallel systems, (2007), Wiley
[45] Sinnen, O., Reducing the solution space of optimal task scheduling, Comput. Oper. Res., 43, 201-214, (2014) · Zbl 1348.90312
[46] Sinnen, O., Reducing the solution space of optimal task scheduling, Comput. Oper. Res., 43, 201-214, (2014) · Zbl 1348.90312
[47] Venugopalan, S.; Sinnen, O., Optimal linear programming solutions for multiprocessor scheduling with communication delays, Proc. of 12th Int. Conference on Algorithms and Architectures for Parallel Processing (ICA3PP 2012). Vol. 7439 of Lecture Notes in Computer Science, 129-138, (2012), Springer Fukuoka, Japan
[48] Venugopalan, S.; Sinnen, O., ILP formulations for optimal task scheduling with communication delays on parallel systems, IEEE Trans. Parallel Distrib. Syst., 26, 1, 142-151, (2015)
[49] Venugopalan, S.; Sinnen, O., Memory limited algorithms for optimal task scheduling on parallel systems, J. Parallel Distrib. Comput., 92, 35-49, (2016)
[50] Winter, A.; Kullbach, B.; Riediger, V., An overview of the gxl graph exchange language, Softw. Vis., 528-532, (2002) · Zbl 1043.68992
[51] Yang, T.; Gerasoulis, A., List scheduling with and without communication delays, Parallel Comput., 19, 12, 1321-1344, (1993) · Zbl 0797.68020
[52] Yang, T.; Gerasoulis, A., On the granularity and clustering of directed acyclic task graphs, IEEE Trans. Parallel Distrib. Syst., 4, 6, 686-701, (1993)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.