基于符號(hào)執(zhí)行的MPI程序分析與驗(yàn)證技術(shù)研究.pdf

1、軟件可信性提高是計(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)，即只有在某些特定輸

2、入的時(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ù)雜性，在輸入覆蓋之外，

3、符號(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)榱双@取高性能，允許所謂的“通配接

4、收”，即標(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

5、.異步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í)候更加突出：

6、在沒有采用路徑削減技術(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程

7、序符號(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