Document Open Access Logo

Modeling Cache Coherence to Expose Interference

Authors Nathanaël Sensfelder, Julien Brunel, Claire Pagetti

PDF
Thumbnail PDF

File

LIPIcs.ECRTS.2019.18.pdf
  • Filesize: 1.24 MB
  • 22 pages

Document Identifiers

Author Details

Nathanaël Sensfelder
  • ONERA, Toulouse, France
Julien Brunel
  • ONERA, Toulouse, France
Claire Pagetti
  • ONERA, Toulouse, France

Acknowledgements

We would like to thank Mamoun Filali-Amine (IRIT-CNRS) for his helpful insights on how to validate our model and related works suggestions.

Cite As Get BibTex

Nathanaël Sensfelder, Julien Brunel, and Claire Pagetti. Modeling Cache Coherence to Expose Interference. In 31st Euromicro Conference on Real-Time Systems (ECRTS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 133, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ECRTS.2019.18

Abstract

To facilitate programming, most multi-core processors feature automated mechanisms maintaining coherence between each core’s cache. These mechanisms introduce interference, that is, delays caused by concurrent access to a shared resource. This type of interference is hard to predict, leading to the mechanisms being shunned by real-time system designers, at the cost of potential benefits in both running time and system complexity.
We believe that formal methods can provide the means to ensure that the effects of this interference are properly exposed and mitigated. Consequently, this paper proposes a nascent framework relying on timed automata to model and analyze the interference caused by cache coherence.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Multicore architectures
  • Computer systems organization → Real-time systems
Keywords
  • Real-time systems
  • multi-core processor
  • cache coherence
  • formal methods

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theor. Comput. Sci., 126(2):183-235, April 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90010-8.
  2. James Archibald and Jean-Loup Baer. Cache Coherence Protocols: Evaluation Using a Multiprocessor Simulation Model. ACM Trans. Comput. Syst., 4(4):273-298, September 1986. URL: http://dx.doi.org/10.1145/6513.6514.
  3. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Handbook of Satisfiability, chapter Satisfiability Modulo Theories, pages 825-885. IOS Press, 2009. Google Scholar
  4. Gerd Behrmann, Alexandre David, and Kim G. Larsen. A Tutorial on Uppaal, pages 200-236. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30080-9_7.
  5. Frédéric Boniol, Hugues Cassé, Eric Noulard, and Claire Pagetti. Deterministic Execution Model on COTS Hardware. In Proceedings of the 25th International Conference on Architecture of Computing Systems (ARCS'12), pages 98-110, 2012. Google Scholar
  6. Franck Cassez and Jean-Luc Béchennec. Timing Analysis of Binary Programs with UPPAAL. In 13th International Conference on Application of Concurrency to System Design, ACSD 2013, pages 41-50. IEEE Computer Society, July 2013. URL: http://dx.doi.org/10.1109/ACSD.2013.7.
  7. Franck Cassez and Pablo González de Aledo Marugán. Timed Automata for Modelling Caches and Pipelines. In Rob J. van Glabbeek, Jan Friso Groote, and Peter Höfner, editors, Proceedings Workshop on Models for Formal Analysis of Real Systems, MARS 2015, Suva, Fiji, November 23, 2015., volume 196 of EPTCS, pages 37-45, 2015. URL: http://dx.doi.org/10.4204/EPTCS.196.4.
  8. Sudipta Chattopadhyay, Abhik Roychoudhury, and Tulika Mitra. Modeling Shared Cache and Bus in Multi-cores for Timing Analysis. In Proceedings of the 13th International Workshop on Software &Compilers for Embedded Systems, SCOPES '10, pages 6:1-6:10, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1811212.1811220.
  9. Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen. METAMOC: Modular Execution Time Analysis using Model Checking. In Björn Lisper, editor, 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010), volume 15 of OpenAccess Series in Informatics (OASIcs), pages 113-123, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. The printed version of the WCET'10 proceedings are published by OCG (www.ocg.at) - ISBN 978-3-85403-268-7. URL: http://dx.doi.org/10.4230/OASIcs.WCET.2010.113.
  10. Giorgio Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proceedings of the 12th International Conference on Computer Aided Verification, CAV '00, pages 53-68, London, UK, UK, 2000. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=647769.734088.
  11. Philip Enslow, Jr. Multiprocessor Organization - a Survey. ACM Comput. Surv., 9(1):103-129, March 1977. Google Scholar
  12. Sylvain Girbal, Xavier Jean, Jimmy le Rhun, Daniel Gracia Pérez, and Marc Gatti. Deterministic Platform Software for Hard Real-Time systems using multi-core COTS. In 34th Digital Avionics Systems Conference (DASC'15), 2015. Google Scholar
  13. Andreas Gustavsson, Andreas Ermedahl, Björn Lisper, and Paul Pettersson. Towards WCET Analysis of Multicore Architectures Using UPPAAL. In 10th International Workshop on Worst-Case Execution Time Analysis, WCET 2010, July 6, 2010, Brussels, Belgium, pages 101-112, 2010. URL: http://dx.doi.org/10.4230/OASIcs.WCET.2010.101.
  14. Mohamed Hassan, Anirudh M. Kaushik, and Hiren D. Patel. Predictable Cache Coherence for Multi-core Real-Time Systems. In 2017 IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2017, Pittsburg, PA, USA, April 18-21, 2017, pages 235-246, 2017. URL: http://dx.doi.org/10.1109/RTAS.2017.13.
  15. Xavier Jean, David Faura, Marc Gatti, Laurent Pautet, and Thomas Robert. Ensuring robust partitioning in multicore platforms for IMA systems. In 31st Digital Avionics Systems Conference (DASC'16), 2012. Google Scholar
  16. M. Lv, W. Yi, N. Guan, and G. Yu. Combining Abstract Interpretation with Model Checking for Timing Analysis of Multicore Software. In 2010 31st IEEE Real-Time Systems Symposium, pages 339-349, November 2010. URL: http://dx.doi.org/10.1109/RTSS.2010.30.
  17. Claire Maiza, Hamza Rihani, Juan Maria Rivas, Joël, Godelieve Goossens, Sebastian Altmeyer, and Robert I. Davis. A Survey of Timing Verification Techniques for Multi-Core Real-Time Systems. Technical report, Grenoble INP/Ensimag/Verimag, 2018. Google Scholar
  18. Rodolfo Pellizzoni, Emiliano Betti, Stanley Bak, Gang Yao, John Criswell, Marco Caccamo, and Russell Kegley. A Predictable Execution Model for COTS-Based Embedded Systems. In 17th IEEE Real-Time and Embedded Technology and Applications Symposium RTAS 2011, pages 269-279, 2011. Google Scholar
  19. Fong Pong and Michel Dubois. A New Approach for the Verification of Cache Coherence Protocols. IEEE Trans. Parallel Distrib. Syst., 6(8):773-787, August 1995. URL: http://dx.doi.org/10.1109/71.406955.
  20. Daniel J. Sorin, Mark D. Hill, and David A. Wood. A Primer on Memory Consistency and Cache Coherence. Morgan &Claypool Publishers, 1st edition, 2011. Google Scholar
  21. Nivedita Sritharan, Anirudh M. Kaushik, Mohamed Hassan, and Hiren D. Patel. HourGlass: Predictable Time-based Cache Coherence Protocol for Dual-Critical Multi-Core Systems. CoRR, abs/1706.07568, 2017. URL: http://arxiv.org/abs/1706.07568.
  22. V. Suhendra, T. Mitra, and A. Roychoudhury and. WCET centric data allocation to scratchpad memory. In 26th IEEE International Real-Time Systems Symposium (RTSS'05), pages 10 pp.-232, December 2005. URL: http://dx.doi.org/10.1109/RTSS.2005.45.
  23. Texas Instruments. TCI6630K2L Multicore DSP+ARM KeyStone II System-on-Chip. Technical Report SPRS893E, Texas Instruments Incorporated, 2013. Google Scholar
  24. Sascha Uhrig, Lillian Tadros, and Arthur Pyka. MESI-Based Cache Coherence for Hard Real-Time Multicore Systems. In Luís Miguel Pinho Pinho, Wolfgang Karl, Albert Cohen, and Uwe Brinkschulte, editors, Architecture of Computing Systems - ARCS 2015, pages 212-223, Cham, 2015. Springer International Publishing. Google Scholar
  25. L. Wehmeyer and P. Marwedel. Influence of memory hierarchies on predictability for time constrained embedded software. In Design, Automation and Test in Europe, pages 600-605 Vol. 1, March 2005. URL: http://dx.doi.org/10.1109/DATE.2005.183.
  26. Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter Puschner, Jan Staschulat, and Per Stenström. The Worst-case Execution-time Problem - Overview of Methods and Survey of Tools. ACM Transactions Embedded Computing Systems, 7(3):36:1-36:53, May 2008. Google Scholar
  27. Reinhard Wilhelm and Jan Reineke. Embedded systems: Many cores - Many problems. In 7th IEEE International Symposium on Industrial Embedded Systems (SIES'12), pages 176-180, 2012. Google Scholar
  28. Heechul Yun, Gang Yao, Rodolfo Pellizzoni, Marco Caccamo, and Lui Sha. MemGuard: Memory bandwidth reservation system for efficient performance isolation in multi-core platforms. In 19th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS'13), pages 55-64, 2013. Google Scholar
  29. Wei Zhang and Jun Yan. Static Timing Analysis of Shared Caches for Multicore Processors. JCSE, 6(4):267-278, 2012. URL: http://dx.doi.org/10.5626/JCSE.2012.6.4.267.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact