摘 要:過程間并發(fā)程序分析問題是一個(gè)不可判定問題，理解這個(gè)不可判定問題的來源是發(fā)展一個(gè)有效的分析算法的基礎(chǔ)#65377;現(xiàn)有的證明[1]通過構(gòu)造三個(gè)并發(fā)任務(wù)的PCP問題實(shí)例，證明過程間并發(fā)程序分析是一個(gè)不可判定問題#65377;利用反射的思想，僅僅用兩個(gè)并發(fā)任務(wù)構(gòu)造該問題的一個(gè)PCP問題實(shí)例，證明在兩個(gè)并發(fā)任務(wù)的情況下，過程間并發(fā)程序分析是一個(gè)不可判定問題#65377;

關(guān)鍵詞:過程間并發(fā)程序分析; 上下文敏感; 同步敏感;不可判定問題;

中圖分類號(hào):TP311.5 文獻(xiàn)標(biāo)識(shí)碼:A

1 引 言

隨著現(xiàn)代軟件系統(tǒng)的日趨龐大，并發(fā)技術(shù)的廣泛運(yùn)用，過程間并發(fā)程序分析技術(shù)顯得更加重要，并且越來越得到廣泛的關(guān)注，然而，即使在只有兩個(gè)并發(fā)任務(wù)的情況下，過程間并發(fā)程序分析仍然可能是一個(gè)不可判定問題#65377;

由于路徑約束可能不可解，因此，就一般意義上的精確程序分析都是不可判定的，但即使不考慮路徑約束，簡單的將分支路徑的選擇視為不確定性選擇(這是程序分析普遍采用的近似方法)，過程間并發(fā)程序分析仍然是不可判定的^[1]#65377;第一次對(duì)這個(gè)問題給出了明確的結(jié)論和證明，由于精確的過程間并發(fā)程序分析是不可能的，近年來的研究工作大多考慮如何進(jìn)行近似的非精確分析^[5，6]，或者回避并發(fā)程序的同步^[7]#65377;盡管過程間并發(fā)程序分析是一個(gè)不可判定問題，但不是所有的程序都是不可判定的，通過對(duì)不可判定發(fā)生原因的分析，我們希望可以找出一大類程序?qū)嶋H上是可以進(jìn)行精確分析的#65377;

要找出不可判定的必要條件，就必須理解為什么會(huì)產(chǎn)生不可判定的情況，單獨(dú)的過程間分析和并發(fā)分析都是可判定的^[4，8]，但一旦結(jié)合起來就成了一個(gè)不可判定的問題，可以直觀的認(rèn)為，不可判定的情況在過程和并發(fā)產(chǎn)生了某種關(guān)系的情形下才會(huì)發(fā)生#65377;值得思考的是，過程發(fā)生在單個(gè)任務(wù)內(nèi)，而并發(fā)發(fā)生在任務(wù)間，這兩者之間是如何發(fā)生關(guān)系的呢?現(xiàn)有的證明^[1]通過構(gòu)造三個(gè)并發(fā)任務(wù)的PCP問題實(shí)例，證明了過程間并發(fā)程序分析過程間并發(fā)程序分析是一個(gè)不可判定問題#65377;意識(shí)到這個(gè)結(jié)論的不充分性^[1]，利用兩個(gè)上下文無關(guān)語言的交補(bǔ)充了它的第一個(gè)證明，并認(rèn)為這兩種證明方式是不等價(jià)的#65377;

