一種基於Java並發程序錯誤的不變式檢測系統的製作方法
2023-04-28 07:54:01 3
專利名稱：一種基於Java並發程序錯誤的不變式檢測系統的製作方法
技術領域：
本發明屬於程序錯誤檢測技術領域，具體涉及一種針對Java並發程序錯誤的檢測系統。
背景技術：
隨著計算機多核技術的發展，Java多線程技術的優勢體現的越來越明顯。多線程技術不僅能夠提高程序的運行效率，還能提高程序的實時響應性，從而提升用戶體驗，目前推出的軟體產品大多以多線程的方式實現。然而，多線程技術在為程序帶來這些優勢的同時，由於其編寫時的複雜性和執行時的不確定性，也給程式設計師帶來了新的挑戰。在程序編寫時，程式設計師需要額外地對各個線程中的工作進行同步管理，保持數據的一致性，否則就可能引發程序並發錯誤，會對軟體的質量造成重大影響，並且這類錯誤較難被檢測和修復。
為了統一地檢測程序中多種類型的並發錯誤，一系列基於不變式的檢測工具被提出。這類工具首先制定相應的不變式規則來代表可能產生並發錯誤的程序行為，然後通過一定數量的訓練運行提取滿足不變式的所有正確程序行為，最後以收集到的信息指導檢測運行時的並發錯誤檢查。不變式檢測方法作為目前最為有效的並發錯誤檢測手段，以提取正確程序行為的方式自動識別程序並發錯誤，較之傳統的分析方法在精度和效率上都有一定的優勢。但現有的不變式檢測工具主要為C/C++語言設計，未考慮Java的程序特性。傳統的不變式檢測工具以上下文不敏感的信息來區分不同程序點，該信息一般為靜態指令(例如，方法名和文件行號的組合)。但是由於Java中大量的包裝函數，程序中大量的訪存操作被封裝在包裝函數中，其中最為典型的就是程序中的getter和setter函數了。如果繼續沿用靜態指令來區分程序點，調用相同包裝函數的不同訪存操作都被認為是同一程序點，這樣可能會誤導檢測工具最終檢測結果的正確性。以一個極端的情況為例，私有欄位只能通過getter來讀取，通過setter來修改，那麼傳統的工具會認為所有調用這兩個函數的程序點都是相同的，這樣顯然是不精確的。如圖I所示，兩端程序是相同含義的C++和Java的程序片段，且S2語句應該在S3語句執行完後被執行，否則會造成錯誤。對於C++程序，使用訪存操作的靜態語句能分析出S36S2是正確依賴，而S16S2則是錯誤依賴，這樣在檢測運行時就能檢測出這一錯誤。但是Java程序中由於封裝函數的存在，訪存操作都被包含在封裝函數中，無論是正確依賴還是錯誤依賴都是S46S5，由於無法區分正確和錯誤依賴，所以這一併發錯誤就無法被檢測出來。簡單地說，上下文不敏感的信息不足以區分Java程序中的訪存程序點，使用靜態語句表示程序點不能滿足Java程序檢測的要求，而上下文敏感的技術則為Java程序的不變式檢測帶來了新的機會。
發明內容
為了解決上述提到的Java程序中的封裝函數導致傳統工具無法有效區分程序點的問題，本發明提供一種基於Java並發程序錯誤的不變式檢測系統。
本發明在動態運行時對程序的上下文信息進行記錄，並為每個帶有上下文信息的程序點收集和檢測程序並發錯誤，以此消除因封裝函數所帶來的程序點無法區分的影響。本發明提供了一種基於Java並發程序錯誤的不變式檢測系統，包括預處理模塊、不變式訓練模塊、不變式文件分析模塊，不變式檢測模塊，錯誤排序刪減模塊以及上下文收集傳遞模塊六大模塊；所述上下文收集傳遞模塊與所述不變式訓練模塊以及所述不變式檢測模塊同時運行，在動態運行時所述上下文收集傳遞模塊將當前的上下文信息進行轉換，傳遞給所述不變式訓練模塊或所述不變式檢測模塊；所述不變式訓練模塊或不變式檢測模塊使用接收到的上下文信息連同靜態語句來表示一個唯一的程序點。其中
I.預處理模塊，負責檢測和過濾程序中不會引起並發錯誤的對象。這樣的對象有兩類，分別是局部對象和單賦值對象。本發明通過靜態分析找出這些對象，並在字節碼中添加標籤進行標示。在訓練和檢測運行階段，本發明識別這些標籤，並忽略對有標籤對象的檢查和記錄，從而降低檢測所帶來的開銷。
2.不變式訓練模塊，使用多次訓練運行，基於對象粒度提取程序中的不變式信息，並將收集的不變式集合以文件形式進行保存，每次正確運行產生一個不變式記錄文件。3.文件分析模塊，負責把所有記錄文件中的信息按照不變式規則進行歸併，最終合成一個文件。4.不變式檢測模塊，利用合成文件指導檢測運行。當檢測運行中的程序行為與記錄中的對象不變式信息出現矛盾時，說明可能存在並發錯誤，需要進一步分析。5.錯誤排序刪減模塊，負責對檢測模塊檢測到的程序錯誤做可信性分析。該模塊使用啟發式算法，為所有檢測到的錯誤計算相應的可信值。刪除可信值較低的錯誤，其他篩選得到的錯誤經過排序後反饋給程式設計師。6.上下文收集傳遞模塊，用於在動態運行時以一定的方式記錄和傳遞當前的上下文信息。上下文收集傳遞模塊與不變式訓練模塊以及不變式檢測模塊同時運行，在動態運行時上下文收集傳遞模塊將當前的上下文信息進行轉換，傳遞給不變式訓練模塊或不變式檢測模塊；
不變式訓練模塊或不變式檢測模塊使用接收到的上下文信息連同靜態語句來表示一個唯一的程序點；
上下文收集傳遞模塊與在訓練和檢測運行中同一程序點上的上下文信息保持一致。本發明中，上下文收集傳遞模塊記錄和傳遞當前的上下文信息時可採用PCC模式，即利用程序當前行號和當前調用棧的信息連續地使用哈希函數進行計算，通過計算出的值來表示當前程序點的上下文內容，用公式表達為
p = f{p, c) = (3/3 十 c) mod 264 ⑴
其中p*表示被調用函數中某個程序位置的上下文哈希值的數值，P表示調用函數的上下文哈希值，c表示在當前函數中的位置信息。PCC模式具體計算過程是通過從上至下的方式展開的，即表示上下文的哈希值P會從調用函數向被調用函數傳遞並進行相應的計算。PCC模式中的計算起點函數包括1)程序的main函數；2)程序中所有繼承了java. lang. Thread類和java. lang. Runnable類中所聲明的run函數。這些起點函數都是程序中所有線程的入口 ；具體實現中為了使不同運行中相同下上文環境具有相同的PCC值，PCC模式下把所有起點函數的PCC值初始化為O。本發明中，PCC方法能簡單地通過比較PCC值，達到區分程序中的上下文環境的目的，不對程序的運行帶來過大的性能影響；並且在不同的運行中，相同的上下文環境能匹配相同的PCC值。本發明中，上下文收集傳遞模塊記錄和傳遞當前的上下文信息時還可採用PaCC方法，其也以計算哈希值的方式來表示當前程序調用棧的信息。其記錄從調用棧底向上到真正調用封裝函數的位置。PaCC模式下計算的程序點哈希值依賴於當前上下文窗口中siz印個程序點的信息，包括它們的文件名字符串哈希值(C)，文件行號(h)。哈希值由上下文窗口由下至上計算,計算sizep次,其計算公式為
權利要求
1.一種基於Java並發程序錯誤的不變式檢測系統，包括預處理模塊、不變式訓練模塊、不變式文件分析模塊，不變式檢測模塊，錯誤排序刪減模塊，其特徵在於還包括上下文收集傳遞模塊；所述上下文收集傳遞模塊與所述不變式訓練模塊以及所述不變式檢測模塊同時運行，在動態運行時所述上下文收集傳遞模塊將當前的上下文信息進行轉換，傳遞給所述不變式訓練模塊或所述不變式檢測模塊；所述不變式訓練模塊或不變式檢測模塊使用接收到的上下文信息連同靜態語句來表示一個唯一的程序點。
2.根據權利要求I所述的不變式檢測系統，其特徵在於所述上下文收集傳遞模塊記錄和傳遞當前的上下文信息時採用PCC模式，即利用程序當前行號和當前調用棧的信息連續地使用哈希函數進行計算，通過計算出的值來表示當前程序點的上下文內容，用公式表達為 P = i{Pf c) = (3p + c) mod 204 ⑴ 其中P*表示被調用函數中某個程序位置的上下文哈希值的數值，P表示調用函數的上下文哈希值，c表示在當前函數中的位置信息； 所述PCC模式具體計算過程是通過從上至下的方式展開的，即表示上下文的哈希值P會從調用函數向被調用函數傳遞並進行相應的計算； 所述PCC模式中的計算起點函數包括1)程序的main函數，2)程序中所有繼承了java. lang. Thread 類和 java. lang. Runnable 類中所聲明的 run 函數； 所述PCC模式下，所有起點函數的PCC值初始化為O。
3.根據權利要求I所述的不變式檢測系統，其特徵在於所述上下文收集傳遞模塊記錄和傳遞當前的上下文信息時採用PaCC模式，其用計算哈希值的方式來表示當前程序調用棧的信息，其記錄從調用棧底向上到真正調用封裝函數的位置，PaCC模式下計算的程序點哈希值由上下文窗口由下至上計算，計算sizep次,其計算公式為 Pg =c, Ii) = (13ρa + Sc + h) mod 2 ^⑵ 其中Pa*表示被調用函數中某個程序位置的上下文哈希值的數值，Pa表示調用函數的上下文哈希值，c表示文件名字符串哈希值，h表示文件行號； 其中所述sizep表示上下文窗口的大小,其大於或等於當前封裝方法的棧深度depthw加1，即 sizep >= depthw+I (3) 。
4.根據權利要求3所述的不變式檢測系統，其特徵在於所述上下文窗口的大小sizep為4。
全文摘要
本發明屬於程序錯誤檢測技術領域，具體為一種基於Java並發程序錯誤的不變式檢測系統。其包括預處理模塊、不變式訓練模塊、不變式文件分析模塊，不變式檢測模塊，錯誤排序刪減模塊及上下文收集傳遞模塊六大模塊；本發明在在動態運行時以PaCC及PCC模式對程序的上下文信息進行記錄，解決了Java程序中的封裝函數導致傳統工具無法有效區分程序點的問題。
文檔編號G06F11/36GK102799527SQ201210236250
公開日2012年11月28日 申請日期2012年7月10日 優先權日2012年7月10日
發明者楊珉, 王笛 申請人:復旦大學