Skip to main content
Top

2017 | OriginalPaper | Chapter

Towards Automated Variant Selection for Heterogeneous Tiled Architectures

Authors : Christel Baier, Sascha Klüppelholz, Sascha Wunderlich

Published in: Models, Algorithms, Logics and Tools

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Heterogeneous hardware/software systems that include many components with different characteristics offer great potential for high performance and energy-efficient computing. To exploit this potential, adaptive allocation and scheduling algorithms are needed for selecting software variants and mapping them to processing elements that attempt to achieve a good balance between resource-awareness and performance. The evaluation is typically carried out using simulation techniques. However, the space spanned by the possible combinations of hardware/software variants and management strategies is huge, which makes it nearly impossible to find an optimum using simulation-based methods. The purpose of the paper is to illustrate the general feasibility of an alternative approach using probabilistic model checking for families of systems that are obtained by varying, e.g., the hardware-software combinations or the resource management strategies. More precisely, we consider heterogeneous multi-processor systems based on tiled architectures and provide a tool chain that yields a flexible and comfortable way to specify families of concrete systems and to analyze them using the probabilistic model checker PRISM and ProFeat as a front end. We illustrate how the family-based approach can be used to analyze the potential of heterogeneous hardware elements, software variants and adaptive resource management and scheduling strategies by applying our framework to a simplified model of the multi-processor Tomahawk platform that has been designed for integrating heterogeneous devices.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
The implementation and examples are available for download at https://​wwwtcs.​inf.​tu-dresden.​de/​ALGI/​PUB/​KimFest17/​.
 