本文利用反射的思想構(gòu)造了一個(gè)PCP問題實(shí)例，僅僅用兩個(gè)并發(fā)任務(wù)將該問題轉(zhuǎn)化為PCP問題，從而證明了:在兩個(gè)并發(fā)任務(wù)的情況下，過程間并發(fā)程序分析是一個(gè)不可判定問題#65377;證明的構(gòu)造過程直觀的顯示了，發(fā)生在任務(wù)內(nèi)的過程匹配和發(fā)生在任務(wù)間的同步匹配如何產(chǎn)生相互影響:任務(wù)的同步匹配關(guān)系被并發(fā)的其他任務(wù)反射回該任務(wù)本身，從而造成同步匹配與過程匹配的相互影響#65377;進(jìn)一步的，本文指出，同步匹配關(guān)系被反射回自身后，實(shí)際上反映的是對(duì)應(yīng)的并發(fā)任務(wù)的過程匹配關(guān)系#65377;不可判定的表現(xiàn)形式是，在一個(gè)任務(wù)內(nèi)形成兩個(gè)可交織的過程匹配，其中一個(gè)過程匹配是另一個(gè)并發(fā)任務(wù)的過程匹配通過同步匹配產(chǎn)生的“投影”#65377;

計(jì)算技術(shù)與自動(dòng)化2007年6月第26卷第2期繆 力等:過程間并發(fā)程序分析不可判定的一個(gè)新證明方法2 過程間并發(fā)程序模型

單過程程序結(jié)構(gòu)可通過控制流圖表達(dá)#65377;控制流圖CFG是一種有向圖，記為G=， 其中N是節(jié)點(diǎn)集，表示程序的控制點(diǎn);E是邊集，表示程序中所有語句;s 與e 是N 中兩個(gè)特殊節(jié)點(diǎn)，稱為初始節(jié)點(diǎn)與終止節(jié)點(diǎn)，從s有指向程序第一個(gè)語句節(jié)點(diǎn)的邊，程序的每個(gè)出口節(jié)點(diǎn)有指向e的邊#65377;

過程間控制流圖ICFG是對(duì)控制流圖CFG的擴(kuò)展，每個(gè)過程用一個(gè)完整的CFG表示，過程的調(diào)用和返回通過CALL邊和RETURN邊表示并連接到整個(gè)ICFG中#65377;

一個(gè)并發(fā)程序由多個(gè)并行執(zhí)行的任務(wù)構(gòu)成，每個(gè)任務(wù)表示為一個(gè)單獨(dú)的過程間控制流圖ICFG#65377;本文采用的同步模型與[1]完全一致，用invoke/accept機(jī)制實(shí)現(xiàn)同步操作#65377;

一個(gè)任務(wù)X通過語句invoke Y.E向另一個(gè)任務(wù)Y發(fā)送一個(gè)同步請(qǐng)求，任務(wù)Y通過accept E接受請(qǐng)求#65377;任務(wù)X發(fā)送同步請(qǐng)求后即被掛起，直到該同步請(qǐng)求被接受，反之，任務(wù)Y執(zhí)行到同步接受語句時(shí)也被掛起，直到有其他任務(wù)發(fā)出相應(yīng)的同步請(qǐng)求#65377;

對(duì)于過程間控制流圖，不是所有圖中連通的路徑都是可行的，可行路徑必須滿足過程匹配關(guān)系#65377;

定義2.1 過程匹配

并發(fā)程序中的一個(gè)任務(wù)是一個(gè)包括多個(gè)過程的獨(dú)立任務(wù)(程序)，程序中的一條可行路徑必須滿足過程匹配，即過程返回點(diǎn)必須匹配最近的過程調(diào)用點(diǎn)#65377;

利用上下文無關(guān)文法，可以形式化的表示這種匹配關(guān)系:

balance表示調(diào)用點(diǎn)的平衡關(guān)系#65377;

balance →(u balance)u|ε，(u表示進(jìn)入調(diào)用點(diǎn)u，)u表示從調(diào)用點(diǎn)u返回#65377;

matched表示調(diào)用點(diǎn)的匹配關(guān)系#65377;

