With the growing volume and demand for data a major concern for an Organization is to discover what data there actually is, what it contains and how it is being used and by who. The amount of data and the disparate systems used to handle this data increase in their number and complexity every year and unifying these systems becomes more and more complex. In this work we describe an Intelligent search engine system, specifically designed to tackle the problem of information retrieval and sharing in a large multifaceted organization, that already has many systems in place for each Department, which is an integral part of a joint Operational Data Platform(ODP) for data exploration and processing.

With the growing volume and demand for data, a major concern for an Organization is the creation of collaborative Data-Driven projects. With the amount of data, number of departments and the development of potential use cases, the complexity of creating Multitenant and Collaborative environments for multidisciplinary teams to work and create productive solutions, is becoming more and more important problem. In this work, we describe an approach to building such an environment with scalability, flexibility and productivity in mind. This solution is an integral part of a joint Operational Data Platform for data exploration and processing at large data driven Organizations.

Automated test generation is a promising direction in hardware verification research area. Functional test generation methods based on models are widespread at the moment. In this paper, a functional test generation method based on model checking is proposed and compared to existing solutions. Automated model extraction from the hardware design’s source code is used. Supported HDLs include VHDL and Verilog. Several kinds of models are used at different steps of the test generation method: guarded action decision diagram (GADD), high-level decision diagram (HLDD) and extended finite-state machine (EFSM). The high-level decision diagram model (which is extracted from the GADD model) is used as a functional model. The extended finite-state machine model is used as a coverage model. The aim of test generation is to cover all the transitions of the extended finite state machine model. Such criterion leads to the high HDL source code coverage. Specifications based on transition and state constraints of the EFSM are extracted for this purpose. Later, the functional model and the specifications are automatically translated into the input format of the nuXmv model checking tool. nuXmv performs model checking and generates counterexamples. These counterexamples are translated to functional tests that can be simulated by the HDL simulator. The proposed method has been implemented as a part of the HDL Retrascope framework. Experiments show that the method can generate shorter tests than the FATE and RETGA methods providing the same or better source code coverage.

This paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The method is comprised of three main steps. First, a Promela model written for a certain configuration of the system is generalized to the model being parameterized with the number of processors. To do it, some assumptions on the protocol are used as well as simple induction rules. Second, the parameterized model is abstracted from the number of processors. It is done by syntactical transformations of the model assignments, expressions, and communication actions. Finally, the abstract model is verified with the Spin model checker in a usual way. The method description is accompanied by the proof of its correctness. It is stated that the suggested abstraction is conservative in a sense that every invariant (a property that is true in all reachable states) of the abstract model is an invariant of the original model (invariant properties are the properties of interest during verification of cache coherence protocols). The method has been automated by a tool prototype that, given a Promela model, parses the code, builds the abstract syntax tree, transforms it according to the rules, and maps it back to Promela. The tool (and the method in general) has been successfully applied to verification of the MOSI protocols implemented in the Elbrus computer systems.

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.

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.

Nested Petri nets (NP-nets) have proved to be one of the convenient formalisms for distributed multi-agent systems modeling and analysis. It allows representing multi-agent systems structure in a natural way, since tokens in the system net are Petri nets themselves, and have their own behavior. Multi-agent systems are highly concurrent. Verification of such systems with model checking method causes serious difficulties arising from the huge growth of the number of system intermediate states (state-space explosion problem). To solve this problem an approach based on unfolding system behavior was proposed in the literature. Earlier in [4] the applicability of unfolding for nested Petri nets verification was studied, and the method for constructing unfolding for safe conservative nested Petri nets was proposed. In this work we propose another method for constructing safe conservative nested Petri nets unfoldings, which is based on translation of such nets into classical Petri nets and applying standard method for unfolding construction to them. We discuss also the comparative merits of the two approaches. Key words: multi-agent systems; verification; Petri nets; nested Petri nets; unfoldings.

The method for exploitability estimation of program bugs is presented. Using this technique allows to prioritize software bugs that were found. Thus, it gives an opportunity for a developer to fix bugs, which are most security critical at first. The method is based on combining preliminary classification of program bugs and automatic exploit generation. Preliminary classification is used to filter non-exploitable software defects. For potentially exploitable bugs corresponding exploit generation algorithm is chosen. In case of a successful exploit generation the operability of exploit is checked in program emulator. There are various ways that used for finding software bugs. Fuzzing and dynamic symbolic execution are often used for this purpose. The main requirement for the use of the proposed method is an opportunity to get input data, which cause program to crash. The technique could be applied to program binaries and does not require debug information. Implementation of the method is a set of software tools, which are interconnected with control scripts. The preliminary classification method and automatic exploit generation method are implemented as stand-alone tools, and could be used separately. The technique was used to analyze 274 program crashes, which were obtained by fuzzing. The analysis managed to detect 13 exploitable bugs, for which successfully workable exploits were generated.

The paper describes a static analysis approach for buffer overflow detection in C/C++ source code. This algorithm is designed to be path-sensitive as it is based on symbolic execution with state merging. For now, it works only with buffers on stack or on static memory with compile-time known size. We propose a formal definition for buffer overflow errors that are caused by executing a particular sequence of program control-flow edges. To detect such errors, we present an algorithm for computing a summary for each program value at any program point along multiple paths. This summary includes all joined values at join points with path conditions. It also tracks value relations such as arithmetic operations, cast instructions, binary relations from constraints. For any buffer access we compute a sufficient condition for overflow using this summary for index variable and the reachability condition for the current function point. If this condition is proved to be satisfiable by an SMT-solver, we use its model given by the solver to detect error path and report the warning with this path. This approach was implemented for Svace static analyzer as the new buffer overflow detector, and it has found a significant amount of unique true warnings that are not covered by the old buffer overflow detector implementations.

