Генератор тестовых программ для архитектуры ARMv8 на основе инструмента MicroTESK
ARM is a family of microprocessor instruction set architectures developed in a company with the same name. The newest architecture of this family, ARMv8, contains a large number of instructions of various types and is notable for its complex organization of virtual memory, which includes hardware support for multilevel address translation and virtualization. All of this makes functional verification of microprocessors with this architecture an extremely difficult technical task. An integral part of microprocessor verification is generation of test programs, i.e. programs in the assembly language, which cause various situations (exceptions, pipeline stalls, branch mispredictions, data evictions in caches, etc.). The article describes the requirements for industrial test program generators and presents a generator for microprocessors with the ARMv8 architecture, which has been developed with the help of MicroTESK (Microprocessor TEsting and Specification Kit). The generator supports an instruction subset typical for mobile applications (about 400 instructions) and consists of two main parts: (1) an architecture-independent core and (2) formal specifications of ARMv8 or, more precisely, a model automatically constructed on the basis of the formal specifications. With such a structure, the process of test program generator development consists mainly in creation of formal specifications, which saves efforts by reusing architecture-independent components. An architecture is described using the nML and mmuSL languages. The first one allows describing the microprocessor registers and syntax and semantics of the instructions. The second one is used to specify the memory subsystem organization (address spaces, various buffers and tables, address translation algorithms, etc.) The article describes characteristics of the developed generator and gives a comparison with the existing analogs.
This volume contains the Proceedings of 22nd Concurrency, Specification and Programming (GS&P) Workshop held on September 25-27, 2013 in Warsaw. There were 48 submissions. Each submission was reviewed by two program committee members. The committee decided to accept 40 papers. The Workshop was initiated in the mid 1970s by computer scientists and mathematicians from Warsaw and Humboldt Universities, as Polish-German annual meetings. They were suspended for some years in the 1980s and reactimed in 1992. Thereafter, the Workshop, organised alternatingly by the Institutes of Informatics and Mathematics of the University of Warsaw and the Institute of Informatics of Humboldt University in Berlin on the basis of an exchange program, has been given the name GS&P. It should be mentioned that the CS&P meetings, initially purely bilateral, since 1992 have developed into events attended by participants from a number of different countries beside Poland and Germany. The present GS&P'13 meeting attracted contributors from: Canada, Egypt, France, Germany, Italy, Nepal, The Netherlands, Poland, Russia, Serbia, Slenakia, Sweden, Turkey, United Kingdom, United States, and Vietnam. The organisation of this year's CS&P would not be possible without the resources and financing provided by seven institutions. We would like to thank the Faculty of Mathematics, Informatics and Mechanics of the University of Warsaw and the Institute of Informatics of the Humboldt University of Berlin for the continuing financial and organisational support provided to GS&P over last twenty-two years. The essential financial backing received from the Warsaw Center of Mathematics and Computer Science made the organisation of CS&P 2013 possible. Our thanks go to the Bialystok University of Technology for providing the means for publishing this proceedings volume. Last, but not the least, we are grateful for the significant financial support provided by the Vistula University in Warsaw.
This volume contains the papers presented at CS&P 2014: 23th International Workshop on Concurrency, Specification and Programming held on September 28 - October 1, 2014 in Chemnitz. Since the early seventies Warsaw University and Humboldt-University have alternately organized an annual workshop - since 1993 as CS&P. Over time, it has grown from a bilateral seminar to a meeting attended also by colleagues from other countries than Poland and Germany. This year there are 34 participants from 10 countries.
The specification-based approach is widely used for test program generation for functional verification of microprocessors. The size of microprocessor specifications is measured in thousands lines of code. Consequently, their maintenance requires significant effort. Typical maintenance activities include regular updates, substitution of deprecated functionality, and support for new revisions and implementation-defined features. Our team is working on MicroTESK, a tool that generates test programs for microprocessors based on specifications of the instruction set architectures. The specifications are created in a specialized language, called nML, extended with facilities to manage revision-specific and implementation-defined features. The tool has been applied to ARMv8, MIPS64, PowerPC, RISC-V, and x86 microprocessors. This paper describes our experience in maintaining specifications and the approach we use to simplify this process.
Test program generation and simulation is the most widely used approach to functional verification of microprocessors. High complexity of modern hardware designs creates a demand for automated tools that are able to generate test programs covering non-trivial situations in microprocessor functioning. The majority of such tools use test program templates that describe scenarios to be covered in an abstract way. This provides verification engineers with a flexible way to describe a wide range of test generation tasks with minimum effort. Test program templates are developed in special domain-specific languages. These languages must fulfill the following requirements: (1) be simple enough to be used by verification engineers with no sufficient programming skills; (2) be applicable to various microprocessor architectures and (3) be easy to extend with facilities for describing new types of test generation tasks. The present work discusses the test program template description language used in the reconfigurable and extensible test program generation framework MicroTESK being developed at ISP RAS. It is a flexible Ruby-based domain-specific language that allows describing a wide range of test generation tasks in terms of hardware abstractions. The tool and the language have been applied in industrial projects dedicated to verification of MIPS and ARM microprocessors.
Relevance of development of the power effective server equipment optimized for solution of standard problems of datasenter locates in article. The main characteristics of the unified multiprocessor hardware-software server complex developed by staff of National research university "Higher School of Economics" are described
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and verication, programming and specification languages, etc.
The paper proposes a method of automated construction of behavior models of microprocessors, which are used in the process of test program generation to predict the results. The proposed method is based on using formal specifications of instruction set architecture. The method is implemented in MicroTESK, a test program generation tool being developed at ISP RAS. The tool has been successfully applied in industrial projects.
The SLAM-based Static Driver Verifier Research Platform (SDVRP), as a tool that systematically analyzes source code and allows writing custom SLIC rules for various platforms, provided a potent verification mechanism for an embedded software system based on ARM Cortex-M0 microprocessor. The correctness of this software is of particular importance in the sense that there are program states which can cause physical damage to hardware.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.
A model for organizing cargo transportation between two node stations connected by a railway line which contains a certain number of intermediate stations is considered. The movement of cargo is in one direction. Such a situation may occur, for example, if one of the node stations is located in a region which produce raw material for manufacturing industry located in another region, and there is another node station. The organization of freight traﬃc is performed by means of a number of technologies. These technologies determine the rules for taking on cargo at the initial node station, the rules of interaction between neighboring stations, as well as the rule of distribution of cargo to the ﬁnal node stations. The process of cargo transportation is followed by the set rule of control. For such a model, one must determine possible modes of cargo transportation and describe their properties. This model is described by a ﬁnite-dimensional system of diﬀerential equations with nonlocal linear restrictions. The class of the solution satisfying nonlocal linear restrictions is extremely narrow. It results in the need for the “correct” extension of solutions of a system of diﬀerential equations to a class of quasi-solutions having the distinctive feature of gaps in a countable number of points. It was possible numerically using the Runge–Kutta method of the fourth order to build these quasi-solutions and determine their rate of growth. Let us note that in the technical plan the main complexity consisted in obtaining quasi-solutions satisfying the nonlocal linear restrictions. Furthermore, we investigated the dependence of quasi-solutions and, in particular, sizes of gaps (jumps) of solutions on a number of parameters of the model characterizing a rule of control, technologies for transportation of cargo and intensity of giving of cargo on a node station.
Event logs collected by modern information and technical systems usually contain enough data for automated process models discovery. A variety of algorithms was developed for process models discovery, conformance checking, log to model alignment, comparison of process models, etc., nevertheless a quick analysis of ad-hoc selected parts of a journal still have not get a full-fledged implementation. This paper describes an ROLAP-based method of multidimensional event logs storage for process mining. The result of the analysis of the journal is visualized as directed graph representing the union of all possible event sequences, ranked by their occurrence probability. Our implementation allows the analyst to discover process models for sublogs defined by ad-hoc selection of criteria and value of occurrence probability
Existing approaches suggest that IT strategy should be a reflection of business strategy. However, actually organisations do not often follow business strategy even if it is formally declared. In these conditions, IT strategy can be viewed not as a plan, but as an organisational shared view on the role of information systems. This approach generally reflects only a top-down perspective of IT strategy. So, it can be supplemented by a strategic behaviour pattern (i.e., more or less standard response to a changes that is formed as result of previous experience) to implement bottom-up approach. Two components that can help to establish effective reaction regarding new initiatives in IT are proposed here: model of IT-related decision making, and efficiency measurement metric to estimate maturity of business processes and appropriate IT. Usage of proposed tools is demonstrated in practical cases.