matched→matched (u|balance #65377;

如果一個(gè)程序分析方法要求所有的路徑必須是滿足過程匹配的，則這種程序分析方法稱為上下文敏感的程序分析方法#65377;

定義2.2 同步匹配

對(duì)于一個(gè)并發(fā)程序中的一個(gè)任務(wù)，其一條執(zhí)行路徑中可能產(chǎn)生一個(gè)同步序列，該同步序列必須與其他并發(fā)任務(wù)產(chǎn)生的一個(gè)同步序列匹配#65377;

如果一個(gè)程序分析方法要求所有的路徑必須是滿足同步匹配的，則這種程序分析方法稱為同步敏感的程序分析方法#65377;注意同步匹配只是要求兩個(gè)任務(wù)的同步序列對(duì)應(yīng)匹配，并不要求象過程匹配那樣有調(diào)用點(diǎn)的進(jìn)入和返回的平衡#65377;

為了使討論簡化，本文所指的程序分析問題都是可達(dá)性問題，即程序中某個(gè)語句是否可達(dá)，這是程序分析中最簡單的問題#65377;

3 利用反射的思想構(gòu)造并發(fā)過程間程序分析的PCP問題實(shí)例 PCP問題是一個(gè)已知的不可判定問題#65377;將需要證明的問

題轉(zhuǎn)化為一個(gè)PCP問題，是一種常用的證明不可判定的方法，同時(shí)，PCP問題能夠?qū)π枰C明的不可判定問題給出一個(gè)直觀的認(rèn)識(shí)#65377;

定義3.1 PCP問題

給定任意兩個(gè)01字符串序列X，Y，X=w1，w2，…，wr，Y=z1，z2，…zr，是否存在一個(gè)大于0的整數(shù)k及一個(gè)序列i1，i2，…，ik，使得wi1wi2…wik=zi1zi2…zik#65377;

例如，考慮r=3的兩個(gè)序列X=0101，101，111，Y=01，011，0111101，這個(gè)PCP問題的實(shí)例^[2]存在一個(gè)解為序列1，2，3，1，即有

w1w2w3w1=0101 101 111 0101 = 01 011 0111101 01=z1z2z3z1#65377;

注意PCP問題的不可判定性與問題的一個(gè)性質(zhì)相關(guān):j≤k， wij的出現(xiàn)次數(shù)等于zij的出現(xiàn)次數(shù)#65377;

[1]的想法是:用X，Y分別表示一個(gè)并發(fā)程序中兩個(gè)并發(fā)任務(wù)的同步序列，X，Y中的每個(gè)字符串表示在不同調(diào)用點(diǎn)上的同步序列，將程序分析問題轉(zhuǎn)化為PCP問題#65377;這種方法的困難在于，如何使得不同任務(wù)的兩個(gè)調(diào)用必須重復(fù)執(zhí)行同樣的次數(shù)，[1]通過在兩個(gè)并發(fā)任務(wù)的每個(gè)調(diào)用點(diǎn)增加一個(gè)特定的同步變量進(jìn)行控制，這樣證明了上下文相關(guān)和同步相關(guān)的程序分析是不可判定的#65377;

但增加同步變量產(chǎn)生了一個(gè)問題，為了控制這些同步變量，我們不得不再增加一個(gè)并發(fā)任務(wù)(上圖中的任務(wù)D)控制這些同步變量，所以[1]文中利用PCP問題的實(shí)例實(shí)際上證明的是:當(dāng)任務(wù)數(shù)>2時(shí)，過程間并發(fā)程序分析是不可判定問題#65377;不需要增加任何輔助的同步變量和并發(fā)任務(wù)的證明關(guān)鍵在于構(gòu)造合適的過程和并發(fā)產(chǎn)生的關(guān)系，直接反映不可判定的來源#65377;

