[發明專利]基于絕對地址匯聚的數據訪問沖突檢測方法

有效

• 申請號: 201310744736.5
• 申請日: 2013-12-30
• 公開（公告）號: CN103699388A
• 公開（公告）日: 2014-04-02
• 發明（設計）人: 王政;綦艷霞;顧斌;董曉剛;陳睿;陳堯;趙雷;郭向英
• 申請（專利權）人: 北京控制工程研究所
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 中國航天科技專利中心 11009
• 代理人: 陳鵬

技術領域

本發明涉及一種針對航天嵌入式C程序中數據競爭檢測的方法。

背景技術

航天嵌入式C程序一般采用任務—中斷的架構。任務由控制周期定時調用。在任務執行過程中，如果出現中斷信號，那么任務被掛起，轉入相應的中斷服務程序。一般來說，航天嵌入式C程序具有多重中斷，這些中斷的優先級不同。低優先級的中斷對應的中斷服務程序執行時，如果出現高優先級的中斷信號，那么當前中斷服務程序被掛起，轉入高優先級的中斷對應的中斷服務程序。

任務和中斷服務程序之間、不同的中斷服務程序之間，都存在共享數據。如果對該共享數據進行寫操作，那么就會發生數據競爭。航天嵌入式C程序一般通過絕對地址訪問的方式與外部設備進行交互。這種方式的特點之一是對一處絕對地址進行寫操作，可能改變從另一處絕對地址讀取到的值。以某種串口設備為例，該串口設備提供兩個可訪問的絕對地址，分別表示數據緩沖區和緩沖區空余字節數。對前者的寫操作，將影響對后者的讀操作的結果。如圖1所示，任務通過循環語句向串口發送數據，直至串口的緩沖區填滿。中斷服務程序則在串口的緩沖區有4個字節或4個字節以上的空余時，向串口發送4個字節的數據。如果中斷信號發生在判斷循環條件和執行循環體之間，且此時*PORT_SIZE的值為4，那么中斷服務程序將向串口寫入4個字節的數據。中斷服務程序結束后，任務恢復，繼續執行循環體。此時，串口的緩沖區已滿，循環體中向串口寫入1個字節的語句將導致串口的緩沖區溢出。由于中斷服務程序和任務對*PORT_SIZE均為讀操作，因此會無法判斷，從而導致數據競爭。

現有的數據訪問沖突檢測方法主要是針對發生在共享變量之間的數據訪問沖突，僅有少數方法能檢測發生在絕對地址上的數據訪問沖突。這些方法往往簡單地將絕對地址視為共享變量的特殊形式，而沒有考慮絕對地址之間的關聯性。

發明內容

本發明的技術解決問題是：克服現有技術的不足，提供了一種基于絕對地址匯聚的數據訪問沖突檢測方法，可以降低C程序中數據競爭檢測的漏報率。

本發明的技術解決方案是：基于絕對地址匯聚的數據訪問沖突檢測方法，步驟如下：

（1）對C源程序進行語法分析，構造源程序中使用的絕對地址集合；利用絕對地址集合，構造間接影響關系；所述的間接影響關系是一組絕對地址上的一一映射關系，具有一一映射關系的兩個絕對地址中，對其中一個絕對地址的寫操作會導致另一個絕對地址的讀操作的結果發生變化；

（2）根據C源程序中的中斷響應函數，尋找C源程序包括的所有中斷上下文；

（3）對于步驟（2）中確定的每個中斷上下文，進行下列檢查：

（31）將C源程序的主程序中進行讀操作的絕對地址構成的集合記作R₁，寫操作構成的集合記作W₁，將C源程序的中斷中進行讀操作的絕對地址構成的集合記作R₂，寫操作構成的集合記作W₂；

（32）令w₁=closure(E,W₁)，w₂=closure(E,W₂)，其中E為步驟（1）中的間接影響關系；w_i=closure(E,W_i)，i=1、2的計算步驟如下：

（321）令w_i=W_i；

（322）對任意的d∈w_i，令w_i'=w_iU{E(d)}；其中E(d)為絕對地址d所處的間接影響關系對應的絕對地址；

（323）如果w_i=w_i'那么w_i=closure(E,W_i)計算完畢，否則令w_i=w_i'，并回到步驟（322）；

（33）令A=(w₁∩w₂)U(w₁∩R₂)U(R₁∩w₂)；如果A=，那么沒有數據訪問沖突；否則判定在集合A中的絕對地址處發生數據訪問沖突。