Генерация тестовых программ для подсистемы управления памятью MIPS64 на основе спецификаций

В данной работе описан инструмент автоматической генерации тестовых программ для подсистем управления памятью микропроцессоров с архитектурой MIPS64. Предлагаемое средство базируется на среде MicroTESK, разрабатываемой в Институте системного программирования РАН. Инструмент состоит из двух частей: архитектурно независимого ядра генерации тестовых программ и спецификации подсистемы памяти MIPS64. Такое разделение не является новым - аналогичный подход применяется в промышленных генераторах, в том числе в Genesys-Pro, разрабатываемом в исследовательском подразделении компании IBM. Основные различия между инструментами состоят в форме представления спецификаций, типе извлекаемой из них информации и способах использования этой информации для построения тестов. В предлагаемом подходе спецификации включают в себя описания инструкций доступа к памяти (инструкций чтения и записи) и описания механизмов управления памятью, таких как буфер трансляции адресов, таблица страниц, устройство аппаратного поиска по таблице страниц, кэш-память. Для спецификации такого рода механизмов (устройств) разработан проблемно-ориентированный язык, названный mmuSL. Инструмент анализирует mmuSL-спецификации и извлекает все возможные пути исполнения инструкций (варианты обработки запросов к подсистеме памяти) и все возможные зависимости между этими путями (конфликты использования устройств). Извлеченная информация используется для систематического перебора тестовых программ для заданного пользователем тестового шаблона и позволяет исчерпывающим образом исследовать совместное исполнение группы инструкций, включая разного рода граничные случаи. Тестовые данные для тестовых программ (значения адресов, содержимое буферов и т.п.) генерируются с использованием техник символического исполнения и решения ограничений.

микропроцессор, подсистема памяти, кэширование, трансляция адресов, формальная спецификация, тестовая программа, генератор тестовых программ, MIPS64

1. MIPS64™ Architecture For Programmers. Volume 1: Introduction to the MIPS64™ Architecture. Revision 6.01. MIPS Technologies Inc. 2014. 148 p.

2. MIPS64™ Architecture For Programmers. Volume 3: MIPS64™/microMIPS64™ Privileged Resource Architecture. Revision 6.03. MIPS Technologies Inc. 2015. 368 p.

3. A. Adir, E. Almog, L. Fournier, E. Marcus, M. Rimon, M. Vinov, A. Ziv. Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. Design & Test of Computers, 2004. pp. 84-93.

4. R.L. Glass. Facts and Fallacies of Software Engineering. Addison-Wesley Professional, 2002. 224 p.

5. T. Li, D. Zhu, Y. Guo, G. Liu, S. Li. MA2TG: A Functional Test Program Generator for Microprocessor Verification. Euromicro Conference on Digital System Design, 2005. pp. 176-183.

6. A. Kamkin, A. Tatarnikov. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. Spring/Summer Young Researchers Colloquium on Software Engineering, 2012, pp. 64-69.

7. Инструмент MicroTESK. http://forge.ispras.ru/projects/microtesk

8. M. Freericks. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993.

9. A. Adir, L. Fournier, Y. Katz, A. Koyfman. DeepTrans – Extending the Model-based Approach to Functional Verification of Address Translation Mechanisms High-Level Design Validation and Test Workshop, 2006. pp. 102-110.

10. Д. Воробьев, А. Камкин. Генерация тестовых программ для подсистемы управления памятью микропроцессора. Труды ИСП РАН, 17, 2009, с. 119-132

11. A. Kamkin, A. Protsenko, A. Tatarnikov. An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms Trudy ISP RAN, 27(3), 2015. pp. 125–138.

12. Язык программирования Ruby. http://www.ruby-lang.org

13. A. Kamkin, E. Kornykhin, D. Vorobyev. Reconfigurable Model-Based Test Program Generator for Microprocessors International Conference on Software Testing, Verification and Validation Workshops, 2011. pp. 47-54.

14. A.S. Kamkin, T.I. Sergeeva, S.A. Smolov, A.D. Tatarnikov, M.M. Chupilko. Extensible Environment for Test Program Generation for Microprocessors. Programming and Computer Software, 40(1), 2014, pp. 1-9.

15. Библиотека Fortress. http://forge.ispras.ru/projects/solver-api

16. SMT-решатель Z3. http://github.com/Z3Prover/z3

17. SMT-решатель CVC4. http://cvc4.cs.nyu.edu

18. MIPS64™ Architecture For Programmers. Volume 2: The MIPS64™ Instruction Set Reference Manual. Revision 6.04. MIPS Technologies Inc. 2015. 551 p.

19. Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus, G. Shurek. Constraint-Based Random Stimuli Generation for Hardware Verification AI Magazine, 28(3), 2007. pp. 13-30.