Task-Node Mapping in an Arbitrary Computer Network Using SMT Solver

  • Andrii KovalovEmail author
  • Elisabeth Lobe
  • Andreas Gerndt
  • Daniel Lüdtke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


The problem of mapping (assigning) application tasks to processing nodes in a distributed computer system for spacecraft is investigated in this paper. The network architecture is developed in the project ‘Scalable On-Board Computing for Space Avionics’ (ScOSA) at the German Aerospace Center (DLR). In ScOSA system the processing nodes are connected to a network with an arbitrary topology. The applications are structured as directed graphs of periodic and aperiodic tasks that exchange messages. In this paper a formal definition of the mapping problem is given. We demonstrate several ways to formulate it as a satisfiability modulo theories (SMT) problem and then use Z3, a state-of-the-art SMT solver, to produce the mapping. The approach is evaluated on a mapping problem for an optical navigation application as well as on a set of randomly generated task graphs.


  1. 1.
    Baruah, S.: Task partitioning upon heterogeneous multiprocessor platforms. In: Proceedings of the 10th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2004, pp. 536–543 (2004)Google Scholar
  2. 2.
    Biewer, A., Andres, B., Gladigau, J., Schaub, T., Haubelt, C.: A symbolic system synthesis approach for hard real-time systems based on coordinated SMT-solving. In: 2015 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 357–362 (2015)Google Scholar
  3. 3.
    Bjørner, N., Phan, A.-D., Fleckenstein, L.: vZ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46681-0_14 Google Scholar
  4. 4.
    Cheng, Z., Zhang, H., Tan, Y., Lim, Y.: SMT-based scheduling for multiprocessor real-time systems. In: 2016 IEEE/ACIS 15th International Conference on Computer and Information Science (ICIS), pp. 1–7 (2016)Google Scholar
  5. 5.
    Cruz, E.H.M., Diener, M., Pilla, L.L., Navaux, P.O.A.: An efficient algorithm for communication-based task mapping. In: 2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, pp. 207–214 (2015)Google Scholar
  6. 6.
    Deveci, M., Rajamanickam, S., Leung, V.J., Pedretti, K., Olivier, S.L., Bunde, D.P., Çatalyürek, U.V., Devine, K.: Exploiting geometric partitioning in task mapping for parallel computers. In: 2014 IEEE 28th International Parallel and Distributed Processing Symposium, pp. 27–36 (2014)Google Scholar
  7. 7.
    Franz, T., Lüdtke, D., Maibaum, O., Gerndt, A.: Model-based software engineering for an optical navigation system for spacecraft. In: Deutscher Luft-und Raumfahrtkongress. Braunschweig, Germany, September 2016Google Scholar
  8. 8.
    Glantz, R., Meyerhenke, H., Noe, A.: Algorithms for mapping parallel processes onto grid and torus architectures. In: Proceedings of the 2015 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015, pp. 236–243. IEEE Computer Society, Washington, DC (2015)Google Scholar
  9. 9.
    Hoefler, T., Jeannot, E., Mercier, G.: An overview of process mapping techniques and algorithms in high-performance computing. In: Jeannot, E., Zilinskas, J. (eds.) High Performance Computing on Complex Environments, pp. 75–94. Wiley (2014)Google Scholar
  10. 10.
    Hoefler, T., Snir, M.: Generic topology mapping strategies for large-scale parallel architectures. In: Proceedings of the International Conference on Supercomputing, ICS 2011, pp. 75–84. ACM, New York (2011)Google Scholar
  11. 11.
    Lee, S.Y., Aggarwal, J.K.: A mapping strategy for parallel processing. IEEE Trans. Comput. C–36(4), 433–442 (1987)Google Scholar
  12. 12.
    Lei, T., Kumar, S.: A two-step genetic algorithm for mapping task graphs to a network on chip architecture. In: Proceedings of the Euromicro Symposium on Digital System Design, pp. 180–187 (2003)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Liu, W., Yuan, M., He, X., Gu, Z., Liu, X.: Efficient SAT-based mapping and scheduling of homogeneous synchronous dataflow graphs for throughput optimization. In: 2008 Real-Time Systems Symposium, pp. 492–504 (2008)Google Scholar
  15. 15.
    Lüdtke, D., Westerdorff, K., Stohlmann, K., Börner, A., Maibaum, O., Peng, T., Weps, B., Fey, G., Gerndt, A.: OBC-NG: towards a reconfigurable on-board computing architecture for spacecraft. In: 2014 IEEE Aerospace Conference, pp. 1–13 (2014)Google Scholar
  16. 16.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  17. 17.
    Potts, C.: Analysis of a linear programming heuristic for scheduling unrelated parallel machines. Discrete Appl. Math. 10(2), 155–164 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Satish, N., Ravindran, K., Keutzer, K.: A decomposition-based constraint optimization approach for statically scheduling task graphs with communication delays to multiprocessors. In: 2007 Design, Automation Test in Europe Conference Exhibition, pp. 1–6 (2007)Google Scholar
  19. 19.
    Tendulkar, P., Poplavko, P., Maler, O.: Symmetry breaking for multi-criteria mapping and scheduling on multicores. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 228–242. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-40229-6_16 CrossRefGoogle Scholar
  20. 20.
    Wang, L., Li, Z., Song, M., Ren, S.: A genetic algorithm based approach to maximizing real-time system value under resource constraints. In: 2012 IEEE 31st International Performance Computing and Communications Conference (IPCCC), pp. 285–294 (2012)Google Scholar
  21. 21.
    Yang, L., Liu, W., Jiang, W., Li, M., Yi, J., Sha, E.H.M.: Application mapping and scheduling for network-on-chip-based multiprocessor system-on-chip with fine-grain communication optimization. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 24(10), 3027–3040 (2016)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Andrii Kovalov
    • 1
    Email author
  • Elisabeth Lobe
    • 1
  • Andreas Gerndt
    • 1
  • Daniel Lüdtke
    • 1
  1. 1.German Aerospace Center (DLR), Simulation and Software TechnologyCologneGermany

Personalised recommendations