The paper describes the approach used in implementing OpenMP offloading to NVIDIA accelerators in GCC. Offloading refers to a new capability in OpenMP 4.0 specification update that allows the programmer to specify regions of code that should be executed on an accelerator device that potentially has its own memory space and has an architecture tuned towards highly parallel execution. NVIDIA provides a specification of the abstract PTX architecture for the purpose of low-level, and yet portable, programming of their GPU accelerators. PTX code usually does not use explicit vector (SIMD) computation; instead, vector parallelism is expressed via SIMT (single instruction - multiple threads) execution, where groups of 32 threads are executed in lockstep fashion, with support on hardware level for divergent branching. However, some control flow constructs such as spinlock acquisition can lead to deadlocks, since reconvergence points after branches are inserted implicitly. Thus, our implementation maps logical OpenMP threads to PTX warps (synchronous groups of 32 threads). Individual PTX execution contexts are therefore mapped to logical OpenMP SIMD lanes (this is similar to the mapping used in OpenACC). To implement execution of one logical OpenMP thread by a group of PTX threads we developed a new code generation model that allows to keep all PTX threads active, have their local state (register contents) mirrored, and have side effects from atomic instructions and system calls such as malloc happen only once per warp. This is achieved by executing the original atomic or call instruction under a predicate, and then propagating the register holding the result using the shuffle exchange (shfl) instruction. Furthermore, it is possible to setup the predicate and the source lane index in the shuffle instruction in a way that this sequence has the same effect as just the original instruction inside of SIMD regions. We also describe our implementation of compiler-defined per-warp stacks, which is required to have per-warp automatic storage outside of SIMD regions that allows cross-warp references (normally automatic storage in PTX is implemented via .local memory space which is visible only in the PTX thread that owns it). This is motivated by our use of unmodified OpenMP lowering in GCC where possible, and thus using libgomp routines for entering parallel regions, distribution of loop iterations, etc. We tested our implementation on a set of micro-benchmarks, and observed that there is a fixed overhead of about 100 microseconds when entering a target region, mostly due to startup procedures in libgomp (and notably due to calls to malloc), but for long-running regions where that overhead is small we achieve performance similar to analogous OpenACC and CUDA code.

As a further development of case-based approach to complex object control with objects that cannot be formalized by mathematical model, authors offer new object behavior model. This model deals with objects that are involved in low-intensity processes, and then suddenly (as it seems) and spontaneously are changing their states in avalanche-like manner. To describe such changes a new conception of satellite class is introduced. The influence of satellite classes may be treated as an additional control action that effects on the class to which the object belonged. This model is firstly oriented on medicine applications where one can find many examples of the similar behavior.

Graph databases appear to be the most popular and relevant among non-relational databases. Its popularity is caused by its relatively easy implementation in the problems in which data have big numbers of relations such as protein-protein interaction and others. With the development of fast internet connection, graph database found another interesting application in representation of social networks. Moreover, graph edges are storable which lowers graph traversing calculation costs. Such system appeared to be natural and in-demand in the era of Internet and social networks. The most significant by size and matter section of graph databases problems is data mining. It contains such problems as associative rules learning, data classification and categorization, clustering, regression analysis etc. In this review, data mining graph database problems are considered which are most commonly presented in modern literature. Their popularity is represented by the big number of publications on these problems on several recent years’ major conferences. Such problems as influence maximization, motif mining, pattern matching and simrank problems are examined. For every type of a problem we analyzed different papers and described basic algorithms which were offered 10-15 years ago. We also considered state-of-the-art solutions as well as some important in-between versions. This review consists of 6 sections. Besides introduction and conclusion, each section is dedicated to its own type of graph database problem.

In recent years, as performance and capacity of main and external memory grow, performance of database management systems (DBMSes) on certain kinds of queries is more determined by raw CPU speed. Currently, PostgreSQL uses the interpreter to execute SQL queries. This yields an overhead caused by indirect calls to handler functions and runtime checks, which could be avoided if the query were compiled into native code "on-the-fly", i.e. just-in-time (JIT) compiled: at run time the specific table structure is known as well as data types and built-in functions used in the query as well as the query itself. This is especially important for complex queries, performance of which is CPU-bound. We’ve developed a PostgreSQL extension that implements SQL query JIT compilation using LLVM compiler infrastructure. In this paper we show how to implement JIT compilation to speed up sequential scan operator (SeqScan) as well as expressions in WHERE clauses. We describe some important optimizations that are possible only with dynamic compilation, such as precomputing tuple attributes offsets only for attributes used by the query. We also discuss the maintainability of our extension, i.e. the automation for translating PostgreSQL backend functions into LLVM IR, using the same source code both for our JIT compiler and the existing interpreter. Currently, with LLVM JIT we achieve up to 5x speedup on synthetic tests as compared to original PostgreSQL interpreter.

Currently there is growing interest in motion planning problems that play a key role in automation of technologically difficult processes in mechanical, power and transport engineering, medicine, construction and creation of new products and services. This interest particularly relates to the increasing role of computer simulation and such disciplines as complex planning of industrial projects, realistic 3D animation, robotic surgery, automotive products assembly and organization of movement of transport streams. This paper is devoted to the overview and analysis of modern motion planning methods.