過程間并發(fā)程序分析不可判定的一個新證明方法

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

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

中圖分類號:TP311.5 文獻標識碼:A

1 引 言

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

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

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

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

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

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

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

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

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

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

定義2.1 過程匹配

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

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

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

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

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

matched→matched (u|balance #65377;

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

定義2.2 同步匹配

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

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

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

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

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

定義3.1 PCP問題

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

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

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

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

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

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

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

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

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

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

4 導致不可判定的因素

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

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

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

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

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

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

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

5 結(jié) 論

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

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