發(fā)布時(shí)間：2018-01-02 08:41

  本文關(guān)鍵詞：基于符號(hào)執(zhí)行的MPI程序分析與驗(yàn)證技術(shù)研究　出處：《國(guó)防科學(xué)技術(shù)大學(xué)》2016年博士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： 符號(hào)執(zhí)行 MPI 死鎖 緩沖區(qū)錯(cuò)誤 同步錯(cuò)誤 懶惰匹配 面向死鎖的符號(hào)執(zhí)行引導(dǎo)

【摘要】：軟件可信性提高是計(jì)算機(jī)科學(xué)中的重要研究問題。MPI是高性能計(jì)算領(lǐng)域開發(fā)并發(fā)程序的主流框架,大部分運(yùn)行在超級(jí)計(jì)算機(jī)上的并發(fā)程序是采用MPI開發(fā)的,有些開發(fā)代價(jià)超過幾十人年。考慮到使用MPI開發(fā)的高性能應(yīng)用的規(guī)模以及高性能計(jì)算中心的高昂構(gòu)建、維護(hù)費(fèi)用,MPI程序的可信性保障問題日漸引起人們的重視,而MPI程序的分析和驗(yàn)證技術(shù)作為可信性提高的手段,成為大規(guī)模并行程序開發(fā)的關(guān)鍵技術(shù)。由于MPI程序缺陷可能輸入相關(guān),即只有在某些特定輸入的時(shí)候才表現(xiàn)出來,不提供輸入覆蓋的技術(shù)如測(cè)試、正確性檢查、動(dòng)態(tài)驗(yàn)證等,難以捕獲到這些輸入相關(guān)缺陷。符號(hào)執(zhí)行是上世紀(jì)70年代提出的一種基于約束求解的程序分析技術(shù),可以自動(dòng)化地探索程序路徑空間。符號(hào)執(zhí)行可用于程序的缺陷查找、自動(dòng)測(cè)試和自動(dòng)驗(yàn)證。本文基本思路就是使用符號(hào)執(zhí)行來分析MPI程序。然而,作為一種通用的基本程序分析方法,符號(hào)執(zhí)行在應(yīng)用于MPI程序分析上時(shí),面臨挑戰(zhàn):面對(duì)MPI程序本身的不確定性以及復(fù)雜性,在輸入覆蓋之外,符號(hào)執(zhí)行本身無法提供MPI程序的非確定性覆蓋;由于符號(hào)執(zhí)行本身的特性,在分析規(guī)模較大的MPI程序時(shí),其可擴(kuò)展性面臨一定的挑戰(zhàn)。本文圍繞這兩方面的挑戰(zhàn)展開了研究,旨在進(jìn)一步提高M(jìn)PI程序的可信性。本文的主要研究?jī)?nèi)容包括:1.同步MPI程序的符號(hào)執(zhí)行方法。現(xiàn)存的絕大部分MPI程序缺陷檢測(cè)方法不能同時(shí)提供輸入和不確定性的雙重覆蓋,因此可能存在漏報(bào)問題。而在MPI程序中,人們?yōu)榱双@取高性能,允許所謂的“通配接收”,即標(biāo)記和接收源允許使用通配符,運(yùn)行時(shí)才決定此接收操作是和具體的哪個(gè)發(fā)送操作相匹配,這就帶來了一定的非確定性。針對(duì)帶有通配接收的阻塞MPI程序,本文采用符號(hào)執(zhí)行來保證輸入空間的覆蓋,使用懶惰匹配的方法保證通配接收帶來的非確定性覆蓋,并提出了一種即時(shí)調(diào)度方法來減少盲目的交疊遍歷;另外,我們證明了依據(jù)此調(diào)度方法,不會(huì)漏掉通配接收的匹配而導(dǎo)致漏報(bào)死鎖。在基準(zhǔn)測(cè)試集上的實(shí)驗(yàn)表明,該方法可以有效地找到程序中的死鎖、運(yùn)行時(shí)錯(cuò)誤等。2.異步MPI程序的符號(hào)執(zhí)行方法。人們?yōu)榱碎_發(fā)高效的MPI程序,盡可能使得MPI任務(wù)的計(jì)算時(shí)間和底層MPI庫的通信時(shí)間重疊,常常通過調(diào)用非阻塞接口的方法來實(shí)現(xiàn)。然而,本文之前針對(duì)阻塞MPI程序提出的方法在面對(duì)非阻塞MPI調(diào)用的時(shí)候,無法直接適用。為了繼續(xù)保持不確定性和輸入空間的雙重覆蓋,本文擴(kuò)展了懶惰匹配方法,其主要思想是盡可能地推遲非確定性源接收的匹配時(shí)機(jī)。另一方面,符號(hào)執(zhí)行的路徑空間爆炸問題在分析MPI程序的時(shí)候更加突出:在沒有采用路徑削減技術(shù)的情況下,路徑數(shù)目與程序的進(jìn)程數(shù)、通配接收對(duì)應(yīng)的匹配數(shù)、程序的分支數(shù)目都呈指數(shù)關(guān)系。本文提出了一種面向死鎖的符號(hào)執(zhí)行引導(dǎo)技術(shù),根據(jù)已有路徑信息,把引導(dǎo)問題轉(zhuǎn)換成為一個(gè)死鎖的模型檢驗(yàn)問題,根據(jù)結(jié)果來引導(dǎo)符號(hào)執(zhí)行更快找到死鎖。3.MPI緩沖區(qū)錯(cuò)誤檢測(cè)。非阻塞MPI調(diào)用能夠通過重疊部分計(jì)算和通信過程,從而能夠有效降低通信開銷,但是可能帶來應(yīng)用程序和底層MPI庫的緩沖區(qū)錯(cuò)誤。本文基于所提出的MPI程序符號(hào)執(zhí)行方法提出了一種查找輸入相關(guān)的緩沖區(qū)錯(cuò)誤的方法,使用一個(gè)性質(zhì)來規(guī)約非阻塞通信綁定的緩沖區(qū)上發(fā)生的事件應(yīng)該滿足的時(shí)序,然后在符號(hào)執(zhí)行過程中對(duì)每條路徑進(jìn)行檢查。同時(shí)針對(duì)檢查方法中需要對(duì)大量?jī)?nèi)存訪問指令的解釋執(zhí)行增加檢查的問題,提出了兩種優(yōu)化方法,以減少在內(nèi)存訪問指令處的檢查數(shù)目。此外,本文基于同步以及異步MPI程序的符號(hào)執(zhí)行方法,實(shí)現(xiàn)了MPI符號(hào)執(zhí)行平臺(tái)MPISE。MPISE針對(duì)MPI程序的源代碼進(jìn)行分析,能夠檢測(cè)MPI程序的死鎖、緩沖區(qū)錯(cuò)誤與運(yùn)行時(shí)錯(cuò)誤,其主要優(yōu)點(diǎn)有:為MPI程序分析提供輸入和通配接收帶來的非確定性接收雙重覆蓋、支持異步調(diào)用、不需要修改用戶源代碼等。在驗(yàn)證的程序規(guī)模方面,本文已使用MPISE分析最大多達(dá)80 k LOC的MPI程序。
[Abstract]:To improve the software trustworthiness is.MPI important research problems in Computer Science in the field of high performance computing framework is the mainstream development of concurrent programs, most run on a supercomputer concurrent program is developed using MPI, some development costs more than dozens of years. Considering the high performance applications developed using the MPI scale and high performance computing center high building, maintenance costs, dependability problem MPI program has attracted people's attention, and the MPI program analysis and verification techniques to improve credibility as a means to become the key technology of large-scale parallel program development. Because the MPI bugs may enter, i.e. only when certain inputs do not appear, do not provide input covering techniques such as testing, examination, dynamic verification, to capture these input related defects. Symbolic execution is the world Ji 70s proposed an analysis technique of constraint solving based on the procedures, can automatically explore the program path space. Can be used to find the defects of symbolic execution procedures, automatic test and automatic verification. The basic idea of this paper is to use symbolic execution to analyze MPI program. However, as a basic procedure of general analysis method, symbolic execution face the challenge in using MPI analysis program, the MPI program itself: in the face of uncertainty and complexity in the input coverage, symbolic execution itself cannot provide non deterministic MPI program by covering; to enforce its own characteristics in the analysis of symbols, the larger MPI program, its scalability facing certain challenges. This paper focuses on the two challenges of research, to further improve the credibility of the MPI program. The main contents of this paper include: 1. the symbol synchronization of MPI Method of execution. Most of the existing MPI program defect detection method can not provide input and double coverage uncertainty at the same time, so there may be missing. While in the MPI program, in order to obtain high performance, allowing the so-called "wildcard receiving", which are markers and receiving the source allows the use of wildcards, decide when this operation the receive operation and which is sending the specific operation, which brings uncertainty to some extent. Aiming at receiving wildcard blocking MPI program, this paper uses symbolic execution to ensure the input space coverage, using the method of lazy, that covers the non deterministic wildcard receive brought, and put forward a kind of instant scheduling method to reduce overlapping traversal blindness; in addition, we prove that the scheduling method based on this, will not miss the wildcard matching and receiving lead to underreporting deadlock. In the benchmark set. Experiment shows that this method can effectively find the deadlock in the program, such as asynchronous MPI program error.2. symbolic execution method runs. In order to develop efficient MPI program, as much as possible so that the communication time MPI task computing time and the underlying MPI library overlap, often by adjusting method using non blocking interface to achieve. However, this method for blocking before MPI procedure is proposed in the face of non blocking MPI call, can not be directly applicable. In order to continue to maintain double coverage uncertainty and input space, this paper extends the lazy matching method, the main idea is as far as possible, the time delay uncertainty source received. On the other hand, path the space explosion problem of symbolic execution is more prominent in the analysis of the MPI program: in the absence of the path cut technology, path number and course number, distribution of receiving The matching number should be the number of branches of the program have an exponential relationship. This paper presents a deadlock oriented symbolic execution guide technology, according to the existing path information, to guide the problem into a model checking problem of deadlock, according to the results to guide the symbolic execution faster to find errors in.3.MPI buffer deadlock detection. Non blocking MPI call through overlap of computation and communication process, which can effectively reduce the communication overhead, but may bring the buffer application and the underlying MPI library error. This paper proposed the implementation of the program symbol MPI proposed a method to find the input buffer related errors based on the sequential use of a property specification non blocking communication binding buffer events should be satisfied, then for each path in check during symbolic execution. At the same time for the inspection method for To access a lot of memory instructions to explain the implementation of increased inspection problems, put forward two kinds of optimization methods, to reduce the number of check in memory access instructions. In addition, the implementation method of synchronous and asynchronous MPI program based on the realization of the MPI symbol, symbolic execution platform MPISE.MPISE for MPI source code analysis can deadlock detection of the MPI program, running buffer error and error, its main advantages are: to provide non deterministic input and wildcard receive brought to receive double coverage for MPI program analysis, support for asynchronous calls, the user does not need to modify the source code. In the verification of the program size, this paper has analyzed the maximum up to 80 K LOC MPI program using MPISE.

