nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego

verfasst von : Waheed Ahmad, Jaco van de Pol

Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Streaming applications for mobile platforms impose high demands on a system’s throughput and energy consumption. Dynamic system-level techniques have been introduced, to reduce power consumption at the expense of performance. We consider DPM (Dynamic Power Management) and DVFS (Dynamic Voltage and Frequency Scaling). The complex programming task now includes mapping and scheduling every task onto a heterogeneous multi-processor hardware platform. Moreover, DPM and DVFS parameters must be controlled, to meet all throughput constraints while minimizing the energy consumption.

Previous work proposed to automate this process, by modeling streaming applications in SDF (Synchronous Data Flow), modeling the processor platform, translating both models to PTA (Priced Timed Automata, where prices model energy), and using Uppaal Cora to compute energy-optimal schedules that adhere to the throughput constraints.

In this paper, we experiment with an alternative approach, based on stochastic hybrid games. We investigate the applicability of Uppaal Stratego to first synthesize a permissive controller satisfying a throughput constraint, and then select a near-optimal strategy that additionally minimizes the energy consumption. Our goal is to compare the Uppaal Cora and Uppaal Stratego approaches in terms of modeling effort, results and computation times, and to reveal potential limitations.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Plasma Lab: A Modular Statistical Model Checking Platform

Nächstes Kapitel Statistical Model Checking for Product Lines

Ahmad, W., de Groote, R., Hölzenspies, P.K.F., Stoelinga, M., van de Pol, J.: Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. In: Proceedings of 14th International Conference on Application of Concurrency to System Design, (ACSD), pp. 72–81 (2014)

Ahmad, W., Hölzenspies, P.K.F., Stoelinga, M., van de Pol, J.: Green computing: power optimisation of VFI-based real-time multiprocessor dataflow applications. In: Proceedings of 18th Euromicro Conference on Digital Systems Design (DSD), pp. 271–275 (2015)

Ahmad, W., Jongerden, M., Stoelinga, M., van de Pol, J.: Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. In: Proceedings of 16th International Conference on Application of Concurrency to System Design (ACSD), pp. 114–123 (2016)

Ahmad, W., Yildiz, B.M., Rensink, A., Stoelinga, M.: Evaluating the tools on the face detection and recognition case study, Chap. 2, pp. 4–6. FP7 EU Project SENSATION, Deliverable D1.4 (2016)

Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRefMATH

Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRef

Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. SIGMETRICS Perform. Eval. Rev. 32(4), 34–40 (2005)CrossRef

Benini, L., Bogliolo, A., Micheli, G.D.: A survey of design techniques for system-level dynamic power management. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 8(3), 299–316 (2000)CrossRef

Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). doi:10.1007/11539452_9 CrossRef

10.

David, A., Du, D., Larsen, K.G., Legay, A., Mikučionis, M., Bøgsted Poulsen, D., Sedwards, S.: Statistical model checking for stochastic hybrid systems. ArXiv e-prints (2012)

11.

David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., Sørensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129–145. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11936-6_10

12.

David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206–211. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_16

13.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015)CrossRef

14.

Devadas, V., Aydin, H.: On the interplay of voltage/frequency scaling and device power management for frame-based real-time embedded applications. IEEE Trans. Comput. 61(1), 31–44 (2012)MathSciNetCrossRef

15.

Gerards, M.E.T., Hurink, J.L., Kuper, J.: On the interplay between global DVFS and scheduling tasks with precedence constraints. IEEE Trans. Comput. 64, 1742–1754 (2014)MathSciNet

16.

Han, J.J., Wu, X., Zhu, D., Jin, H., Yang, L.T., Gaudiot, J.L.: Synchronization-aware energy management for VFI-based multicore real-time systems. IEEE Trans. Comput. 61(12), 1682–1696 (2012)MathSciNetCrossRef

17.

Henzinger, T.: The theory of hybrid automata. In: Proceedings of Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 278–292 (1996)

