[發明專利]一種基于圖形化衛式命令演算的多任務編譯方法

有效

• 申請號: 201810045360.1
• 申請日: 2018-01-17
• 公開（公告）號: CN108319458B
• 公開（公告）日: 2021-04-06
• 發明（設計）人: 楊志斌;袁勝浩;謝健;劉承威;王飛;薛壘;王永孟
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F8/41
• 分類號: G06F8/41
• 代理公司: 南京瑞弘專利商標事務所(普通合伙) 32249
• 代理人: 楊曉玲

1.一種基于圖形化衛式命令演算的多任務編譯方法，其特征在于：用于將圖形化衛式命令演算語言GCC_graph編譯生成多任務可執行Ada/C代碼，編譯過程包括如下步驟：

1)定義圖形化衛式命令演算GCC_graph語言，包括圖形化規約、文本語法和形式語義；

2)使用函數式程序設計語言CAML描述基于GCC_graph的時鐘演算；

3)使用函數式程序設計語言CAML描述基于GCC_graph的任務劃分，包括劃分前進行的數據依賴分析和依次采用的三種劃分方法，所述三種劃分方法包括基于拓撲排序的任務劃分、優化拓撲排序劃分結果和基于流水線方式的任務劃分方法；

4)使用函數式程序設計語言CAML描述基于劃分結果的虛擬多線程代碼自動生成方法；

5)使用函數式程序設計語言CAML描述虛擬多線程代碼轉換到可執行多任務Ada/C代碼方法；

所述步驟1)中定義圖形化衛式命令演算GCC_graph語言包括：

建立與GCC_graph有關的基本定義：

一個GCC_graph模型是定義在信號變量集合V上的衛式動作集合；

GCC_graph模型的輸入輸出為一組取值序列，記為信號變量或信號；

在每一個邏輯時刻，信號為兩種狀態中之一：處于存在狀態并攜帶一個值value或者處于缺失狀態，缺失狀態記為⊥；信號s中所有處于存在狀態的邏輯時刻集合定義為s對應的抽象時鐘，記為如果兩個信號s1和s2的抽象時鐘相同，則稱s1和s2同步；

a)圖形化規約的基本建模元素定義：

衛式動作的基本結構和對應的圖形化建模元素包括立即動作、延遲動作、約束動作、輸入動作和輸出動作五類，具體如下：

立即動作：接收(m+n)個輸入信號，包含m個輸入信號用于衛式判斷和n個輸入信號用于計算動作，如果衛式G為true，則進行計算f，并返回輸出信號k，否則不執行任何操作；其中，f表達常量、算術運算、邏輯運算以及用戶自定義函數；

延遲動作：接收m個用于衛式判斷和n個用于動作計算的輸入信號，如果衛式G為true，則執行計算f，并延遲一個邏輯時刻輸出結果k，否則不執行任何操作；

約束動作：接收m個用于衛式判斷和n個用于約束的輸入信號，如果衛式為true，則執行同步操作，同步n個輸入信號，并輸出同步結果，否則不執行任何操作；

輸入動作：從外部環境中接收輸入信號，在每個邏輯時刻，在執行每個GCC_graph中計算之前，始終檢查輸入信號；

輸出動作：將信號輸出到外部環境中；在每個邏輯時刻，在每個GCC_graph中的計算完成之后判斷是否輸出信號；

b)GCC_graph文本語法的形式化定義：

GCC_graph的五類基本結構的形式語法和對應語義解釋如下所示：

其中，衛式G是定義在信號變量X、信號變量x的邏輯時鐘及其初始時鐘之上的布爾條件，x∈X；τ是定義在X上的表達式；σ是定義在X及其邏輯時鐘上的布爾表達式；

GCC_graph抽象語法表示為：上述定義中，GCC/x為GCC_graph中的局部信號變量聲明；不同的GCC_graph之間組合采用同步組合操作‘||’；表示G和σ可能有x、f(G,...,G)這四種表達方式，τ表示τ可能有x、f(τ,...,τ)這兩種表達方式；

c)GCC_graph的形式語義：分為兩部分：第一部分為先定義衛式、約束和表達式的時鐘和取值；第二部分為基于蹤跡模型定義GCC_graph的指稱語義；

第一部分，在給定蹤跡S、邏輯時刻i和信號變量X，定義下列函數：

I)的域定義為為真，當且僅當在S上的邏輯時刻i，G中的所有信號變量都處于存在狀態，由于每個時鐘都可以在任意邏輯時刻被讀取，因此被定義為真：

定義一個偏函數當為真，計算γ的取值為真或假：

II)的域定義為為真，當且僅當在S上的邏輯時刻i，τ中的所有信號變量都不缺失：

定義一個偏函數當為真，計算τ的取值真或假：和分別具有I)中和相同的定義；

第二部分，基于蹤跡模型定義GCC_graph的指稱語義：

一個GCC_graph系統的蹤跡語義定義為蹤跡的集合，即，

立即動作：

延遲動作：

約束定義：

輸入動作：

輸出動作：

GCC_graph的組合語義定義為：