Autotuning Parallel Programs by Model Checking

The paper presents a new approach to autotuning data-parallel programs. Autotuning is a search for optimal program settings which maximize its performance. The novelty of the approach lies in the use of the model checking method to find the optimal tuning parameters by the method of counterexamples. In our work, we abstract from specific programs and specific processors by defining their representative abstract patterns. Our method of counterexamples implements the following four steps. At the first step, an execution model of an abstract program on an abstract processor is described in the language of a model checking tool. At the second step, in the language of the model checking tool, we formulate the optimality property that depends on the constructed model. At the third step, we find the optimal values of the tuning parameters by using a counterexample constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counter-example for the optimal parameters. We apply this approach to autotuning parallel programs written in OpenCL, a popular modern language that extends the C language for programming both standard multi-core processors (CPUs) and massively parallel graphics processing units (GPUs). As a verification tool, we use the SPIN verifier and its model representation language Promela, whose formal semantics is good for modelling the execution of parallel programs on processors with different architectures.

Notes on Recent Achievements in Proving Stability using KeYmaeraX

KeYmaeraX is a Hoare-style theorem prover for hybrid systems. A hybrid system can be seen as an aggregation of both discrete and continuous variables, whose values can change abruptly or continuously, respectively. KeYmaeraX supports only variables having the primitive type bool or real. Due to the mixture of discrete and continuous system elements, one promising application area for KeYmaeraX are closed-loop control systems. A closed-loop control system consists of a plant and a controller. While the plant is basically an aggregation of continuous variables whose values change over time accordingly to physical laws, the controller can be seen as an algorithm formulated in a classical programming language. In this paper, we review some recent extensions of the proof calculus applied by KeYmaeraX that make formal proofs on the stability of dynamic systems more feasible. Based on an example, we first introduce to the topic and prove asymptotic stability of a given system in a hand-written mathematical style. This approach is then compared with a formal encoding of the problem and a formal proof established in KeYmaeraX. We also discuss open problems such as the formalization of asymptotic stability.

Solving Linear Programming Problems by Reducing to the Form with an Obvious Answer

The article considers a method for solving a linear programming problem (LPP), which requires finding the minimum or maximum of a linear functional on a set of non-negative solutions of a system of linear algebraic equations with the same unknowns. The method is obtained by improving the classical simplex method, which when involving geometric considerations, in fact, generalizes the Gauss complete exclusion method for solving systems of equations. The proposed method, as well as the method of complete exceptions, proceeds from purely algebraic considerations. It consists of converting the entire LPP, including the objective function, into an equivalent problem with an obvious answer. For the convenience of converting the target functional, the equations are written as linear functionals on the left side and zeros on the right one. From the coefficients of the mentioned functionals, a matrix is formed, which is called the LPP matrix. The zero row of the matrix is the coefficients of the target functional, $a_{00}$ is its free member. The algorithms are described and justified in terms of the transformation of this matrix. In calculations the matrix is a calculation table. The method under consideration by analogy with the simplex method consists of three stages. At the first stage the LPP matrix is reduced to a special 1-canonical form. With such matrices one of the basic solutions of the system is obvious, and the target functional on it is $ a_{00}$, which is very convenient. At the second stage the resulting matrix is transformed into a similar matrix with non-positive elements of the zero column (except $a_{00}$), which entails the non-negativity of the basic solution. At the third stage the matrix is transformed into a matrix that provides non-negativity and optimality of the basic solution. For the second stage the analog of which in the simplex method uses an artificial basis and is the most time-consuming, two variants without artificial variables are given. When describing the first of them, along the way, a very easy-to-understand and remember analogue of the famous Farkas lemma is obtained. The other option is quite simple to use, but its full justification is difficult and will be separately published.

On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

A Recursive Inclusion Checker for Recursively Defined Subtypes