【學(xué)位授予單位】：國(guó)防科學(xué)技術(shù)大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP311.1

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 林夢(mèng)香;陳胤立;陳睿;周剛;;基于懶替換的C符號(hào)執(zhí)行[J];北京航空航天大學(xué)學(xué)報(bào);2009年06期

2 洪宇;陳光;于見平;韓柯;;處理符號(hào)執(zhí)行中數(shù)組元素混淆的一種新方法[J];計(jì)算機(jī)應(yīng)用;2005年S1期

3 過辰楷;姬秀娟;許靜;;基于分支混淆算法的符號(hào)執(zhí)行技術(shù)[J];計(jì)算機(jī)科學(xué);2012年09期

4 劉杰;曹琰;魏強(qiáng);彭建山;;符號(hào)執(zhí)行中的循環(huán)依賴分析方法[J];計(jì)算機(jī)工程;2012年22期

5 黃暉;陸余良;夏陽;;基于動(dòng)態(tài)符號(hào)執(zhí)行的二進(jìn)制程序缺陷發(fā)現(xiàn)系統(tǒng)[J];計(jì)算機(jī)應(yīng)用研究;2013年09期

6 翁子盛;王寶生;林錦濱;;程序符號(hào)執(zhí)行中的數(shù)組分析[J];長(zhǎng)江大學(xué)學(xué)報(bào)(自然科學(xué)版)理工卷;2010年01期

