[發明專利]時間多棧下推網絡的靜態轉換方法

有效

• 申請號: 201510581206.2
• 申請日: 2015-09-14
• 公開（公告）號: CN105260295B
• 公開（公告）日: 2018-09-25
• 發明（設計）人: 錢俊彥;甘鵬程;郭云川;趙嶺忠;古天龍
• 申請（專利權）人: 桂林電子科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F21/57
• 代理公司: 桂林市持衡專利商標事務所有限公司 45107
• 代理人: 陳躍琳

1.一種時間多棧下推網絡的靜態轉換方法，其特征是，包括如下步驟：

步驟(1)將含有時間行為的并發遞歸程序轉換為一個等價的可模擬程序執行的時間多棧下推網絡，該時間多棧下推網絡的執行對應于程序包含的所有動作或行為；

步驟(1.1)構造實時并發遞歸程序的抽象模型即時間多棧下推網絡；

所構造的時間多棧下推網絡是一個六元組M_T＝(n,Q,q₀,Γ,T,Δ)，其中M_T表示時間多棧下推網絡，n表示系統中棧的個數；Q表示有限狀態集；q₀表示初始狀態；Γ表示有限棧符集；T＝T_G∪T_L表示有限時鐘集，其中T_G表示全局時鐘，用于標識實時并發系統中全局變量或事務的時間，T_L表示棧內局部時鐘，用于標識系統中局部變量或子事務的時間；遷移關系為描述系統格局的遷移；

所構造的時間多棧下推網絡的格局C＝<Work[n],q,{w_i}_i∈[n],v>，其中q∈Q，為[n]子集，表示當前工作棧集，w_i為棧i的字，表示棧i的內容，描述為v表示時鐘當前取值；

步驟(1.2)將所構造的時間多棧下推網絡用操作語義進行描述；其中時間多棧下推網絡作為實時并發程序的模型，用于描述多個棧同時產生遷移，其遷移關系Δ分為棧內遷移Δⁱⁿ、棧間切換Δ^inter和并發執行Δ^||；

步驟(1.2.1)對于一個棧i內遷移的執行，用形式表示，其中q和q′均表示狀態，w_i和w_i′均表示棧i的字，v和v′均表示時鐘當前取值，a表示變量，op_in為棧內遷移時的動作集，包括空操作nop、時間約束判斷t∈I？、時鐘重置t←I、時間流逝Time←c、壓棧操作push(a,I)和出棧操作pop(a,I)，其中I表示時鐘取值范圍，t∈T，Time為具體時間值；故棧內遷移關系Δⁱⁿ表示為Δ^nop∪Δ^？∪Δ^＝∪Δ^├∪Δ^push∪Δ^pop，其中Δ^nop、Δ^？、Δ^＝、Δ^├、Δ^push和Δ^pop分別表示上述操作的遷移；根據不同的棧內遷移動作op_in給出其執行含義如下：

1)Δⁱⁿ＝Δ^nop:op_in＝nop，w_i′＝w_i，v′＝v；表示格局內元素未發生變化；

2)Δⁱⁿ＝Δ^？:op_in＝t∈I？，w_i′＝w_i，v′＝v，v(t)∈I；表示當t的時鐘值在I范圍內時，執行該操作，格局內元素未發生變化；

3)Δⁱⁿ＝Δ^＝:op_in＝t←I，w_i′＝w_i，v′＝v[t←c]，c∈I；表示給時鐘t指定I范圍內的任意值c，其它格局內元素未發生變化；v(t)表示時鐘值；

4)Δⁱⁿ＝Δ^├:op_in＝Time←c，w_i′＝w_i^+c，假設w_i＝<a₁,v₁><a₂,v₂>…<a_n,v_n>，那么w_i^+c＝<a₁,v₁+c><a₂,v₂+c>…<a_n,v_n+c>，v′＝v+c；表示格局內所有時鐘增加c，格局內非時鐘內容未發生變化；w_i^+c表示w_i的時鐘增加c，a₁，a₂，…，a_n表示變量，v₁，v₂，…，v_n表示對應于變量a₁，a₂，…，a_n的當前時鐘取值；5)Δⁱⁿ＝Δ^push:op_in＝push(a,I)，w_i′＝w_i·<a,c>，c∈I，v′＝v；表示將變量a壓入棧頂，并設定相應時鐘為t，其時鐘值為I范圍內的任意值；

6)Δⁱⁿ＝Δ^pop:op_in＝pop(a,I)，w_i＝w_i′·＜a,c＞，c∈I，v′＝v；表示將棧頂內時鐘值為I范圍的變量a彈出；

步驟(1.2.2)描述棧間切換Δ^inter；假設棧間切換操作表示棧i切換到棧j，用形式表示，其中q,q′∈Q；v′＝v；w_i，w_j分別為棧i,j的字，i,j∈[n]且i≠j；上下文切換時，將棧j從等待棧切換到工作棧，同時將棧i從工作棧切換到等待棧，則切換后的工作棧Work[n]′＝Work[n]\{i}∪{j}；

