Font Size: a A A

Formal Modeling,Verification And Performance Evaluation Of Multi-core Software

Posted on:2014-01-26Degree:DoctorType:Dissertation
Country:ChinaCandidate:Y LinFull Text:PDF
GTID:1228330401454013Subject:Systems analysis and integration
Abstract/Summary:PDF Full Text Request
The emergence of multi-core architecture meets the dual demands of high-performance and low-power consumption, but at the same time, it also brings new challenges in the area of parallel programming. Research of effective methods and tools to support multi-core parallel software development is an urgent problem now.Aiming at developing proper, high-performance and scalable multi-core applications, this dissertation firstly proposed a formal development method which is based on the theory of petri net. Due to its intuitive graphical expression capability and rigorous mathematical foundation, petri net is particularly suitable for representation and analysis of applications with concurrency, synchronization and conflict features. By qualitatively understanding modeled system’s dynamic behavior and quantitatively calculating various performance indicators, this formal method effectively supports validation and evaluation work in the early stage of multi-core software development. Secondly, a method of acceleration sequential applications on mulit-core architecture is also proposed. The purpose of constructing program dependence graph and then transforming it into petri net is to make use of various model analysis methods of petri net. Specifically, the main contents and contributions of this dissertation are as follows:(1) Based on the theory of petri net, method of constructing MTP-PN (Multi-threaded Program Petri Nets) is proposed to satisfy the modeling requirements of multi-threaded parallel programming. By an abstract description of multi-threaded program, MTP-PN allows programmer to put more energy into the parallel program itself rather than some specific implementation details. By modeling the structure, the function and threads interaction, MTP-PN can effectively represent multi-threaded program’s characteristics as concurrency, synchronization, resource conflicts, etc.;(2) Some verification algorithms which are dedicated to validate structure properties and dynamic properties of MTP-PN are proposed. These verification algorithms can help programmer to efficiently detect whether there have competition, deadlock, live lock or other common concurrency errors in the early stage of the program design phase, thereby reducing design errors, and improving the reliability of software systems;(3) To satisfy the demand of performance analysis and evaluation of multi-core software, a method of extending MTP-PN to generalized stochastic MTP-PN is introduced. Based on the generalized stochastic MTP-PN, it not only can alleviate the state explosion problem, but also can quantitatively analyze program’s various performance indicators;(4) Algorithms of constructing program dependence graph, as well as transforming program dependence graph into petri net are proposed. The method of transforming PDG to petri net not only helps programmer to detect conflicts and deadlocks existed in the program, but also helps programmer to easily find interdependencies among various modules of the program;(5) Analyzing petri net by P-invariant technology is proposed.Study case showed that this method can effectively identify non-loop parallelism and can improve the efficiency of inherent parallelism identification.This method provides a new practical analytical method of parallel optimization for sequential programs.Based on the theory of petri net, this dissertation not only effectively supports the verification and performance evaluation in the early stage of software development, but also provides a new approach on parallel optimization of sequential programs. As the polynuclear structure has been becoming the mainstream of the general-purpose processor, the work of this dissertation has certain research and application value.
Keywords/Search Tags:Multi-core, Petri net, formal software development, performance evaluation, MTP-PN
PDF Full Text Request
Related items