• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
Of all publications in the section: 123
Sort:
by name
by year
Article
Gordenko M., Avdoshin S. M. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 221-232.

In this article, the routing problems are described. It is shown, that almost all routing problem can be transformed into each other. An example of the Mixed Chinese Postman problem is discussed. The article gives an overview of various variants of Chinese Postman Problem. For all problems the mathematical formulation is given. Moreover, the useful real-life application is presented, too. Then, the article provides a table of possible Chinese Postman problems and identifies parameters that can be varied for obtaining new problems. Five parameters have been identified, such as: presence of set of edges; presence of set of arcs; presence of edges with cost, depending on traversing; the presence of set of required edges; the presence of set of required arcs. It was shown that by varying these parameters one can obtain tasks that were not described earlier but can be used in real life. Four new tasks were identified. Then it is shown that the Chinese Postman problem can be solved as another routing tasks through graph transformations. The method for transforming Chinese Postman problem into the Generalized Travelling Salesman problem is given. Then the results of solving the above problem are presented by simple algorithms, and their effectiveness is shown. The research is not over yet. The testing of other algorithms is planned.

Added: Sep 2, 2018
Article
Dworzanski L. W., Михайлов В. Е. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 4. P. 175-190.

Well-structured transition systems (WSTS) became a well-known tool in the study of concurrency systems for proving decidability of properties based on coverability and boundedness. Each year brings new formalisms proven to be WSTS systems. Despite the large body of theoretical work on the WSTS theory, there has been a notable gap of empirical research of well-structured transition systems. In this paper, the tool for behavioural analysis of such systems is presented. We suggest the extension of SETL language to describe WSTS systems (WSTSL). It makes the description of new formalisms very close to the formal definition. Therefore, it is easy to introduce and modify new formalisms as well as conduct analysis of the behavioural properties without much programming efforts. It is highly convenient when a new formalism is still under active development. Two most studied algorithms for analysis of well-structured transition systems behavior (backward reachability and the Finite Reachability Tree analyses) have been implemented; and, their performance was measured through the runs on such models as Petri Nets and Lossy Channel Systems. The developed tool can be useful for incorporating and testing analysis methods to formalisms that occur to be well-structuredness transition systems.

Added: Oct 1, 2017
Article
Гималетдинова А. Р., Degtiarev K.Y. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 4. P. 87-106.