步驟(1.2.3)描述并發操作Δ^||；假設op＝op_in∪op_inter為棧遷移動作集，并發執行用形式表示，Work[n]為當前工作棧集，如果不發生棧間切換，則Work[n]′＝Work[n]，如果發生棧間切換則Work[n]′＝Work[n]\{i}∪{j}；

步驟(2)將步驟(1)所給定的一個時間多棧下推網絡M_T＝([n],Q,q₀,Γ,T,Δ)，通過下述靜態轉換過程獲得多棧下推網絡M_M＝([n]^M,Q^M,q₀^M,Γ^M,Δ^M)；

1)棧個數[n]^M的轉換：[n]^M＝[n]，即M_M的棧數量與M_T的棧數量相等；

2)狀態Q^M的轉換：Q^M＝Q，即M_T的狀態集與M_M的狀態集相同；

3)初始狀態q₀^M的轉換：q₀^M＝q₀，即M_M的初始狀態與M_T的初始狀態相同；

4)棧字符Γ^M的轉換：Γ^M＝2^Z×key，其中Z為普通項集Y，即Z:＝Y，key為時鐘關鍵點集；

5)遷移關系Δ到Δ^M的轉換規則：

M_T的格局遷移為為棧i的字，設d_i為棧i的棧深度，用w_ij表示棧i內第j層的子字，j∈[d_i]，w_ij|_Γ表示w_ij投影在Γ的棧字符，v(w_ij|_Γ)表示投影與棧字符Γ相關聯的時鐘值，表示投影與棧字符Γ相關聯的時鐘值在時鐘域等價后的關鍵點，T_G為全局時鐘，表示全局時鐘的時鐘值在時鐘域等價后的關鍵點，棧i內容其中i∈[n],j∈[d_i]，下面具體描述不同op的構造：

5.1)Δ＝Δ^nop時，op＝nop，如果那么在M_M中有與之對應，即兩者nop操作相同；

5.2)Δ＝Δ^？時，op＝t∈I？，在M_M中有遷移關系Δ^M？與Δ^？相對應，此時M_M的格局遷移為其中{R_i}_i∈[n]表示M_M域R中任意個子域，遷移關系Δ^M？表示在{R_i}上進行判斷操作；

5.3)Δ＝Δ^＝時，op＝t←I，在M_M中有遷移關系Δ^M＝與Δ^＝相對應，此時M_M的格局遷移為其中遷移關系Δ^M＝表示在對{R_i}進行賦值操作，v(t)∈I為M_T賦值時鐘值，為賦值時鐘值在時間域等價后的關鍵點，t∈Z為項內字符，表示將關鍵點賦值給字符t；

5.4)Δ＝Δ^├時，op＝Time←c，在M_M中有遷移關系Δ^M├與Δ^├相對應，此時M_M的格局遷移為其中遷移關系Δ^M├表示在對{R_i}中所有字符的時鐘值增加c后取關鍵點，對任意i∈[n]，棧i內容R′_i＝R′_i1…R′_ij…R′_id,v(w_ij|_Γ)+c表示投影出的棧字符Γ的時鐘值增加c，v(T_G)+c表示全局時鐘的時鐘值增加c；

5.5)Δ＝Δ^pop時，op＝pop(a,I)，在M_M中有遷移關系Δ^Mpop與Δ^pop相對應，此時M_M的格局遷移為其中遷移關系Δ^Mpop表示關鍵點等于的字符a∈Γ出棧，R′_i＝R′_i1…R′_ij…R′_id，((w_ij|_Γ)-a)表示在投影出的棧字符Γ內刪除字符a；

5.6)Δ＝Δ^push時，op＝push(a,I)，在M_M中有遷移關系Δ^Mpush與Δ^push相對應，此時M_M的格局遷移為其中遷移關系Δ^Mpop表示關鍵點等于的字符a∈(Γ∪T)入棧，R′_i＝R′_i1…R′_ij…R′_id，((w_ij|_Γ)+a)表示在投影出的棧字符Γ內增加字符a，(T_G+a)表示在全局時鐘內增加字符a；

5.7)Δ＝Δ^inter時，在M_M中有遷移關系Δ^Minter與Δ^inter相對應，此時M_M的格局遷移為其中{R_i}，{R_j}分別為棧i，j的域，i,j∈[n]且i≠j；上下文切換時，將棧j從等待棧切換到工作棧，同時將棧i從工作棧切換到等待棧；

5.8)Δ＝Δ^||時，在M_M中有遷移關系Δ^M||與Δ^||相對應，此時M_M的格局遷移為工作棧集Work[n]內的每個棧，調用相應的棧內遷移轉換，轉換后格局為＜Work[n]′,q′,{R_j}_j∈[n]＞。