7 賈春福;王志;劉昕;劉昕海;;路徑模糊:一種有效抵抗符號(hào)執(zhí)行的二進(jìn)制混淆技術(shù)[J];計(jì)算機(jī)研究與發(fā)展;2011年11期

8 周孔偉,蔡經(jīng)球;符號(hào)執(zhí)行—介于程序驗(yàn)證和程序調(diào)試之間的方法[J];小型微型計(jì)算機(jī)系統(tǒng);1982年04期

9 高仲儀 ,梁霞;符號(hào)執(zhí)行和測(cè)試數(shù)據(jù)輔助生成的實(shí)驗(yàn)系統(tǒng)[J];北京航空學(xué)院學(xué)報(bào);1988年04期

10 程紹銀;蔣凡;林錦濱;唐艷武;;基于有限回溯符號(hào)執(zhí)行的軟件疑似缺陷的自動(dòng)驗(yàn)證[J];清華大學(xué)學(xué)報(bào)(自然科學(xué)版);2009年S2期

相關(guān)會(huì)議論文 前3條

1 林錦濱;張曉菲;劉暉;;符號(hào)執(zhí)行技術(shù)研究[A];全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集（第二十四卷）[C];2009年

2 范海虹;;俄漢姓名稱呼對(duì)比[A];外語語言教學(xué)研究——黑龍江省外國(guó)語學(xué)會(huì)第十一次學(xué)術(shù)年會(huì)論文集[C];1997年