In the last few years there has been a growing interest in route building oriented mobile applications with the following features of navigation and sending timely notifications about arrival. Despite the large body of existing knowledge on navigational services, there has been an important issue relative to positioning accuracy. The paper discusses a possible solution to comparison problem, which is linked to the determination of the closeness to destination metro station through finding a difference between user’s current coordinates and fixed-point coordinates. With this end in view, fuzzy logic approach is used to develop Routes Recommender System (RRS) that utilizes linguistic variables to express the vague and uncertain term ‘closeness to…’. The paper provides detailed explanation of each variable considered in the fuzzy inference system (FIS), set of fuzzy rules in line with graphical representation of system’s output. Based on Mamdani model, we propose a set of test cases to check maintainability of the model and provide a description about received results. At a later time, an Android-based mobile application aimed at public transport route building will be developed whose notification system will be based on our model`s implementation presented. It should be emphasized that the paper examines potentials of the modeling approach based on interval type-2 fuzzy sets (IT2FS) that attract much attention these days in various research studies and conventional Mamdani fuzzy inference system (MFIS) as applied to real and rather topical problem. The significance of developing such models may be of a high demand for appropriate representation of factors that are inherently vague and uncertain. Hence, this study may also contribute to future research on similar topics.

Added: Sep 12, 2017
Article
R.A. Nesterov, I.A. Lomazova. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 4. P. 21-38.

Process mining offers various tools for studying process-aware information systems. They mainly involve several participants (or agents) managing and executing operations on the basis of process models. To reveal the actual behavior of agents, we can use process discovery. However, for large-scale processes, it does not yield models, which help understand how agents interact since they are independent and their concurrent implementation can lead to a very sophisticated behavior. To overcome this problem, we propose interface patterns, which allow getting models of multi-agent processes with a clearly identified agent behavior and interaction scheme as well. The correctness of patterns is provided via morphisms. We also conduct a preliminary experiment, results of which are highly competitive compared to the process discovery without interface patterns.

Added: Sep 6, 2017
Article
Mallachiev K. A., Pakulin N. V., Khoroshilov A. V. et al. Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 4. P. 283-294.

Modern embedded OS are designed to be used in control solutions in various hardware contexts. Control computers may differ in the architecture of the CPU, the structure of communication channels, supported communication protocols, etc. Embedded OS are often statically configured to create an OS image, which intended to be executed on some specific control computer. System integrator usually performs this configuration. Embedded OS are often developed by many companies. Joint development and integration is very complex if OS doesn’t support modularity. Support of modularity and component assembly reduces the need of communication among companies during development and integration. This allows customers to create minimal solutions that are optimally adapted to the particular task and hardware platform. Furthermore, customers may be interested in adding their own low level components without OS modification. In this article, we present an approach to building modular embedded solutions from heterogeneous components based on the RTOS JetOS. The mechanism of components binding developed by us allows uniting heterogeneous components from different manufacturers within the same section of the address space. This mechanism allows component developer to independently develop their components. And system integrator can independently from developers configure what component he likes to see in OS image and how components should interact.

Added: Aug 11, 2018
Article
Kuliamin V., Lavrischeva E. M., Mutilin V. S. et al. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 3. P. 189-208.

This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach.

Added: Aug 11, 2018
Article
Силаков Д. В. Труды Института системного программирования РАН. 2008. Т. 14. № 2. С. 159-178.
Added: Sep 22, 2015
Article
Силаков Д. В., Зеленов С. В. Труды Института системного программирования РАН. 2006. Т. 9. С. 129-142.
Added: Sep 22, 2015
Article
Кузнецов С. Д., Турдаков Д. Ю., Борисенко О. Д. Труды Института системного программирования РАН. 2014. Т. 26. № 4. С. 33-44.

This article is dedicated to automation of cluster creation and management for Apache Spark MapReduce implementation in Openstack environments. As a result of this project open-source (Apache 2.0 license) implementation of toolchain for virtual cluster on-demand creation in Openstack environments was presented. The article contains an overview of existing solutions for clustering automation in cloud environments by the start of 2014 year. The article provides a shallow overview of issues and problems in Openstack Heat project that provides a compatibility layer for Amazon EC2 API. The final implementation provided in the article is almost strainforward port of existing toolchain for cluster creation automation for Apache Spark in Amazon EC2 environment with some improvements. Also prepared base system virtual machine image for Openstack is provided. Plans for further work are connected with Ansible project. Using Ansible for observed problem will make possible to implement versatile environment-agnostic solution that is able to work using any cloud computing services provider, set of Docker containers or bare-metal clusters without any dependencies for prepared operating system image. Current article doesn't use Ansible due to the lack of key features at the moment of the project start. The solution provided in this article has been already tested in production environment for graph theory research arcticle.

Added: Nov 26, 2017
Article
Вялый М. Н. Труды Института системного программирования РАН. 2004. Т. 6. С. 51-64.
Added: Oct 17, 2014
Article
С.Д. Кузнецов, Прохоров А. А. Труды Института системного программирования РАН. 2012. Т. 23. С. 173-194.

One of the most important ways of increasing the speed of the modern databases is to cache frequently used data in RAM. Classical replacement policies are intended to minimize the number of buffer pool faults. This optimization method implicitly relies on the fact that the speeds of reading and writing to the hard disc are equal. Gradual technology improvement and cost reduction of flash memory have led to the creation of solid-state data storages (SSD) that are now increasingly used in personal computers and storage systems. Flash drives have advantages over traditional hard drives, high read and write speeds and significantly small time of random data access are the most important of them. However, the most popular flash-memory types read data at a higher speed than write it. Due to this feature the use of classical replacement algorithms of disk data caching is ineffective. This paper reviews recently developed algorithms of database buffer pool management designed to work with flash memory drives: CFDC (Clean First – Dirty Clustered), CASA (Cost-Aware Self- Adaptive), SAWC (Self Adaptive with Write Clustering), and FD-Buffer. Some of these algorithms demonstrate significant advantages over the classical algorithm LRU.

Added: Nov 1, 2017
Article
Лаврищева Е. М., Пакулин Н. В., Рыжов А. Г. и др. Труды Института системного программирования РАН. 2018. Т. 30. № 3. С. 99-120.
Added: Aug 11, 2018
Article
Сергей Кузнецов, Денис Турдаков, Коршунов А. В. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 439-456.
Added: Nov 25, 2017
Article
С.С.Гайсарян, Самоваров О. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 403-420.
Added: Sep 13, 2016
Article
Клеменков П. А., Кузнецов С. Д. Труды Института системного программирования РАН. 2012. Т. 23. С. 143-158.

Big data challenged traditional storage and analysis systems in several new ways. In this paper we try to figure out how to overcome this challenges, why it's not possible to make it efficiently and describe three modern approaches to big data handling: NoSQL, MapReduce and real-time stream processing. The first section of the paper is the introduction. The second section discuss main issues of Big Data: volume, diversity, velocity, and value. The third section describes different approaches to solving the problem of Big Data. Traditionally one might use a relational DBMS. The paper propose some steps that allow to continue RDBMS using when it’s capacity becomes not enough. Another way is to use a NoSQL approach. The basic ideas of the NoSQL approach are: simplification, high throughput, and unlimited scaling out. Different kinds of NoSQL stores allow to use such systems in different applications of Big Data. MapReduce and it’s free implementation Hadoop may be used to provide scaling out Big Data analytics. Finally, several data management products support real time stream processing under Big Data. The paper briefly overviews these products. The final section of the paper is the conclusion.

Added: Oct 31, 2017
Article
Кулямин В. В., Лаврищева Е., Мутилин В. и др. Труды Института системного программирования РАН. 2016. Т. 28. № 3. С. 189-208.
Added: Aug 28, 2017
Article
Кошкарев А., Медведев А., Вишняков Ю. и др. Труды Института системного программирования РАН. 2012. Т. 23. С. 245-256.
Added: Jan 26, 2016
Article
Татарников А. Д., Камкин А. С., Проценко А. С. и др. Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 87-102.

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.

Added: Nov 24, 2017
Article
Камкин А. С., Чупилко М., Лебедев М. и др. Труды Института системного программирования РАН. 2017. Т. 29. № 4. С. 247-256.

Hardware testing is a process aimed at detecting manufacturing faults in integrated circuits. To measure test quality, two main metrics are in use: fault detection abilities (fault coverage) and test application time (test length). Many algorithms have been suggested for test generation; however, no scalable solution exists. In this paper, we analyze applicability of functional tests generated from high-level models for low-level manufacturing testing. A particular test generation method is considered. The input information is an HDL description. The key steps of the method are system model construction and coverage model construction. Both models are automatically extracted from the given description. The system model is a representation of the design in the form of high-level decision diagrams. The coverage model is a set of LTL formulae defining reachability conditions for the transitions of the extended finite state machine. The models are translated into the input format of a model checker. For each coverage model formula the model checker generates a counterexample, i.e. an execution that violates the formula (makes the corresponding transition to fire). The approach is intended for covering of all possible execution paths of the input HDL description and detecting dead code. Experimental comparison with the existing analogues has shown that it produces shorter tests, but they achieve lower stuck-at fault coverage comparing with the dedicated approach. An improvement has been proposed to overcome the issue. 

Added: Nov 6, 2017
Article
Захаров В. А., Новикова Т. А. Труды Института системного программирования РАН. 2014. Т. 26. № 2. С. 245-268.
It is generally accepted that to unify a pair of substitutions θ_1 and θ_2 means to find out a pair of substitutions η' and η'' such that the compositions θ_1 η' and θ_2 η'' are the same. Actually, unification is the problem of solving linear equations of the form θ_1 X=θ_2 Y in the semigroup of substitutions. But some other linear equations on substitutions may be also viewed as less common variants of unification problem. In this paper we introduce a two-sided unification as the process of bringing a given substitution θ_1 to another given substitution θ_2 from both sides by giving a solution to an equation Xθ_1 Y=θ_2. Two-sided unification finds some applications in software refactoring as a means for extracting instances of library subroutines in arbitrary pieces of program code. In this paper we study the complexity of two-sided unification for substitutions and programs. In Section 1 we discuss the concept of unification on substitutions and programs, outline the recent results on program equivalence checking that involve the concept of unification and anti-unification, and show that the problem of library subroutine extraction may be viewed as the problem of two-sided unification for programs. In Section 2 we formally define the concept of two-sided unification on substitutions and show that the problem of two-unifiability is NP-complete (in contrast to P-completeness of one-sided unifiability problem). NP-hardness of two-sided unifiability problem is established in Section 4 by reducing to it the bounded tiling problem which is known to be NP-complete; the latter problem is formally defined in Section 3. In Section 5 we define two-sided unification of sequential programs in the first-order model of programs supplied with strong equivalence (logic&term equivalence) of programs and proved that this problem is NP-complete. This is the main result of the paper.
Added: Sep 30, 2015
Article
Монаков А., Платонов В., Аветисян А. И. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 357-374.

The article proposes methods for supporting development of efficient programs for modern parallel architectures, including hybrid systems. First, specialized profiling methods designed for programmers tasked with parallelizing existing code are proposed. The first method is loop-based profiling via source-level instrumentation done with Coccinelle tool. The second method is memory reuse distance estimation via virtual memory protection mechanism and manual instrumentation. The third method is cache miss and false sharing estimation by collecting a partial trace of memory accesses using compiler instrumentation and estimating cache behavior in postprocessing based on the trace and a cache model. Second, the problem of automatic parallel code generation for hybrid architectures is discussed. Our approach is to generate OpenCL code from parallel loop nests based on GRAPHITE infrastructure in the GCC compiler. Finally, in cases where achieving high efficiency on hybrid systems requires significant rework of data structures or algorithms, one can employ auto-tuning to specialize for specific input data and hardware at run time. This is demonstrated on the problem of optimizing sparse matrix-vector multiplication for GPUs and its use for accelerating linear system solving in OpenFOAM CFD package. We propose a variant of “sliced ELLPACK” sparse matrix storage format with special treatment for small horizontal or diagonal blocks, where the exact parameters of matrix structure and GPU kernel launch should be automatically tuned at runtime for the specific matrix and GPU hardware.

Added: Mar 22, 2017