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

《多核软件形式化建模、验证及性能评价方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、独创性声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人或集体已经发表或撰写过的研究成果，对本文的研究做出贡献的集体和个人均已在论文中作了明确的说明并表示了谢意。研究生签名：率日期：论文使用和授权说明本人完全了解云南大学有关保留、使用学位论文的规定，即：学校有权保留并向国家有关部门或机构送交学位论文和论文电子版；允许论文被查阅或借阅；学校可以公布论文的全部或部分内容，可以采用影印、缩印或其他复制手段保存论文。(保密的论文在解

2、密后应遵循此规定)研究生签名：芈导师签名：—二够日期：本人及导师同意将学位论文提交至清华大学“中国学术期刊(光盘版)电子杂志社’’进行电子和网络出版，并编入CNKI系列数据库，传播本学位论文的全部或部分内容，同意按《中国优秀博硕士学位论文全文数据库出版章程》规定享受相关权益。研究生签名：二!社导师签名：—二够日期：＼必嬲摘要新型多核体系结构的出现及主流化，在满足用户对高性能及低功耗双重需求的同时，对并行程序设计研究也产生了重要的影响，带来了新的挑战。研发有效的方法与工具，支持程序设计人员开发与多核相适应

3、的并行软件是目前多核并行编程领域面临的一个关键技术问题。围绕开发正确、高性能和可扩展多核应用程序这一目标，本文首先研究形式化开发多核应用程序的方法，借助Petri网直观的图形表现能力和严密的数学基础，通过定性分析被建模系统的动态行为以及定量计算被建模系统的各种性能指标，有效支持多核程序开发过程中的正确性验证和性能评价；其次，研究多核加速串行程序的方法，提出串行程序并行优化的一种解决思路，通过构造串行程序的程序依赖图，并将此程序依赖图转换为Petri网，借助Petri网丰富的模型分析方法挖掘串行程序内在的

4、并行性，以打造出更多支持多线程并行运行的应用软件，更好地利用多核平台资源。本文主要研究成果包括：(1)面向多核多线程并行程序建模的需求，基于Petri网理论，提出多线程程序Petri网模型MTP．PN(Multi-threadedProgramPetriNets)。MTP．PN通过抽象描述多线程程序，使得程序员可以把更多的精力投入到并行程序本身而非其具体实现细节，通过建模多线程程序的结构及功能、线程之间的交互以及对共享资源的访问，能够有效描述出程序的执行流程以及线程之间并发、同步、资源冲突等特性；(2)

5、基于MTP．PN，给出验证该模型结构性质以及动态性质的相关算法。通过这些验证算法，能够有效在软件开发的早期发现程序设计流程中是否存在竞争、死锁、活锁等常见并发错误问题，从而减少设计错误、提高软件系统的可靠性；(3)针对多核软件开发性能分析与评价的需求，扩展MTP．PN为广义随机MTP。PN。广义随机MTP．PN的构建，不但能够定量分析程序的各项性能指标，也为缓解状态爆炸问题提供了一种解决的途径。基于该模型，评价多核引入对程序性能的影响，以优化软件性能，该方法对指导多核编程具有重要作用；(4)给出构建程序

6、依赖图的算法，给出把程序依赖图转换为Petri网的算法。该方法除了可以借助Petri网理论来分析程序运行过程中是否存在冲突和死锁等情况以外，还可以很直观地发现程序运行中的各个模块之间的相互依赖关系，为形式化分析程序模块之间的依赖关系及挖掘串行程序内在并行性打下了基础；(5)给出基于库所不变量技术对Petri网进行分析的方法。实例说明该方法可以有效识别非循环并行性，提高并行挖掘的能力，从而为并行优化串行程序提供一种新的实用分析方法。本文基于Petri网理论，并根据特定需求进行扩充和改进，不但有效支持了软件

7、开发过程中的正确性验证和性能调整，也为现有串行程序的并行化改造提供了一种新的解决思路。随着多核这一并行结构已经成为桌面系统通用处理器的主流，论文的工作有较好的研究意义和应用价值。关键词：多核；Petri网；形式化软件开发；性能评价；MTP．PNAbstractTheemergenceofmulti—corearchitecturemeetsthedualdemandsofhigh·performanceandlow-powerconsumption，butatthesametime，italsobrin

8、gsnewchallengesintheareaofparallelprogramming．Researchofeffectivemethodsandtoolstosupportmulti-coreparallelsoftwaredevelopmentisanurgentproblemnow．Aimingatdevelopingproper,high-performanceandscalablemulti—coreapplications，