Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, Lecture Notes in Computer Science
11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers The Ershov Informatics Conference Perspectives of System Informatics (in the PSI Conference Series) is the premier international forum in Russia for research and applications in computer, software, and information sciences. The conference brings together academic and industrial researchers, developers, and users to discuss the most recent topics in the field. PSI provides an ideal venue for setting up research collaborations between the rapidly growing Russian informatics community and its international counterparts, as well as between established scientists and younger researchers. The 11th edition of the conference was held during June 27–29, 2017, in Moscow (Russian Federation). Over 150 researchers and students participated in the event. This volume contains the papers presented at PSI 2017. There were 57 submissions. Each submission was reviewed by at least two, and on average three, Program Committee members. The committee decided to accept 31 papers. Dines Bjørner DTU (Denmark) spoke at the opening of the conference about the contribution of academician Victor Ivannikov to computer science, one of the organizers of this conference, who died at the end of 2016. Famous scientists in the field of computer science presented invited talks: – Sriram Rajamani (Microsoft Research, India) — “Trusted Cloud: How to Make the Cloud More Secure” – Andrei Sabelfeld (Chalmers University of Technology in Gothenburg, Sweden and Gothenburg University, Sweden) — “Taint Tracking Without Tracking Taints” – Michael Gerard Hinchey (Irish Software Engineering Research Centre, Lero) — “Building Resilient Space Exploration Systems” We wish to thank all those involved in the support and organization of this conference as well as the Program Committee members and the anonymous reviewers. Without them and all their hard work, the realization of such an ambitious project would not have been possible.
The paper presents MicroTESK, a tool for test program generation for functional verification of microprocessors. It generates test programs from templates which describe generation tasks in terms of constraints that must be satisfied in order to reach certain coverage goals. The tool uses formal specifications of the instruction set as a source of knowledge about the microprocessor under verification. This gives several advantages. First, the tool is easily adapted to new architectures by providing corresponding specifications. Second, constraints that constitute coverage model are automatically extracted from specifications. Third, a reference model used to track the microprocessor state during test generation is constructed on the basis of specifications. Such an approach helps to reduce the effort required to create test programs and increase the quality of testing. The tool has been successfully applied in industrial projects for verification of ARMv8 and MIPS64 microprocessors.
Several previous evaluations of memory models for SMT-based deductive verification tools have shown that the choice of memory model may significantly affect both the number of automatically discharged verification conditions and the capabilities of the verification tool. One of the most efficient memory models for deductive verification of low-level C code is based on region analysis and component-as-array modeling. However, originally this model doesn’t support many C language idioms widely used in low-level system code including the Linux kernel. The paper suggests a modification of this model that extends it with full support for arbitrarily nested structures, unions and arrays, arbitrary pointer arithmetic and general pointer type casts. The extension for nested structures and arrays requires no additional annotation overhead. The support for pointer arithmetic, unions and pointer type casts generally requires user annotations. The proposed model fully preserves the performance of the original memory model for earlier supported code. Preliminary practical evaluation on an industrial security kernel module showed a small specification overhead required for code where the proposed model is not fully automatic.
A component model enabling to construct new software components from existing ones dynamically, at runtime, without their bytecodes generation is presented with supporting it software framework. The framework is implemented using JavaBeans component model, but is aimed to eliminate its drawback – the inability to create user-defined components without bytecodes generation. To construct user-defined component dynamically, a composed prototype object is built using predefined (hardcoded and/or composed) component instances; that prototype object can provide functionality required and can be transformed at runtime into a new component (instantiable type) whose instances are able to provide the same functionality, but more efficiently. The prototype object is composed using meta-components – the framework provided components to produce user-defined components dynamically.
A raster is the primary data type in Earth science, geology, remote sensing and other fields with tremendous growth of data volumes. An array DBMS is an option to tackle big raster data processing. However, raster data are traditionally stored in files, not in databases. Command line tools have long being developed to process raster files. Most tools are feature-rich and free but optimized for a single machine. This paper proposes new techniques for distributed processing of raster data directly in diverse file formats by delegating considerable portions of work to such tools. An N-dimensional array data model is proposed to maintain independence from the files and the tools. Also, a new scheme named GROUP–APPLY–FINALLY is presented to universally express the majority of raster data processing operations and streamline their distributed execution. New approaches make it possible to provide a rich collection of raster operations at scale and outperform SciDB over
In this paper we present a novel disk-based distributed column-store, describe its architecture and discuss a number of technical solutions. Our system is essentially a query engine which was written completely from scratch. It is aimed for shared-nothing environments and supports different forms of parallel query processing.
Query processing in PosDB is organized according to the classic Volcano pull-based model which is adapted for the column-store case. Currently, we support late materialization only, and therefore employ a join index data structure to represent positional information. In our system query plan can consist of both positional and value operators. PosDB has about a dozen of core operators among which several variants of selections and joins, aggregation. We also have several operators that ensure intra-query parallelism and operators for network interoperability. In its current state the system is fully capable of processing the Star Schema Benchmark in a local and distributed environment.