本文關鍵詞：基于符號執(zhí)行的MPI程序分析與驗證技術研究　出處：《國防科學技術大學》2016年博士論文　論文類型：學位論文

  更多相關文章： 符號執(zhí)行 MPI 死鎖 緩沖區(qū)錯誤 同步錯誤 懶惰匹配 面向死鎖的符號執(zhí)行引導

【摘要】：軟件可信性提高是計算機科學中的重要研究問題。MPI是高性能計算領域開發(fā)并發(fā)程序的主流框架,大部分運行在超級計算機上的并發(fā)程序是采用MPI開發(fā)的,有些開發(fā)代價超過幾十人年�？紤]到使用MPI開發(fā)的高性能應用的規(guī)模以及高性能計算中心的高昂構建、維護費用,MPI程序的可信性保障問題日漸引起人們的重視,而MPI程序的分析和驗證技術作為可信性提高的手段,成為大規(guī)模并行程序開發(fā)的關鍵技術。由于MPI程序缺陷可能輸入相關,即只有在某些特定輸入的時候才表現(xiàn)出來,不提供輸入覆蓋的技術如測試、正確性檢查、動態(tài)驗證等,難以捕獲到這些輸入相關缺陷。符號執(zhí)行是上世紀70年代提出的一種基于約束求解的程序分析技術,可以自動化地探索程序路徑空間。符號執(zhí)行可用于程序的缺陷查找、自動測試和自動驗證。本文基本思路就是使用符號執(zhí)行來分析MPI程序。然而,作為一種通用的基本程序分析方法,符號執(zhí)行在應用于MPI程序分析上時,面臨挑戰(zhàn):面對MPI程序本身的不確定性以及復雜性,在輸入覆蓋之外,符號執(zhí)行本身無法提供MPI程序的非確定性覆蓋;由于符號執(zhí)行本身的特性,在分析規(guī)模較大的MPI程序時,其可擴展性面臨一定的挑戰(zhàn)。本文圍繞這兩方面的挑戰(zhàn)展開了研究,旨在進一步提高MPI程序的可信性。本文的主要研究內(nèi)容包括:1.同步MPI程序的符號執(zhí)行方法�，F(xiàn)存的絕大部分MPI程序缺陷檢測方法不能同時提供輸入和不確定性的雙重覆蓋,因此可能存在漏報問題。而在MPI程序中,人們?yōu)榱双@取高性能,允許所謂的“通配接收”,即標記和接收源允許使用通配符,運行時才決定此接收操作是和具體的哪個發(fā)送操作相匹配,這就帶來了一定的非確定性。針對帶有通配接收的阻塞MPI程序,本文采用符號執(zhí)行來保證輸入空間的覆蓋,使用懶惰匹配的方法保證通配接收帶來的非確定性覆蓋,并提出了一種即時調(diào)度方法來減少盲目的交疊遍歷;另外,我們證明了依據(jù)此調(diào)度方法,不會漏掉通配接收的匹配而導致漏報死鎖。在基準測試集上的實驗表明,該方法可以有效地找到程序中的死鎖、運行時錯誤等。2.異步MPI程序的符號執(zhí)行方法。人們?yōu)榱碎_發(fā)高效的MPI程序,盡可能使得MPI任務的計算時間和底層MPI庫的通信時間重疊,常常通過調(diào)用非阻塞接口的方法來實現(xiàn)。然而,本文之前針對阻塞MPI程序提出的方法在面對非阻塞MPI調(diào)用的時候,無法直接適用。為了繼續(xù)保持不確定性和輸入空間的雙重覆蓋,本文擴展了懶惰匹配方法,其主要思想是盡可能地推遲非確定性源接收的匹配時機。另一方面,符號執(zhí)行的路徑空間爆炸問題在分析MPI程序的時候更加突出:在沒有采用路徑削減技術的情況下,路徑數(shù)目與程序的進程數(shù)、通配接收對應的匹配數(shù)、程序的分支數(shù)目都呈指數(shù)關系。本文提出了一種面向死鎖的符號執(zhí)行引導技術,根據(jù)已有路徑信息,把引導問題轉換成為一個死鎖的模型檢驗問題,根據(jù)結果來引導符號執(zhí)行更快找到死鎖。3.MPI緩沖區(qū)錯誤檢測。非阻塞MPI調(diào)用能夠通過重疊部分計算和通信過程,從而能夠有效降低通信開銷,但是可能帶來應用程序和底層MPI庫的緩沖區(qū)錯誤。本文基于所提出的MPI程序符號執(zhí)行方法提出了一種查找輸入相關的緩沖區(qū)錯誤的方法,使用一個性質(zhì)來規(guī)約非阻塞通信綁定的緩沖區(qū)上發(fā)生的事件應該滿足的時序,然后在符號執(zhí)行過程中對每條路徑進行檢查。同時針對檢查方法中需要對大量內(nèi)存訪問指令的解釋執(zhí)行增加檢查的問題,提出了兩種優(yōu)化方法,以減少在內(nèi)存訪問指令處的檢查數(shù)目。此外,本文基于同步以及異步MPI程序的符號執(zhí)行方法,實現(xiàn)了MPI符號執(zhí)行平臺MPISE。MPISE針對MPI程序的源代碼進行分析,能夠檢測MPI程序的死鎖、緩沖區(qū)錯誤與運行時錯誤,其主要優(yōu)點有:為MPI程序分析提供輸入和通配接收帶來的非確定性接收雙重覆蓋、支持異步調(diào)用、不需要修改用戶源代碼等。在驗證的程序規(guī)模方面,本文已使用MPISE分析最大多達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.

【學位授予單位】：國防科學技術大學
【學位級別】：博士
【學位授予年份】：2016
【分類號】：TP311.1

【相似文獻】

相關期刊論文 前10條

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

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

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

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

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

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

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

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

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

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

相關會議論文 前3條

1 林錦濱;張曉菲;劉暉;;符號執(zhí)行技術研究[A];全國計算機安全學術交流會論文集（第二十四卷）[C];2009年

2 范海虹;;俄漢姓名稱呼對比[A];外語語言教學研究——黑龍江省外國語學會第十一次學術年會論文集[C];1997年

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

相關博士學位論文 前8條

1 張羽豐;符號執(zhí)行可擴展性及可行性關鍵技術研究[D];國防科學技術大學;2013年

2 李游;統(tǒng)一的軟件測試控制流覆蓋準則體系及其符號執(zhí)行制導技術研究[D];南京大學;2016年

3 傅先進;基于符號執(zhí)行的MPI程序分析與驗證技術研究[D];國防科學技術大學;2016年

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

5 安靖;動態(tài)符號執(zhí)行關鍵技術研究[D];北京郵電大學;2014年

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

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

8 邢學智;基于TTCN-3語言的測試理論與技術研究[D];中國科學技術大學;2010年

相關碩士學位論文 前10條

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

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

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

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

5 陳冰;符號執(zhí)行技術研究與改進[D];南京大學;2014年

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

7 鮑鐵勻;符號執(zhí)行制導技術及其應用研究[D];南京大學;2016年

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

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

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

，

本文編號：1368501