Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego | SpringerLink
Skip to main content
Springer Nature Link
Log in

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

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9952))

Included in the following conference series:

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.

This research is supported by the EU FP7 project SENSATION (318490).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 11439
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 14299
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. 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)

    Google Scholar 

  2. 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)

    Google Scholar 

  3. 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)

    Google Scholar 

  4. 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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  8. 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)

    Article  Google Scholar 

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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

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

    Article  Google Scholar 

  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)

    Google Scholar 

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

    Article  Google Scholar 

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

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Article  Google Scholar 

Download references

Acknowledgement

The authors are grateful to Jakob Haahr Taankvist and Peter Gjøl Jensen for their valuable help to understand Uppaal Stratego. The authors would also like to thank the anonymous reviewers for their helpful and constructive comments that greatly contributed to improving the final version of the paper.

Author information

Authors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Waheed Ahmad & Jaco van de Pol

Authors
  1. Waheed Ahmad
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Waheed Ahmad .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Ahmad, W., van de Pol, J. (2016). Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego . In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47166-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47165-5

  • Online ISBN: 978-3-319-47166-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation