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

2021 ◽  
Vol 28 (4) ◽  
pp. 394-412
Author(s):  
Andrew M. Mironov

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.

2021 ◽  
Vol 24 (1) ◽  
pp. 157-183
Author(s):  
Никита Андреевич Катаев

Automation of parallel programming is important at any stage of parallel program development. These stages include profiling of the original program, program transformation, which allows us to achieve higher performance after program parallelization, and, finally, construction and optimization of the parallel program. It is also important to choose a suitable parallel programming model to express parallelism available in a program. On the one hand, the parallel programming model should be capable to map the parallel program to a variety of existing hardware resources. On the other hand, it should simplify the development of the assistant tools and it should allow the user to explore the parallel program the assistant tools generate in a semi-automatic way. The SAPFOR (System FOR Automated Parallelization) system combines various approaches to automation of parallel programming. Moreover, it allows the user to guide the parallelization if necessary. SAPFOR produces parallel programs according to the high-level DVMH parallel programming model which simplify the development of efficient parallel programs for heterogeneous computing clusters. This paper focuses on the approach to semi-automatic parallel programming, which SAPFOR implements. We discuss the architecture of the system and present the interactive subsystem which is useful to guide the SAPFOR through program parallelization. We used the interactive subsystem to parallelize programs from the NAS Parallel Benchmarks in a semi-automatic way. Finally, we compare the performance of manually written parallel programs with programs the SAPFOR system builds.


Author(s):  
D. S. Romanova ◽  
S. Yu. Smogluk

Today, due to problems in improving computing performance, parallel programming continues to evolve. There are many different languages in which you can write parallel programs. One of them is the functional-threading parallel programming language Pifagor, which in turn is very specific and allows you to write a program with maximum parallelism, as well as it is designed to solve the portability problem of parallel programs. Tools and a library of functions continue to be developed for this language. This study is devoted to the development of elements of the mathematical library and the search for the most effective mathematical parallel algorithms. The following methods are considered and used in the work: sequential, recursive (left and right recursion), factorization, and pairwise comparisons. As a result of the study, a number of mathematical functions were developed, and a study was made of the possibility of using these functions in the development of programs for multiplying large-dimensional matrices. The work demonstrates the effectiveness of using the developed simple functions implemented by different methods in matrix multiplication programs. The prospects of further work in this direction are noted, having in mind the analysis of the possibility of using artificial intelligence methods to increase efficiency and facilitate the development of parallel programs with large-sized matrices.


Author(s):  
Olga Mikhaylovna Tikhonova ◽  
Alexander Fedorovich Rezchikov ◽  
Vladimir Andreevich Ivashchenko ◽  
Vadim Alekseevich Kushnikov

The paper presents the system of predicting the indicators of accreditation of technical universities based on J. Forrester mechanism of system dynamics. According to analysis of cause-and-effect relationships between selected variables of the system (indicators of accreditation of the university) there was built the oriented graph. The complex of mathematical models developed to control the quality of training engineers in Russian higher educational institutions is based on this graph. The article presents an algorithm for constructing a model using one of the simulated variables as an example. The model is a system of non-linear differential equations, the modelling characteristics of the educational process being determined according to the solution of this system. The proposed algorithm for calculating these indicators is based on the system dynamics model and the regression model. The mathematical model is constructed on the basis of the model of system dynamics, which is further tested for compliance with real data using the regression model. The regression model is built on the available statistical data accumulated during the period of the university's work. The proposed approach is aimed at solving complex problems of managing the educational process in universities. The structure of the proposed model repeats the structure of cause-effect relationships in the system, and also provides the person responsible for managing quality control with the ability to quickly and adequately assess the performance of the system.


1986 ◽  
Vol 18 (7-8) ◽  
pp. 239-248 ◽  
Author(s):  
Sung Ryong Ha ◽  
Dwang Ho Lee ◽  
Sang Eun Lee

Laboratory scale experiments were conducted to develop a mathematical model for the anaerobic digestion of a mixture of night soil and septic tank sludge. The optimum mixing ratio by volume between night soil and septic tank sludge was found to be 7:3. Due to the high solids content in the influent waste, mixed-liquor volatile suspended solids (MLVSS) was not considered to be a proper parameter for biomass concentration, therefore, the active biomass concentration was estimated based on deoxyribonucleic acid (DNA) concentration in the reactor. The weight ratio between acidogenic bacteria and methanogenic bacteria in the mixed culture of a well-operated anaerobic digester was approximately 3:2. The proposed model indicates that the amount of volatile acid produced and the gas production rate can be expressed as a function of hydraulic residence time (HRT). The kinetic constants of the two phases of the anaerobic digestion process were determined, and a computer was used to simulate results using the proposed model for the various operating parameters, such as BOD5 and volatile acid concentrations in effluent, biomass concentrations and gas production rates. These were consistent with the experimental data.


2021 ◽  
Vol 9 (2) ◽  
pp. 118
Author(s):  
Xinqing Zhuang ◽  
Keliang Yan ◽  
Pan Gao ◽  
Yihua Liu

Anchor dragging is a major threat to the structural integrity of submarine pipelines. A mathematical model in which the mechanical model of chain and the bearing model of anchor were coupled together. Based on the associated flow rule, an incremental procedure was proposed to solve the spatial state of anchor until it reaches the ultimate embedding depth. With an indirect measurement method for the anchor trajectory, a model test system was established. The mathematical model was validated against some model tests, and the effects of two parameters were studied. It was found that both the ultimate embedding depth of a dragging anchor and the distance it takes to reach the ultimate depth increase with the shank-fluke pivot angle, but decrease as the undrained shear strength of clay increases. The proposed model is supposed to be useful for the embedding depth calculation and guiding the design of the pipeline burial depth.


Author(s):  
S. Blom ◽  
S. Darabi ◽  
M. Huisman ◽  
M. Safari

AbstractA commonly used approach to develop deterministic parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to reason about such compiler directives, in particular to show that they do not change the behaviour of the program. Moreover, the verification technique is tool-supported and can be combined with proving functional correctness of the program. To develop our verification technique, we propose a simple intermediate representation (syntax and semantics) that captures the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorised and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show how a widely used subset of OpenMP can be encoded into this intermediate representation. Our verification technique builds on the notion of iteration contract to specify the behaviour of basic blocks; we show that if iteration contracts are manually specified for single blocks, then that is sufficient to automatically reason about data race freedom of the composed program. Moreover, we also show that it is sufficient to establish functional correctness on a linearised version of the original program to conclude functional correctness of the parallel program. Finally, we exemplify our approach on an example OpenMP program, and we discuss how tool support is provided.


Electronics ◽  
2021 ◽  
Vol 10 (15) ◽  
pp. 1843
Author(s):  
Jelena Vlaović ◽  
Snježana Rimac-Drlje ◽  
Drago Žagar

A standard called MPEG Dynamic Adaptive Streaming over HTTP (MPEG DASH) ensures the interoperability between different streaming services and the highest possible video quality in changing network conditions. The solutions described in the available literature that focus on video segmentation are mostly proprietary, use a high amount of computational power, lack the methodology, model notation, information needed for reproduction, or do not consider the spatial and temporal activity of video sequences. This paper presents a new model for selecting optimal parameters and number of representations for video encoding and segmentation, based on a measure of the spatial and temporal activity of the video content. The model was developed for the H.264 encoder, using Structural Similarity Index Measure (SSIM) objective metrics as well as Spatial Information (SI) and Temporal Information (TI) as measures of video spatial and temporal activity. The methodology that we used to develop the mathematical model is also presented in detail so that it can be applied to adapt the mathematical model to another type of an encoder or a set of encoding parameters. The efficiency of the segmentation made by the proposed model was tested using the Basic Adaptation algorithm (BAA) and Segment Aware Rate Adaptation (SARA) algorithm as well as two different network scenarios. In comparison to the segmentation available in the relevant literature, the segmentation based on the proposed model obtains better SSIM values in 92% of cases and subjective testing showed that it achieves better results in 83.3% of cases.


Author(s):  
Xuan Li ◽  
Bingkui Chen ◽  
Yawen Wang ◽  
Guohua Sun ◽  
Teik C. Lim

In this paper, the planar double-enveloping method is presented for the generation of tooth profiles of the internal gear pair for various applications, such as gerotors and gear reducers. The main characteristic of this method is the existence of double contact between one tooth pair such that the sealing property, the load capacity and the transmission precision can be significantly improved as compared to the conventional configuration by the single-enveloping theory. Firstly, the generation principle of the planar double-enveloping method is introduced. Based on the coordinate transformation and the envelope theory, the general mathematical model of the double-enveloping internal gear pair is presented. By using this model, users can directly design different geometrical shape profiles to obtain a double-enveloping internal gear pair with better meshing characteristics. Secondly, to validate the effectiveness of the proposed model, specific mathematical formulations of three double-enveloping internal gear pairs which apply circular, parabolic and elliptical curves as the generating curves are given. The equations of tooth profiles and meshing are derived and the composition of tooth profiles is analyzed. Finally, numerical examples are provided for an illustration.


2016 ◽  
Vol 10 (10) ◽  
pp. 133
Author(s):  
Mohammad Ali Nasiri Khalili ◽  
Mostafa Kafaei Razavi ◽  
Morteza Kafaee Razavi

Items supplies planning of a logistic system is one of the major issue in operations research. In this article the aim is to determine how much of each item per month from each supplier logistics system requirements must be provided. To do this, a novel multi objective mixed integer programming mathematical model is offered for the first time. Since in logistics system, delivery on time is very important, the first objective is minimization of time in delivery on time costs (including lack and maintenance costs) and the cost of purchasing logistics system. The second objective function is minimization of the transportation supplier costs. Solving the mathematical model shows how to use the Multiple Objective Decision Making (MODM) can provide the ensuring policy and transportation logistics needed items. This model is solved with CPLEX and computational results show the effectiveness of the proposed model.


2013 ◽  
Vol 655-657 ◽  
pp. 2262-2265
Author(s):  
Jian Guo Kong

Air traffic flow management is the key to evaluate airspace capacity reasonably and accurately. Based on the flight features of terminal route intersection, this paper builds a mathematical model for scattered flight of departure aircraft, and then evaluates the terminal capacity based on this model. By combining data from Flight Data Recorder (FDR) and flight schedule with the model, an example-runway 02R of Guangzhou Baiyun airport terminal was given to show the effectiveness of the proposed model.


Sign in / Sign up

Export Citation Format

Share Document