学位论文 > 优秀研究生学位论文题录展示

多核软件形式化建模、验证及性能评价方法研究

作　者: 林英
导　师: 李彤
学　校: 云南大学
专　业: 系统分析与集成
关键词: 多核 Petri网形式化软件开发性能评价 MTP-PN
分类号: TP311.52
类　型: 博士论文
年　份: 2013年
下　载: 64次
引　用: 0次
阅　读: 论文下载

内容摘要

新型多核体系结构的出现及主流化,在满足用户对高性能及低功耗双重需求的同时,对并行程序设计研究也产生了重要的影响,带来了新的挑战。研发有效的方法与工具,支持程序设计人员开发与多核相适应的并行软件是目前多核并行编程领域面临的一个关键技术问题。围绕开发正确、高性能和可扩展多核应用程序这一目标,本文首先研究形式化开发多核应用程序的方法,借助Petri网直观的图形表现能力和严密的数学基础,通过定性分析被建模系统的动态行为以及定量计算被建模系统的各种性能指标,有效支持多核程序开发过程中的正确性验证和性能评价；其次,研究多核加速串行程序的方法,提出串行程序并行优化的一种解决思路,通过构造串行程序的程序依赖图,并将此程序依赖图转换为Petri网,借助Petri网丰富的模型分析方法挖掘串行程序内在的并行性,以打造出更多支持多线程并行运行的应用软件,更好地利用多核平台资源。本文主要研究成果包括：(1)面向多核多线程并行程序建模的需求,基于Petri网理论,提出多线程程序Petri网模型MTP-PN (Multi-threaded Program Petri Nets)。MTP-PN通过抽象描述多线程程序,使得程序员可以把更多的精力投入到并行程序本身而非其具体实现细节,通过建模多线程程序的结构及功能、线程之间的交互以及对共享资源的访问,能够有效描述出程序的执行流程以及线程之间并发、同步、资源冲突等特性；(2)基于MTP-PN,给出验证该模型结构性质以及动态性质的相关算法。通过这些验证算法,能够有效在软件开发的早期发现程序设计流程中是否存在竞争、死锁、活锁等常见并发错误问题,从而减少设计错误、提高软件系统的可靠性；(3)针对多核软件开发性能分析与评价的需求,扩展MTP-PN为广义随机MTP-PN。广义随机MTP-PN的构建,不但能够定量分析程序的各项性能指标,也为缓解状态爆炸问题提供了一种解决的途径。基于该模型,评价多核引入对程序性能的影响,以优化软件性能,该方法对指导多核编程具有重要作用：(4)给出构建程序依赖图的算法,给出把程序依赖图转换为Petri网的算法。该方法除了可以借助Petri网理论来分析程序运行过程中是否存在冲突和死锁等情况以外,还可以很直观地发现程序运行中的各个模块之间的相互依赖关系,为形式化分析程序模块之间的依赖关系及挖掘串行程序内在并行性打下了基础；(5)给出基于库所不变量技术对Petri网进行分析的方法。实例说明该方法可以有效识别非循环并行性,提高并行挖掘的能力,从而为并行优化串行程序提供一种新的实用分析方法。本文基于Petri网理论,并根据特定需求进行扩充和改进,不但有效支持了软件开发过程中的正确性验证和性能调整,也为现有串行程序的并行化改造提供了一种新的解决思路。随着多核这一并行结构已经成为桌面系统通用处理器的主流,论文的工作有较好的研究意义和应用价值。

全文目录

摘要  3-5
Abstract  5-7
目录  7-11
第1章绪论  11-24
  本章目标  11
  1.1 研究背景  11-19
    1.1.1 多核处理器体系结构的出现  11-14
    1.1.2 并发与并行  14-15
    1.1.3 多核时代软件开发面临的机遇与挑战  15-17
    1.1.4 形式化开发并发软件  17-19
  1.2 本文主要工作  19-22
    1.2.1 研究目标及意义  19
    1.2.2 研究思路及研究内容  19-21
    1.2.3 主要贡献  21-22
  1.3 论文结构  22-24
第2章相关研究综述  24-31
  本章目标  24
  2.1 引言  24-25
  2.2 PETRI网建模和分析并发程序  25-26
  2.3 并行程序性能分析与评价  26-29
  2.4 串行程序并行化  29-30
  2.5 小结  30-31
