Proceedings of the Institute for System Programming of the RAS
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Proceedings of ISP RAS:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Proceedings of the Institute for System Programming of the RAS, 2016, Volume 28, Issue 4, Pages 99–114
DOI: https://doi.org/10.15514/ISPRAS-2016-28(4)-6
(Mi tisp55)
 

This article is cited in 1 scientific paper (total in 1 paper)

Specification-based test program generation for MIPS64 memory management units

A. S. Kamkin, A. M. Kotsynyak

Institute for System Programming of the Russian Academy of Sciences
Full-text PDF (437 kB) Citations (1)
References:
Abstract: In this paper, a tool for automatically generating test programs for MIPS64 memory management units is described. The solution is based on the MicroTESK framework being developed at the Institute for System Programming of the Russian Academy of Sciences. The tool consists of two parts: an architecture-independent test program generation core and MIPS64 memory subsystem specifications. Such separation is not a new principle in the area: it is applied in a number of industrial test program generators, including IBM's Genesys-Pro. The main distinction is in how specifications are represented, what sort of information is extracted from them, and how that information is exploited. In the suggested approach, specifications comprise descriptions of the memory access instructions, loads and stores, and definition of the memory management mechanisms such as translation lookaside buffers, page tables, table lookup units, and caches. A dedicated problem-oriented language, called mmuSL, is used for the task. The tool analyzes the mmuSL specifications and extracts all possible instruction execution paths as well as all possible inter-path dependencies. The extracted information is used to systematically enumerate test programs for a given user-defined test template and allows exhaustively exercising co-execution of the template instructions, including corner cases. Test data for a particular program are generated by using symbolic execution and constraint solving techniques.
Keywords: microprocessor, memory management unit, caching, address translation, formal specification, test program, test program generation, MIPS64.
Bibliographic databases:
Document Type: Article
Language: English
Citation: A. S. Kamkin, A. M. Kotsynyak, “Specification-based test program generation for MIPS64 memory management units”, Proceedings of ISP RAS, 28:4 (2016), 99–114
Citation in format AMSBIB
\Bibitem{KamKot16}
\by A.~S.~Kamkin, A.~M.~Kotsynyak
\paper Specification-based test program generation for MIPS64 memory management units
\jour Proceedings of ISP RAS
\yr 2016
\vol 28
\issue 4
\pages 99--114
\mathnet{http://mi.mathnet.ru/tisp55}
\crossref{https://doi.org/10.15514/ISPRAS-2016-28(4)-6}
\elib{https://elibrary.ru/item.asp?id=27174141}
Linking options:
  • https://www.mathnet.ru/eng/tisp55
  • https://www.mathnet.ru/eng/tisp/v28/i4/p99
  • This publication is cited in the following 1 articles:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Proceedings of the Institute for System Programming of the RAS
    Statistics & downloads:
    Abstract page:110
    Full-text PDF :74
    References:28
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024