We present a tableaux procedure that checks logical relations between recursively defined subtypes of recursively defined types and apply this procedure to the problem of resolving ambiguous names in a programming language. This work is part of a project to design a new programming language suitable for efficient implementation of logic. Logical formulas are tree-like structures with many constructors having different arities and argument types. Algorithms that use these structures must perform case analysis on the constructors, and access subtrees whose type and existence depend on the constructor used. In many programming languages, case analysis is handled by matching, but we want to take a different approach, based on recursively defined subtypes. Instead of matching a tree against different constructors, we will classify it by using a set of disjoint subtypes. Subtypes are more general than structural forms based on constructors, we expect that they can be implemented more efficiently, and in addition can be used in static type checking. This makes it possible to use recursively defined subtypes as preconditions or postconditions of functions. We define the types and the subtypes (which we will call adjectives), define their semantics, and give a tableaux-based inclusion checker for adjectives. We show how to use this inclusion checker for resolving ambiguous field references in declarations of adjectives. The same procedure can be used for resolving ambiguous function calls.

A Mathematical Model of Parallel Programs and an Approach Based on it to Verification of MPI Programs

The paper presents a new mathematical model of parallel programs, on the basis of which it is possible, in particular, to verify parallel programs presented on a certain subset of the parallel programming interface MPI. This model is based on the concepts of a sequential and distributed process. A parallel program is modeled as a distributed process in which sequential processes communicate by asynchronously sending and receiving messages over channels. The main advantage of the described model is the ability to simulate and verify parallel programs that generate an indefinite number of sequential processes. The proposed model is illustrated by the application of verification of the matrix multiplication MPI program.

An Algorithm for Estimating the Signal Frequency at the Output of a Channel with a Controlled Information Flow under Phase Noise Conditions

Research in the field of efficient frequency estimation algorithms is of great interest. The reason for this is the redistribution of the role of additive and phase noise in many modern radio-engineering applications. An example is the area of measuring radio devices, which usually operate at high signal-to-noise ratios (SNR). The estimation error is largely determined not by the broadband noise, but by the frequency and phase noise of the local oscillators of the receiving and transmitting devices. In particular, earlier works \\cite{Nikiforov} proposed an efficient computational algorithm for estimating the frequency of a quasi-harmonic signal based on the iterative calculation of the autocorrelation sequence (ACS). In \\cite{Volkov}, this algorithm was improved and its proximity to the Rao-Cramer boundary was shown (the sources of this noise are master oscillators and frequency synthesizers). Possibilities of frequency estimation in radio channels make it possible to significantly expand the functionality of the entire radio network. This can include, for example, the problem of adaptive distribution of information flows of a radio network. This also includes the tasks of synchronization and coherent signal processing. For these reasons, more research is needed on this algorithm, the calculation of theoretical boundaries and their comparison with the simulation results.

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.

A Simple Algorithm for Finding a Non-negative Basic Solution of a System of Linear Algebraic Equations

This article describes an algorithm for obtaining a non-negative basic solution of a system of linear algebraic equations. This problem, which undoubtedly has an independent interest, in particular, is the most time-consuming part of the famous simplex method for solving linear programming problems.Unlike the artificial basis Orden’s method used in the classical simplex method, the proposed algorithm does not attract artificial variables and economically consumes computational resources.The algorithm consists of two stages, each of which is based on Gaussian exceptions. The first stage coincides with the main part of the Gaussian complete exclusion method, in which the matrix of the system is reduced to the form with an identity submatrix. The second stage is an iterative cycle, at each of the iterations of which, according to some rules, a resolving element is selected, and then a Gaussian elimination step is performed, preserving the matrix structure obtained at the first stage. The cycle ends either when the absence of non-negative solutions is established, or when one of them is found.Two rules for choosing a resolving element are given. The more primitive of them allows for ambiguity of choice and does not exclude looping (but in very rare cases). Use of the second rule ensures that there is no looping.

Corrigendum to: Y. V. Kosolapov, “On the Detection of Exploitation of Vulnerabilities Leading to the Execution of a Malicious Code”, Modeling and analysis of information systems, vol. 27, no. 2, pp. 138–151, 2020. DOI: https://doi.org/10.18255/1818-1015-2020-2-138-151

In the article by Y. V. Kosolapov “On the Detection of Exploitation of Vulnerabilities Leading to the Execution of a Malicious Code” (Modeling and analysis of information systems, vol. 27, no. 2, pp. 138–151, 2020; https://doi.org/10.18255/1818-1015-2020-2-138-151) an inaccurate description of the algorithm CheckTrace is committed. The correct description of the algorithm CheckTrace is given below. The author apologises for the inconvenience.