Literature
1.
go back to reference Arnold, O., Matus, E., Noethen, B., Winter, M., Limberg, T., Fettweis, G.: Tomahawk: parallelism and heterogeneity in communications signal processing MPSoCs. ACM Trans. Embed. Comput. Syst. 13(3s), 107:1–107:24 (2014)CrossRef Arnold, O., Matus, E., Noethen, B., Winter, M., Limberg, T., Fettweis, G.: Tomahawk: parallelism and heterogeneity in communications signal processing MPSoCs. ACM Trans. Embed. Comput. Syst. 13(3s), 107:1–107:24 (2014)CrossRef
2.
3.
go back to reference Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. STTT 14(1), 53–72 (2012)CrossRef Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. STTT 14(1), 53–72 (2012)CrossRef
4.
go back to reference Bell, S., Edwards, B., Amann, J., Conlin, R., Joyce, K., Leung, V., MacKay, J., Reif, M., Bao, L., Brown III, J.F., Mattina, M., Miao, C.-C., Ramey, C., Wentzlaff, D., Anderson, W., Berger, E., Fairbanks, N., Khan, D., Montenegro, F., Stickney, J., Zook, J.: TILE64 - processor: a 64-core soc with mesh interconnect. In: 2008 IEEE International Solid-State Circuits Conference, ISSCC 2008, Digest of Technical Papers, San Francisco, CA, USA, 3–7 February 2008, pp. 88–89. IEEE (2008) Bell, S., Edwards, B., Amann, J., Conlin, R., Joyce, K., Leung, V., MacKay, J., Reif, M., Bao, L., Brown III, J.F., Mattina, M., Miao, C.-C., Ramey, C., Wentzlaff, D., Anderson, W., Berger, E., Fairbanks, N., Khan, D., Montenegro, F., Stickney, J., Zook, J.: TILE64 - processor: a 64-core soc with mesh interconnect. In: 2008 IEEE International Solid-State Circuits Conference, ISSCC 2008, Digest of Technical Papers, San Francisco, CA, USA, 3–7 February 2008, pp. 88–89. IEEE (2008)
5.
go back to reference Bodden, E., Tolêdo, T., Ribeiro, M., Brabrand, C., Borba, P., Mezini, M.: Spl\({}^{\text{lift}}\): statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 355–364. ACM (2013) Bodden, E., Tolêdo, T., Ribeiro, M., Brabrand, C., Borba, P., Mezini, M.: Spl\({}^{\text{lift}}\): statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 355–364. ACM (2013)
6.
go back to reference Brekling, A.W., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Logic Algebraic Program. 77(1–2), 1–19 (2008)MathSciNetCrossRefMATH Brekling, A.W., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Logic Algebraic Program. 77(1–2), 1–19 (2008)MathSciNetCrossRefMATH
7.
go back to reference Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: Family-based modeling and analysis for probabilistic systems – featuring ProFeat. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 287–304. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49665-7_17 CrossRef Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: Family-based modeling and analysis for probabilistic systems – featuring ProFeat. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 287–304. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49665-7_​17 CrossRef
8.
go back to reference Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013)CrossRef Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013)CrossRef
9.
go back to reference Cordy, M., Classen, A., Heymans, P., Schobbens, P., Legay, A.: ProVeLines: a product line of verifiers for software product lines. In: 17th International Software Product Line Conference Co-located workshops (SPLC), pp. 141–146. ACM (2013) Cordy, M., Classen, A., Heymans, P., Schobbens, P., Legay, A.: ProVeLines: a product line of verifiers for software product lines. In: 17th International Software Product Line Conference Co-located workshops (SPLC), pp. 141–146. ACM (2013)
10.
go back to reference Damiani, F., Schaefer, I.: Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 193–207. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34026-0_15 CrossRef Damiani, F., Schaefer, I.: Family-based analysis of type safety for delta-oriented software product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 193–207. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-34026-0_​15 CrossRef
11.
go back to reference Dastgeer, U., Kessler, C.W.: Performance-aware composition framework for GPU-based systems. J. Supercomput. 71(12), 4646–4662 (2015)CrossRef Dastgeer, U., Kessler, C.W.: Performance-aware composition framework for GPU-based systems. J. Supercomput. 71(12), 4646–4662 (2015)CrossRef
12.
go back to reference Devroey, X., Perrouin, G., Cordy, M., Samih, H., Legay, A., Schobbens, P., Heymans, P.: Statistical prioritization for software product line testing: an experience report. Softw. Syst. Model. 16(1), 153–171 (2017)CrossRef Devroey, X., Perrouin, G., Cordy, M., Samih, H., Legay, A., Schobbens, P., Heymans, P.: Statistical prioritization for software product line testing: an experience report. Softw. Syst. Model. 16(1), 153–171 (2017)CrossRef
13.
go back to reference Donaldson, A.F., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 280–295. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_24 CrossRef Donaldson, A.F., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 280–295. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-12002-2_​24 CrossRef
14.
go back to reference Dubslaff, C., Baier, C., Klüppelholz, S.: Probabilistic model checking for feature-oriented systems. Trans. Asp.-Oriented Softw. Dev. 12, 180–220 (2015) Dubslaff, C., Baier, C., Klüppelholz, S.: Probabilistic model checking for feature-oriented systems. Trans. Asp.-Oriented Softw. Dev. 12, 180–220 (2015)
15.
go back to reference Wentzlaff, D., Griffin, P., Hoffmann, H., Bao, L., Edwards, B., Ramey, C., Mattina, M., Miao, C.-C., Brown III, J.F., Agarwal, A.: On-chip interconnection architecture of the tile processor. IEEE Micro 27, 15–31 (2007)CrossRef Wentzlaff, D., Griffin, P., Hoffmann, H., Bao, L., Edwards, B., Ramey, C., Mattina, M., Miao, C.-C., Brown III, J.F., Agarwal, A.: On-chip interconnection architecture of the tile processor. IEEE Micro 27, 15–31 (2007)CrossRef
16.
go back to reference Gries, M., Hoffmann, U., Konow, M., Riepen, M.: SCC: a flexible architecture for many-core platform research. Comput. Sci. Eng. 13(6), 79–83 (2011)CrossRef Gries, M., Hoffmann, U., Konow, M., Riepen, M.: SCC: a flexible architecture for many-core platform research. Comput. Sci. Eng. 13(6), 79–83 (2011)CrossRef
17.
go back to reference Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_47 CrossRef Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​47 CrossRef
18.
go back to reference Lungu, A., Bose, P., Sorin, D.J., German, S., Janssen, G.: Multicore power management: ensuring robustness via early-stage formal verification. In: 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 78–87. IEEE (2009) Lungu, A., Bose, P., Sorin, D.J., German, S., Janssen, G.: Multicore power management: ensuring robustness via early-stage formal verification. In: 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 78–87. IEEE (2009)
19.
go back to reference Paolucci, P.S., Jerraya, A.A., Leupers, R., Thiele, L., Vicini, P.: SHAPES: a tiled scalable software hardware architecture platform for embedded systems. In: 4th International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pp. 167–172. ACM (2006) Paolucci, P.S., Jerraya, A.A., Leupers, R., Thiele, L., Vicini, P.: SHAPES: a tiled scalable software hardware architecture platform for embedded systems. In: 4th International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pp. 167–172. ACM (2006)
20.
go back to reference Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham (2002) Parker, D.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham (2002)
22.
go back to reference Smit, G.J.M., Kokkeler, A.B.J., Wolkotte, P.T., Hölzenspies, P.K.F., van de Burgwal, M.D., Heysters, P.M.: The chameleon architecture for streaming DSP applications. EURASIP J. Embed. Syst. 2007 (2007). Article ID 078082 Smit, G.J.M., Kokkeler, A.B.J., Wolkotte, P.T., Hölzenspies, P.K.F., van de Burgwal, M.D., Heysters, P.M.: The chameleon architecture for streaming DSP applications. EURASIP J. Embed. Syst. 2007 (2007). Article ID 078082
23.
go back to reference Taylor, M.B., Kim, J., Miller, J., Wentzlaff, D., Ghodrat, F., Greenwald, B., Hoffman, H., Johnson, P., Lee, J.-W., Lee, W., Ma, A., Saraf, A., Seneski, M., Shnidman, N., Strumpen, V., Frank, M., Amarasinghe, S., Agarwal, A.: The raw microprocessor: a computational fabric for software circuits and general-purpose programs. IEEE Micro 22(2), 25–35 (2002)CrossRef Taylor, M.B., Kim, J., Miller, J., Wentzlaff, D., Ghodrat, F., Greenwald, B., Hoffman, H., Johnson, P., Lee, J.-W., Lee, W., Ma, A., Saraf, A., Seneski, M., Shnidman, N., Strumpen, V., Frank, M., Amarasinghe, S., Agarwal, A.: The raw microprocessor: a computational fabric for software circuits and general-purpose programs. IEEE Micro 22(2), 25–35 (2002)CrossRef
24.
go back to reference ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: 19th International Conference on Software Product Line (SPLC), pp. 432–439. ACM (2015) ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: 19th International Conference on Software Product Line (SPLC), pp. 432–439. ACM (2015)
25.
go back to reference ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114–133. Springer, Cham (2016). doi:10.1007/978-3-319-47166-2_8 CrossRef ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114–133. Springer, Cham (2016). doi:10.​1007/​978-3-319-47166-2_​8 CrossRef
26.
go back to reference Thüm, T.: Product-line specification and verification with feature-oriented contracts. Ph.D. thesis, Otto von Guericke University Magdeburg (2015) Thüm, T.: Product-line specification and verification with feature-oriented contracts. Ph.D. thesis, Otto von Guericke University Magdeburg (2015)
27.
go back to reference Thüm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: Generative Programming and Component Engineering (GPCE), pp. 11–20. ACM (2012) Thüm, T., Schaefer, I., Hentschel, M., Apel, S.: Family-based deductive verification of software product lines. In: Generative Programming and Component Engineering (GPCE), pp. 11–20. ACM (2012)
28.
29.
go back to reference Velev, M.N., Gao, P.: Formal verification of safety of polymorphic heterogeneous multi-core architectures. In: 15th International Symposium on Quality Electronic Design (ISQED), pp. 611–617. IEEE (2014) Velev, M.N., Gao, P.: Formal verification of safety of polymorphic heterogeneous multi-core architectures. In: 15th International Symposium on Quality Electronic Design (ISQED), pp. 611–617. IEEE (2014)
30.
go back to reference Völp, M., Klüppelholz, S., Castrillon, J., Härtig, H., Asmussen, N., Aßmann, U., Baader, F., Baier, C., Fettweis, G., Fröhlich, J., Goens, A., Haas, S., Habich, D., Hasler, M., Huismann, I., Karnagel, T., Karol, S., Lehner, W., Leuschner, L., Lieber, M., Ling, S., Märcker, S., Mey, J., Nagel, W., Nöthen, B., Penaloza, R., Raitza, M., Stiller, J., Ungethüm, A., Voigt, A.: The orchestration stack: the impossible task of designing software for unknown future post-CMOS hardware. In: Proceedings of the 1st Workshop on Post-Moore’s Era Supercomputing (PMES) (2016, accepted for publication) Völp, M., Klüppelholz, S., Castrillon, J., Härtig, H., Asmussen, N., Aßmann, U., Baader, F., Baier, C., Fettweis, G., Fröhlich, J., Goens, A., Haas, S., Habich, D., Hasler, M., Huismann, I., Karnagel, T., Karol, S., Lehner, W., Leuschner, L., Lieber, M., Ling, S., Märcker, S., Mey, J., Nagel, W., Nöthen, B., Penaloza, R., Raitza, M., Stiller, J., Ungethüm, A., Voigt, A.: The orchestration stack: the impossible task of designing software for unknown future post-CMOS hardware. In: Proceedings of the 1st Workshop on Post-Moore’s Era Supercomputing (PMES) (2016, accepted for publication)
31.
go back to reference Wilhelm, R., Reineke, J.: Embedded systems: many cores - many problems. In: 7th IEEE International Symposium on Industrial Embedded Systems (SIES), pp. 176–180. IEEE (2012) Wilhelm, R., Reineke, J.: Embedded systems: many cores - many problems. In: 7th IEEE International Symposium on Industrial Embedded Systems (SIES), pp. 176–180. IEEE (2012)
Metadata
Title
Towards Automated Variant Selection for Heterogeneous Tiled Architectures
Authors
Christel Baier
Sascha Klüppelholz
Sascha Wunderlich
Copyright Year
2017
DOI
https://doi.org/10.1007/978-3-319-63121-9_19

Premium Partner