仔細(xì)觀察PCP問題的形式，注意到構(gòu)造一個(gè)PCP問題實(shí)例的關(guān)鍵在于兩點(diǎn)，第一，要求A#65380;B中對(duì)應(yīng)的字符串以完全相同的形式出現(xiàn)，即出現(xiàn)的次數(shù)和順序都完全一致，這種要求非常類似于過程匹配，因此，如果將對(duì)應(yīng)的字符串分別放在過程的調(diào)用點(diǎn)和返回點(diǎn)上(即用一個(gè)過程調(diào)用分割一條路徑的同步序列)，那么程序的執(zhí)行自然滿足這種關(guān)系#65377;第二，要求產(chǎn)生的01字符串相同，這種對(duì)應(yīng)關(guān)系與同步匹配關(guān)系類似#65377;問題在于，如果采用第一方法構(gòu)造PCP問題，則需要對(duì)應(yīng)的同步序列在同一個(gè)任務(wù)內(nèi)#65377;要建立同一個(gè)任務(wù)內(nèi)的同步序列間的同步匹配關(guān)系，必須通過一個(gè)中介達(dá)到#65377;我們?cè)O(shè)想另一個(gè)任務(wù)B是一面鏡子，將需要產(chǎn)生同步關(guān)系的任務(wù)A發(fā)出的X序列反射回任務(wù)A自身，使任務(wù)A的Y序列與這個(gè)反射回來的同步序列匹配，這樣就可以達(dá)到目的#65377;

定理1 對(duì)于過程間并發(fā)程序分析，當(dāng)任務(wù)數(shù)>1時(shí)，即只要有兩個(gè)或兩個(gè)以上的并發(fā)任務(wù)，并發(fā)程序分析就是不可判定問題#65377;

證明:我們同樣將該問題轉(zhuǎn)化為PCP問題，但只需要兩個(gè)任務(wù)，也不需要輔助的同步變量#65377;

在上圖給出的PCP問題的一個(gè)實(shí)例中，任務(wù)A既產(chǎn)生X序列，又產(chǎn)生Y序列，X和Y中對(duì)應(yīng)的01字符串出現(xiàn)的方式顯然是相同的#65377;任務(wù)B的作用是本文證明的關(guān)鍵所在，本來wi和zi之間沒有同步匹配關(guān)系，而任務(wù)B如同一面鏡子，根據(jù)接收的01序列再將這個(gè)01同步序列反射回任務(wù)A，從而導(dǎo)致wi和zi之間產(chǎn)生匹配關(guān)系#65377;任務(wù)B接收任務(wù)A發(fā)送的同步請(qǐng)求(X序列)，并向任務(wù)A發(fā)送與接受到的同步序列相應(yīng)的同步請(qǐng)求序列，而這個(gè)序列在任務(wù)A中是由Y序列接收的，即任務(wù)A的X序列和Y序列必須匹配#65377;這樣任務(wù)A是否能到達(dá)語句u是一個(gè)PCP問題#65377;

4 導(dǎo)致不可判定的因素

構(gòu)造性證明可以提供對(duì)問題的一個(gè)直觀的，深入的認(rèn)識(shí)#65377;我們希望從證明中能對(duì)這樣一個(gè)問題給出啟發(fā)，什么時(shí)候同步相關(guān)會(huì)造成不可判定問題?這對(duì)于實(shí)際的過程間并發(fā)程序分析有重要意義#65377;

引理1 單過程的并發(fā)程序分析是可判定問題#65377;

證明:每個(gè)進(jìn)程同步序列可以表示為一個(gè)正則語言，這個(gè)問題轉(zhuǎn)化為兩個(gè)正規(guī)語言的交集是否為空#65377;

從上一節(jié)給出的不可判定的證明過程，可以得到更有趣的結(jié)果#65377;

在定理1的證明過程中，我們通過任務(wù)B的反射作用，將X序列的同步匹配關(guān)系反射回任務(wù)A的同步序列Y，從而導(dǎo)致X和Y之間產(chǎn)生匹配關(guān)系，任務(wù)B的作用是將任務(wù)間的同步匹配關(guān)系反射到任務(wù)內(nèi)，從而建立了同步與過程的關(guān)系#65377;