第3章研究相关理论基础  31-43
  本章目标  31
  3.1 引言  31
  3.2 基于多核架构的软件开发  31-34
    3.2.1 多核并行编程模型  31-32
    3.2.2 多核并行设计方法  32-34
  3.3 PETRI网基本理论  34-37
    3.3.1 基本术语  34-36
    3.3.2 基本性质  36-37
  3.4 随机PETRI网  37-42
    3.4.1 随机Petri网定义  37-39
    3.4.2 广义随机Petri网  39-42
  3.5 小结  42-43
第4章多核软件的MTP-PN建模和验证  43-85
  本章目标  43
  4.1 引言  43-44
  4.2 多线程程序抽象  44-47
  4.3 MTP-PN建模  47-55
    4.3.1 MTP-PN定义  47-48
    4.3.2 建模程序基本控制结构  48-51
    4.3.3 建模线程交互  51-55
  4.4 MTP-PN建模规则及步骤  55-64
    4.4.1 建模规则  55-62
    4.4.2 建模步骤  62-64
  4.5 MTP-PN基本性质及其验证  64-79
    4.5.1 结构性质及相关验证算法  65-71
    4.5.2 动态性质及相关验证算法  71-78
    4.5.3 合理性定义及其验证算法  78-79
  4.6 建模实例  79-83
    4.6.1 模型建立  79-82
    4.6.2 模型分析  82-83
  4.7 小结  83-85
第5章基于广义随机MTP-PN模型的软件性能评价  85-102
  本章目标  85
  5.1 引言  85-86
  5.2 广义随机MTP-PN模型的建立  86-93
    5.2.1 广义随机MTP-PN定义  86
    5.2.2 瞬时变迁与时间变迁的确定  86-91
    5.2.3 随机开关的确定  91-93
  5.3 基于广义随机MTP-PN的软件性能评价  93-101
    5.3.1 广义随机MTP-PN的性能评价  93-94
    5.3.2 多核架构下广义随机MTP-PN的性能评价  94-101
  5.4 小结  101-102
第6章多核加速串行程序  102-128
  本章目标  102
  6.1 引言  102-103
  6.2 程序分析  103-106
    6.2.1 控制依赖  103-105
    6.2.2 数据依赖  105-106
  6.3 程序依赖图构建  106-121
    6.3.1 控制依赖图  106-113
    6.3.2 数据依赖图  113-119
    6.3.3 程序依赖图  119-121
  6.4 程序依赖图转换成P/T网  121-127
    6.4.1 转换规则  121-122
    6.4.2 转换算法  122-127
  6.5 小结  127-128
第7章基于P不变量结构分解的并行识别方法  128-143
  本章目标  128
  7.1 引言  128
  7.2 基于PETRI网的并行化方法研究  128-129
  7.3 基于P不变量结构分解方法  129-136
    7.3.1 P不变量  129-130
    7.3.2 求解P不变量  130-136
  7.4 并行识别  136-140
    7.4.1 基于库所不变量的并行识别条件  136-139
    7.4.2 程序分析  139-140
  7.5 反例展示  140-142
  7.6 小结  142-143
第8章案例研究  143-167
  本章目标  143
  8.1 案例一 (个人防火墙关键技术在多核平台上的建模、验证与实现)  143-158
    8.1.1 系统MTP-PN建模  144-148
    8.1.2 基于广义随机MTP-PN的性能分析  148-153
    8.1.3 系统实现  153-156
    8.1.4 小结  156-158
  8.2 案例二 (矩阵相乘算法在多核平台上的建模、验证与实现)  158-167
    8.2.1 模型建立  158-160
    8.2.2 性能评价  160-162
    8.2.3 多核架构下的性能评价  162-164
    8.2.4 实验结果对比及分析  164-166
    8.2.5 小结  166-167
第9章总结与展望  167-170
  9.1 主要贡献  167-168
  9.2 进一步的研究工作  168-170
参考文献  170-177
攻读博士学位期间主持和参与的课题  177-178
攻读博士学位期间发表和录用的论文  178-179
致谢  179

多核软件形式化建模、验证及性能评价方法研究

内容摘要

全文目录

相似论文