18.

Herbert, S., Marculescu, D.: Analysis of dynamic voltage/frequency scaling in chip-multiprocessors. In: Proceedings of ACM/IEEE International Symposium on Low Power Electronics and Design (ISLPED), pp. 38–43 (2007)

19.

Irani, S., Pruhs, K.R.: Algorithmic problems in power management. ACM SIGACT News 36(2), 63–76 (2005)CrossRef

20.

Katoen, J.-P., Wu, H., Exponentially timed SADF: compositional semantics, reductions, and analysis. In: Proceedings of 14th ACM/IEEE International Conference on Embedded Software (EMSOFT), pp. 1:1–1:10 (2014)

21.

Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987)CrossRef

22.

Manwell, J.F., McGowan, J.G.: Lead acid battery storage model for hybrid energy systems. Sol. Energy 50(5), 399–405 (1993)CrossRef

23.

March, J.L., Sahuquillo, J., Hassan, H., Petit, S., Duato, J.: A new energy-aware dynamic task set partitioning algorithm for soft and hard embedded real-time systems. Comput. J. 54(8), 1282–1294 (2011)CrossRef

24.

Nelson, A., Moreira, O., Molnos, A., Stuijk, S., Nguyen, B.T., Goossens, K.: Power minimisation for real-time dataflow applications. In: Proceedings of 14th Euromicro Conference on Digital System Design (DSD), pp. 117–124 (2011)

25.

Park, S., Park, J., Shin, D., Wang, Y., Xie, Q., Pedram, M., Chang, N.: Accurate modeling of the delay and energy overhead of dynamic voltage and frequency scaling in modern microprocessors. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 32(5), 695–708 (2013)CrossRef

26.

ter Braak, T.D., Sunesen, K., Ahmad, W., Stoelinga, M., van de Pol, J., Katoen, J.-P., Wu, H.: Evaluating the tools on the face detection and recognition case study, Chap. 2, pp. 6–23. FP7 EU Project SENSATION, Deliverable D4.4 (2016)

27.

Theelen, B., Geilen, M., Basten, T., Voeten, J., Gheorghita, S., Stuijk, S.: A scenario-aware data flow model for combined long-run average and worst-case performance analysis. In: Proceedings of 4th ACM/IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE), pp. 185–194 (2006)

28.

Weiser, M., Welch, B., Demers, A., Shenker, S.: Scheduling for reduced CPU energy. In: Proceedings of 1st USENIX Conference on Operating Systems Design and Implementation (1994)

29.

Wognsen, E.R., Haverkort, B.R., Jongerden, M., Hansen, R.R., Larsen, K.G.: A score function for optimizing the cycle-life of battery-powered embedded systems. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 305–320. Springer, Heidelberg (2015). doi:10.1007/978-3-319-22975-1_20 CrossRef

30.

Yang, Y., Geilen, M., Basten, T., Stuijk, S., Corporaal, H.: Playing games with scenario- and resource-aware SDF graphs through policy iteration. In: Proceedings of Design, Automation and Test in Europe (DATE), pp. 194–199 (2012)

31.

Zhu, J., Sander, I., Jantsch, A.: Energy efficient streaming applications with guaranteed throughput on MPSoCs. In: Proceedings of 8th ACM/IEEE International Conference on Embedded Software (EMSOFT), pp. 119–128 (2008)

32.

Zhuravlev, S., Saez, J.C., Blagodurov, S., Fedorova, A., Prieto, M.: Survey of energy-cognizant scheduling techniques. IEEE Trans. Parallel Distrib. Syst. 24(7), 1447–1464 (2013)CrossRef

Titel: Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego
verfasst von: Waheed Ahmad
Jaco van de Pol
Verlag: Springer International Publishing
Buch: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques
Print ISBN: 978-3-319-47165-5

Electronic ISBN: 978-3-319-47166-2

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-47166-2_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"