但問題并不到此為止，表面上，任務(wù)B是將任務(wù)A發(fā)出的同步匹配關(guān)系反射到任務(wù)A內(nèi)，然而注意到，過程匹配的匹配方式完全不同于同步匹配的匹配方式，任務(wù)A的X序列發(fā)出的同步請(qǐng)求，即使沒有馬上得到Y(jié)序列的接受，任務(wù)A并不會(huì)阻塞，仍然可以繼續(xù)執(zhí)行#65377;任務(wù)A的X和Y之間的匹配模式不是同步匹配模式，而是過程匹配模式#65377;任務(wù)B在調(diào)用點(diǎn)入口接受任務(wù)A的X序列，在調(diào)用返回點(diǎn)將接收的同步請(qǐng)求反射回任務(wù)A的Y序列，實(shí)際上是通過任務(wù)間的同步匹配將其自身的過程匹配關(guān)系“投影”到任務(wù)A，任務(wù)A的X和Y之間的匹配反映的是任務(wù)B的過程匹配關(guān)系，這樣，任務(wù)A內(nèi)有了兩個(gè)可交織的過程匹配，這就是不可判定的來源#65377;同步匹配在這個(gè)不可判定問題中起了一個(gè)傳遞作用，將一個(gè)任務(wù)的過程匹配關(guān)系通過同步匹配關(guān)系“投影”到另一個(gè)并發(fā)的任務(wù)內(nèi)#65377;

上面的分析使我們得到這樣一個(gè)直觀的認(rèn)識(shí):不可判定的表現(xiàn)形式是，在一個(gè)任務(wù)內(nèi)形成兩個(gè)可交織的過程匹配，其中一個(gè)過程匹配是另一個(gè)并發(fā)任務(wù)的過程匹配通過同步匹配的“投影”#65377;

5 結(jié) 論

過程間并發(fā)程序分析是一個(gè)不可判定問題#65377;理解這個(gè)不可判定問題的來源是發(fā)展一個(gè)有效的分析算法的基礎(chǔ)#65377;現(xiàn)有的證明通過構(gòu)造三個(gè)并發(fā)任務(wù)的PCP問題實(shí)例，證明了過程間并發(fā)程序分析過程間并發(fā)程序分析是一個(gè)不可判定問題#65377;本文利用反射的思想構(gòu)造了一個(gè)PCP問題實(shí)例，僅僅用兩個(gè)并發(fā)任務(wù)將該問題轉(zhuǎn)化為PCP問題，證明了在兩個(gè)并發(fā)任務(wù)的情況下，過程間并發(fā)程序分析是一個(gè)不可判定問題#65377;證明的構(gòu)造過程顯示了，發(fā)生在任務(wù)內(nèi)的過程匹配和發(fā)生在任務(wù)間的同步匹配如何產(chǎn)生相互影響:任務(wù)的同步匹配關(guān)系被并發(fā)的其他任務(wù)反射回該任務(wù)本身，從而造成同步匹配與過程匹配的相互影響#65377;進(jìn)一步的，本文指出，同步匹配關(guān)系被反射回自身后，實(shí)際上反映的是對(duì)應(yīng)的并發(fā)任務(wù)的過程匹配關(guān)系，不可判定的表現(xiàn)形式是，在一個(gè)任務(wù)內(nèi)形成兩個(gè)可交織的過程匹配，其中一個(gè)過程匹配是另一個(gè)并發(fā)任務(wù)的過程匹配通過同步匹配的“投影”#65377;我們下一步工作將對(duì)過程間并發(fā)程序分析問題進(jìn)行進(jìn)一步研究，尋求一種有效的分析算法，解決目前過程間并發(fā)程序分析的困難#65377;

注：本文中所涉及到的圖表、注解、公式等內(nèi)容請(qǐng)以PDF格式閱讀原文。