Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

AutoParBench: A Unified Test Framework for OpenMP-based Parallelizers

After decades of advances in techniques of automatic parallelization, software developers can count, today, on many different tools that transform a program, so that it runs in parallel. Yet, most of these tools are still considered research artifacts. They contain latent bugs, often consequence of a sparsity of testing frameworks for autoparallelizers. This dissertation describes one such framework: AutoParBench - the product of a cooperation between UFMG's Compilers Lab, and Lawrence Livermore National Laboratory. AutoParBench is today publicly available, and has been successfully used to find three zero-day bugs in the Intel C Compiler. Its usage also uncovered problems in more research-oriented tools: 2 bugs in DawnCC, 4 in Rose AutoPar and 2 in Cetus. All these bugs have been confirmed, and some of them have been already fixed as an aftermath of this work.

On improving the efficiency of mathematical modeling of the problem of stability of construction

Algorithmic software for mathematical modeling of structural stability is considered, which is reduced to solving a partial generalized eigenvalues problem of sparse matrices, with automatic parallelization of calculations on modern parallel computers with graphics processors. Peculiarities of realization of parallel algorithms for different structures of sparse matrices are presented. The times of solving the problem of stability of composite materialsusing a three-dimensional model of "finite size fibers" on computers of different architectures are given. In mathematical modeling of physical and technical processes in many cases there is a need to solve problems of algebraic problem of eigenvalues (APVZ) with sparse matrices of large volumes. In particular, such problems arise in the analysis of the strength of structures in civil and industrial construction, aircraft construction, electric welding, etc. The solving to these problems is to determine the eigenvalues and eigenvectors of sparse matrices of different structure. The efficiency of solving these problems largely depends on the effectiveness of mathematical modeling of the problem as a whole. Continuous growth of task parameters, calculation of more complete models of objects and processes on computers require an increase in computer productivity. High-performance computing requirements are far ahead of traditional parallel computing, even with multicore processors. High-performance computing requirements are far ahead of traditional parallel computing, even with multicore processors. Today, this problem is solved by using powerful supercomputers of hybrid architecture, such as computers with multicore processors (CPUs) and graphics processors (GPUs), which combine MIMD and SIMD architectures. But the potential of high-performance computers can be used to the fullest only with algorithmic software that takes into account both the properties of the task and the features of the hybrid architecture. Complicating the architecture of modern high-performance supercomputers of hybrid architecture, which are actively used for mathematical modeling (increasing the number of computer processors and cores, different types of computer memory, different programming technologies, etc.) means a significant complication of efficient use of these resources in creating parallel algorithms and programs. here are problems with the creation of algorithmic software with automatic execution of stages of work, which are associated with the efficient use of computing resources, ways to store and process sparse matrices, analysis of the reliability of computer results. This makes it possible to significantly increase the efficiency of mathematical modeling of practical problems on modern high-performance computers, as well as free users from the problems of parallelization of complex problems. he developed algorithmic software automatically implements all stages of parallel computing and processing of sparse matrices on a hybrid computer. It was used at the Institute of Mechanics named after S.P. Tymoshenko NAS of Ukraine in modeling the strength problems of composite material. A significant improvement in the time characteristics of mathematical modeling was obtained. Problems of mathematical modeling of the properties of composite materials has an important role in designing the processes of deformation and destruction of products in various subject areas. Algorithmic software for mathematical modeling of structural stability is considered, which is reduced to solving a partial generalized problem of eigen values of sparse matrices of different structure of large orders, with automatic parallelization of calculations on modern parallel computers with graphics processors. The main methodological principles and features of implementation of parallel algorithms for different structures of sparse matrices are presented, which ensure effective implementation of multilevel parallelism of a hybrid system and reduce data exchange time during the computational process. As an example of these approaches, a hybrid algorithm of the iteration method in subspace for tape and block-diagonal matrices with a frame for computers of hybrid architecture is given. Peculiarities of data decomposition for matrices of profile structure at realization of parallel algorithms are considered. The proposed approach provides automatic determination of the required topology of the hybrid computer and the optimal amount of resources for the organization of an efficient computational process. The results of testing the developed algorithmic software for problems from the collection of the University of Florida, as well as the times of solving the problem of stability of composite materials using a three-dimensional model of "finite size fibers" on computers of different architectures. The results show a significant improvement in the time characteristics of solving problems.