Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 3/2022

11-04-2022 | General

Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture

Authors: Benjamin Binder, Mihail Asavoae, Florian Brandner, Belgacem Ben Hedia, Mathieu Jan

Published in: International Journal on Software Tools for Technology Transfer | Issue 3/2022

Log in

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

search-config
loading …

Abstract

Static worst-case timing analyses compute safe timing bounds of applications running in real-time systems. These bounds are necessary to evaluate the strict timing constraints of real-time systems. Moreover, the inherent complexity of such systems demands that their timing analyses are able to cope with the large resulting state space. In this direction, a potential solution is to perform compositional timing analysis, where the system-level timing is obtained from component-level timings. Undesired timing phenomena, called timing anomalies, threaten the soundness of (compositional) timing analyses. In this work, we investigate how the industrial superscalar TriCore architecture is amenable for compositional timing analyses via a formal evaluation of amplification timing anomalies. Firstly, we adapt and extend a specialized abstraction, called canonical pipeline model, to capture the amplification effects in a formal model of the TriCore architecture. Then, we use model checking to efficiently detect amplification timing anomalies and report the associated complexity results. Finally, we aim for better precision as we design and implement counterexample-based methods so as to uncover patterns leading to such anomalies.

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
2
In this paper, we note an interpretation for which a formula is true an SMT model to distinguish it from our pipeline models.
 
3
It cannot interfere with the up.I instruction since both instructions may only access the PMI in the IF stage.
 
4
This will be refined in Sect. 5.3.3 by taking into account the case of dependent loads (Formula (26)).
 
5
For instance, the memdep attribute globally characterizes two instructions.
 
6
This delay \(delay\_dw\) is here actually a tuple (one delay per I or LS downstream instruction) and a positive delay value is a tuple different from the \(null\_delay=(0,0)\).
 
8
With the only-upstream progression logic however (see Sect. 7.1.1).
 
9
Just before the EX stage where the SRI bus access will occur through the DMI (Sect. 5.2).
 
10
Note that the converse is not true, as mentioned above.
 
11
Namely, the same scenario if we omit the pipeline stages that are not responsible for the delay scenario.
 