3 劉峻宇;李強(qiáng);余祥;何海洋;;基于符號(hào)執(zhí)行的指揮信息系統(tǒng)軟件缺陷檢測(cè)技術(shù)[A];2014第二屆中國(guó)指揮控制大會(huì)論文集（上）[C];2014年

相關(guān)博士學(xué)位論文 前8條

1 張羽豐;符號(hào)執(zhí)行可擴(kuò)展性及可行性關(guān)鍵技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2013年

2 李游;統(tǒng)一的軟件測(cè)試控制流覆蓋準(zhǔn)則體系及其符號(hào)執(zhí)行制導(dǎo)技術(shù)研究[D];南京大學(xué);2016年

3 傅先進(jìn);基于符號(hào)執(zhí)行的MPI程序分析與驗(yàn)證技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2016年

4 范文慶;分段符號(hào)執(zhí)行模型及其環(huán)境交互問題研究[D];北京郵電大學(xué);2010年

5 安靖;動(dòng)態(tài)符號(hào)執(zhí)行關(guān)鍵技術(shù)研究[D];北京郵電大學(xué);2014年

6 曹琰;面向軟件脆弱性分析的并行符號(hào)執(zhí)行技術(shù)研究[D];解放軍信息工程大學(xué);2013年

7 陳廳;動(dòng)態(tài)程序分析技術(shù)在軟件安全領(lǐng)域的研究[D];電子科技大學(xué);2013年

8 邢學(xué)智;基于TTCN-3語言的測(cè)試?yán)碚撆c技術(shù)研究[D];中國(guó)科學(xué)技術(shù)大學(xué);2010年

相關(guān)碩士學(xué)位論文 前10條

1 李奇軍;基于符號(hào)執(zhí)行的代碼靜態(tài)檢測(cè)方法研究與實(shí)現(xiàn)[D];電子科技大學(xué);2015年

2 柯明敏;動(dòng)態(tài)符號(hào)執(zhí)行在軟件漏洞自動(dòng)化發(fā)掘領(lǐng)域的應(yīng)用研究[D];電子科技大學(xué);2015年

3 康文濤;符號(hào)執(zhí)行工具KLEE約束求解優(yōu)化設(shè)計(jì)與實(shí)現(xiàn)[D];電子科技大學(xué);2014年

4 吳情彪;基于符號(hào)執(zhí)行的軟件污點(diǎn)分析研究[D];武漢郵電科學(xué)研究院;2016年

5 陳冰;符號(hào)執(zhí)行技術(shù)研究與改進(jìn)[D];南京大學(xué);2014年

6 李景曦;基于控制流分析的模糊測(cè)試技術(shù)研究[D];北京理工大學(xué);2016年

7 鮑鐵勻;符號(hào)執(zhí)行制導(dǎo)技術(shù)及其應(yīng)用研究[D];南京大學(xué);2016年

8 鄧維;形狀分析符號(hào)執(zhí)行引擎中的狀態(tài)合并[D];中國(guó)科學(xué)技術(shù)大學(xué);2016年

9 袁健;基于符號(hào)執(zhí)行的代碼安全檢查技術(shù)研究與實(shí)現(xiàn)[D];電子科技大學(xué);2016年

10 羅榮森;基于符號(hào)摘要的動(dòng)態(tài)符號(hào)執(zhí)行的研究[D];電子科技大學(xué);2016年

，

本文編號(hào)：1368501