Literature
1.
go back to reference Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 270–288. Springer International Publishing, Cham (2018)CrossRef Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 270–288. Springer International Publishing, Cham (2018)CrossRef
2.
go back to reference Asavoae, M., Ben Hedia, B., Jan, M.: Formal executable models for automatic detection of timing anomalies. In: 18th International Workshop on Worst-Case Execution Time Analysis (WCET), Barcelona, Spain, pp. 2:1–2:13, (2018) Asavoae, M., Ben Hedia, B., Jan, M.: Formal executable models for automatic detection of timing anomalies. In: 18th International Workshop on Worst-Case Execution Time Analysis (WCET), Barcelona, Spain, pp. 2:1–2:13, (2018)
3.
go back to reference Ballabriga, C., Cassé, H., Rochange, C., Sainrat, P.: OTAWA: an open toolbox for adaptive WCET analysis. In: SEUS 2010. pp. 35–46 (2010) Ballabriga, C., Cassé, H., Rochange, C., Sainrat, P.: OTAWA: an open toolbox for adaptive WCET analysis. In: SEUS 2010. pp. 35–46 (2010)
4.
go back to reference Barrett, C., Tinelli, C.: Satisfiability modulo theories, pp. 305–343. Springer International Publishing, Cham (2018). 10.1007/978-3-319-10575-8_11, Barrett, C., Tinelli, C.: Satisfiability modulo theories, pp. 305–343. Springer International Publishing, Cham (2018). 10.1007/978-3-319-10575-8_11,
5.
go back to reference Binder, B., Asavoae, M., Brandner, F., Ben Hedia, B., Jan, M.: Scalable detection of amplification timing anomalies for the superscalar tricore architecture. In: ter Beek, M.H., Ničković, D. (eds.) Formal Methods for Industrial Critical Systems, pp. 151–169. Springer International Publishing, Cham (2020)CrossRef Binder, B., Asavoae, M., Brandner, F., Ben Hedia, B., Jan, M.: Scalable detection of amplification timing anomalies for the superscalar tricore architecture. In: ter Beek, M.H., Ničković, D. (eds.) Formal Methods for Industrial Critical Systems, pp. 151–169. Springer International Publishing, Cham (2020)CrossRef
7.
go back to reference Brady, B.A., Holcomb, D., Seshia, S.A.: Counterexample-guided smt-driven optimal buffer sizing. In: 2011 Design, Automation Test in Europe. pp. 1–6 (2011). 10.1109/DATE.2011.5763058 Brady, B.A., Holcomb, D., Seshia, S.A.: Counterexample-guided smt-driven optimal buffer sizing. In: 2011 Design, Automation Test in Europe. pp. 1–6 (2011). 10.1109/DATE.2011.5763058
8.
go back to reference de Dinechin, B.D., van Amstel, D., Poulhiès, M., Lager, G.: Time-critical computing on a single-chip massively parallel processor. In: Proceedings of the Conference on Design, Automation & Test in Europe (DATE’14). pp. 97:1–97:6 (2014) de Dinechin, B.D., van Amstel, D., Poulhiès, M., Lager, G.: Time-critical computing on a single-chip massively parallel processor. In: Proceedings of the Conference on Design, Automation & Test in Europe (DATE’14). pp. 97:1–97:6 (2014)
9.
go back to reference Eisinger, J., Polian, I., Becker, B., Metzner, A., Thesing, S., Wilhelm, R.: Automatic identification of timing anomalies for cycle-accurate worst-case execution time analysis. In: Proceedings of the Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS). Prague, Czech Republic, pp. 15–20. (2006) Eisinger, J., Polian, I., Becker, B., Metzner, A., Thesing, S., Wilhelm, R.: Automatic identification of timing anomalies for cycle-accurate worst-case execution time analysis. In: Proceedings of the Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS). Prague, Czech Republic, pp. 15–20. (2006)
10.
go back to reference Hahn, S., Reineke, J.: Design and analysis of sic: A provably timing-predictable pipelined processor core. In: 2018 IEEE Real-Time Systems Symposium (RTSS). pp. 469–481 (2018) Hahn, S., Reineke, J.: Design and analysis of sic: A provably timing-predictable pipelined processor core. In: 2018 IEEE Real-Time Systems Symposium (RTSS). pp. 469–481 (2018)
11.
go back to reference Hahn, S., Jacobs, M., Reineke, J.: Enabling compositionality for multicore timing analysis. In: Plantec, A., Singhoff, F., Faucou, S., Pinho, L.M. (eds.) Proceedings of the 24th International Conference on Real-Time Networks and Systems, RTNS 2016, Brest, France, October 19-21, 2016. pp. 299–308. ACM (2016) Hahn, S., Jacobs, M., Reineke, J.: Enabling compositionality for multicore timing analysis. In: Plantec, A., Singhoff, F., Faucou, S., Pinho, L.M. (eds.) Proceedings of the 24th International Conference on Real-Time Networks and Systems, RTNS 2016, Brest, France, October 19-21, 2016. pp. 299–308. ACM (2016)
12.
go back to reference Hahn, S., Reineke, J., Wilhelm, R.: Towards compositionality in execution time analysis: Definition and challenges. SIGBED Rev. 12(1), 28–36 (2015)CrossRef Hahn, S., Reineke, J., Wilhelm, R.: Towards compositionality in execution time analysis: Definition and challenges. SIGBED Rev. 12(1), 28–36 (2015)CrossRef
13.
go back to reference Hennessy, J.L., Patterson, D.A.: Computer architecture - A quantitative approach, 5th Edition. Morgan Kaufmann (2012) Hennessy, J.L., Patterson, D.A.: Computer architecture - A quantitative approach, 5th Edition. Morgan Kaufmann (2012)
14.
go back to reference Infineon Technologies AG: Architecture Overview Handbook, TriCore 1.3, 32-bit Unified Processor Core, IP Cores (05 2002) Infineon Technologies AG: Architecture Overview Handbook, TriCore 1.3, 32-bit Unified Processor Core, IP Cores (05 2002)
15.
go back to reference Infineon technologies AG: TriCore 1 pipeline behaviour and instruction execution timing (2004) Infineon technologies AG: TriCore 1 pipeline behaviour and instruction execution timing (2004)
16.
go back to reference Infineon Technologies AG: AURIX TC21x/TC22x/TC23x Family 32-Bit Single-Chip Microcontroller User’s Manual (12 2014) Infineon Technologies AG: AURIX TC21x/TC22x/TC23x Family 32-Bit Single-Chip Microcontroller User’s Manual (12 2014)
17.
go back to reference Jan, M., Asavoae, M., Schoeberl, M., Lee, E.: Formal semantics of predictable pipelines: a comparative study. In: Proceedings of the 25th Asia and South Pacific Design Automation Conference. IEEE, United States (2020) Jan, M., Asavoae, M., Schoeberl, M., Lee, E.: Formal semantics of predictable pipelines: a comparative study. In: Proceedings of the 25th Asia and South Pacific Design Automation Conference. IEEE, United States (2020)
18.
go back to reference Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings. pp. 142–159 (2002) Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings. pp. 142–159 (2002)
19.
go back to reference Lauterbach GmbH: Simulator for TriCore (04 2021) Lauterbach GmbH: Simulator for TriCore (04 2021)
20.
go back to reference Liu, I., Reineke, J., Lee, E.A.: A PRET architecture supporting concurrent programs with composable timing properties. In: 44th Asilomar Conference on Signals, Systems, and Computers (November 2010) Liu, I., Reineke, J., Lee, E.A.: A PRET architecture supporting concurrent programs with composable timing properties. In: 44th Asilomar Conference on Signals, Systems, and Computers (November 2010)
21.
go back to reference Lundqvist, T., Stenström, P.: Timing anomalies in dynamically scheduled microprocessors. In: Real-Time Systems Symposium. pp. 12–21. RTSS’99, IEEE (1999). 10.1109/REAL.1999.818824 Lundqvist, T., Stenström, P.: Timing anomalies in dynamically scheduled microprocessors. In: Real-Time Systems Symposium. pp. 12–21. RTSS’99, IEEE (1999). 10.1109/REAL.1999.818824
22.
go back to reference Nguyen, V.a., Jenn, E., Serwe, W., Lang, F., Mateescu, R.: Using model checking to identify timing interferences on multicore processors. In: ERTS 2020 - 10th European Congress on Embedded Real Time Software and Systems. pp. 1–10. Toulouse, France (2020) Nguyen, V.a., Jenn, E., Serwe, W., Lang, F., Mateescu, R.: Using model checking to identify timing interferences on multicore processors. In: ERTS 2020 - 10th European Congress on Embedded Real Time Software and Systems. pp. 1–10. Toulouse, France (2020)
23.
go back to reference Reineke, J., Wachter, B., Thesing, S., Wilhelm, R., Polian, I., Eisinger, J., Becker, B.: A definition and classification of timing anomalies. In: 6th International Workshop on Worst-Case Execution Time (WCET) Analysis. Dresden, Germany (2006) Reineke, J., Wachter, B., Thesing, S., Wilhelm, R., Polian, I., Eisinger, J., Becker, B.: A definition and classification of timing anomalies. In: 6th International Workshop on Worst-Case Execution Time (WCET) Analysis. Dresden, Germany (2006)
24.
go back to reference Schoeberl, M., Abbaspour, S., Akesson, B., Audsley, N.C., Capasso, R., Garside, J., Goossens, K., Goossens, S., Hansen, S., Heckmann, R., Hepp, S., Huber, B., Jordan, A., Kasapaki, E., Knoop, J., Li, Y., Prokesch, D., Puffitsch, W., Puschner, P.P., Rocha, A., Silva, C., Sparsø, J., Tocchi, A.: T-CREST: time-predictable multi-core architecture for embedded systems. J. Syst. Arch. Emb. Syst. Design 61(9), 449–471 (2015) Schoeberl, M., Abbaspour, S., Akesson, B., Audsley, N.C., Capasso, R., Garside, J., Goossens, K., Goossens, S., Hansen, S., Heckmann, R., Hepp, S., Huber, B., Jordan, A., Kasapaki, E., Knoop, J., Li, Y., Prokesch, D., Puffitsch, W., Puschner, P.P., Rocha, A., Silva, C., Sparsø, J., Tocchi, A.: T-CREST: time-predictable multi-core architecture for embedded systems. J. Syst. Arch. Emb. Syst. Design 61(9), 449–471 (2015)
25.
go back to reference Seshia, S.A., Subramanyan, P.: Uclid5: Integrating modeling, verification, synthesis and learning. In: 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). pp. 1–10 (2018). 10.1109/MEMCOD.2018.8556946 Seshia, S.A., Subramanyan, P.: Uclid5: Integrating modeling, verification, synthesis and learning. In: 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). pp. 1–10 (2018). 10.1109/MEMCOD.2018.8556946
26.
go back to reference Sun, W.T., Jenn, E., Cassé, H.: Build your own static wcet analyser: the case of the automotive processor aurix tc275. In: 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020) (Jan 2020) Sun, W.T., Jenn, E., Cassé, H.: Build your own static wcet analyser: the case of the automotive processor aurix tc275. In: 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020) (Jan 2020)
27.
go back to reference Ungerer, T., Cazorla, F.J., Sainrat, P., Bernat, G., Petrov, Z., Rochange, C., Quiñones, E., Gerdes, M., Paolieri, M., Wolf, J., Cassé, H., Uhrig, S., Guliashvili, I., Houston, M., Kluge, F., Metzlaff, S., Mische, J.: Merasa: Multicore execution of hard real-time applications supporting analyzability. IEEE Micro 30(5), 66–75 (2010)CrossRef Ungerer, T., Cazorla, F.J., Sainrat, P., Bernat, G., Petrov, Z., Rochange, C., Quiñones, E., Gerdes, M., Paolieri, M., Wolf, J., Cassé, H., Uhrig, S., Guliashvili, I., Houston, M., Kluge, F., Metzlaff, S., Mische, J.: Merasa: Multicore execution of hard real-time applications supporting analyzability. IEEE Micro 30(5), 66–75 (2010)CrossRef
28.
go back to reference Wenzel, I., Kirner, R., Puschner, P.P., Rieder, B.: Principles of timing anomalies in superscalar processors. In: International Conference on Quality Software (QSIC 2005), Melbourne, Australia, pp. 295–306. (2005) Wenzel, I., Kirner, R., Puschner, P.P., Rieder, B.: Principles of timing anomalies in superscalar processors. In: International Conference on Quality Software (QSIC 2005), Melbourne, Australia, pp. 295–306. (2005)
29.
go back to reference Wilhelm, S., Wachter, B.: Towards symbolic state traversal for efficient WCET analysis of abstract pipeline and cache models. In: 7th International Workshop on Worst-Case Execution Time (WCET) Analysis, Pisa, Italy, July 3, (2007) Wilhelm, S., Wachter, B.: Towards symbolic state traversal for efficient WCET analysis of abstract pipeline and cache models. In: 7th International Workshop on Worst-Case Execution Time (WCET) Analysis, Pisa, Italy, July 3, (2007)
Metadata
Title
Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture
Authors
Benjamin Binder
Mihail Asavoae
Florian Brandner
Belgacem Ben Hedia
Mathieu Jan
Publication date
11-04-2022
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 3/2022
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00655-1

Other articles of this Issue 3/2022

International Journal on Software Tools for Technology Transfer 3/2022 Go to the issue

Premium Partner