AADL的四種經典設計模式
編輯推薦: |
本文來自於個人部落格,本文在AADL基本知識瞭解的基礎上,為了增強建模工具和驗證工具Cheddar之間的互操作性,引入了AADL的四種經典通訊設計模式,我希望對您的學習有所幫助。 |
一、同步資料流(Synchronous data-flows)模式
1.描述
在同步資料流模式中,執行緒在dispatch時讀取輸入埠的資料、在complete時向輸出埠寫資料。此模式不需要共享的data構件,processor構件需要指定固定優先順序排程策略(如Rate Monotonic等)。
2.舉例
例如,三個週期執行緒通過兩個事件埠連線(data port connections)連結在一起,AADL圖形模型如圖1所示,AADL文字表示較簡單,此處省略。
圖1 同步資料流模式
3.分析
這種模式只能用靜態排程策略,每個執行緒總是在固定的時間讀資料、執行、寫資料(即使在不需要的情況下),因此顯得不靈活。但這種模式的分析卻非常簡單,可以進行處理器利用率(processor utilization factor)分析和最壞響應時間(WCRT)分析等。
二、互斥(Mutex)模式
1.描述
互斥模式考慮了非同步通訊的情形,在此模式中,執行緒通過優先順序繼承協議(priority inheritance protocols)非同步訪問共享的data構件。
2.舉例
為了闡釋非同步執行緒間通訊,本文以互斥訊號量Mutex的P/V原語的實現作為案例。AADL模型的圖形表示如圖2。
圖2 互斥通訊模式
AADL模型的文字表示如下:
SUBPROGRAM IMPLEMENTATION P.others
ANNEX Behavior_Specification {**
states
s0: initial state;
s1: return state;
transitions:
busy: s0 -[on me.The_Value=0]->s1{};
free: s0-[on me.The_Value=1]-> s1{ me.The_Value := 0; };
**};
END P.others;
SUBPROGRAM IMPLEMENTATION V.others
ANNEX Behavior_Specification {**
states
s: initial return state;
transitions:
s -[]-> s { me.The_Value := 1; };
**};
END V.others;
THREAD IMPLEMENTATION Thread_A.others
PROPERTIES
Dispatch_Protocol => Periodic;
Period => 10 ms;
ANNEX Behavior_Specification {**
states
s0: initial state;
s1, s2, s3, s4: state;
s5: complete state;
transitions
acquire_M1: s0-[]->s1{P!(Mutex_1);};
acquire_M2: s1-[]->s2{P!(Mutex_2);};
critical_section: s2-[]->s3 {…};
release_M1: s3-[]->s4{V!(Mutex_1);};
release_M2: s4-[]->s5{V!(Mutex_2);};
**};
END Thread_A.others;
THREAD IMPLEMENTATION Thread_B.others
…
ANNEX Behavior_Specification {**
…
transitions
acquire_M2: s0-[]->s1{P!(Mutex_2);};
acquire_M1: s1-[]->s2{P!(Mutex_1);};
…
**};
END Thread_B.others;
3.分析
這種模式可以進行死鎖驗證和WCRT等,但計算WCRT前需要先計算等待時間,這是很重要的。
三、黑板(Blackboard)模式
1.描述
典型作業系統有很多同步設計模式,如訊號量、讀者寫者、生產者消費者等等。對於程式語言也有專用的同步設計模式,如黑板設計模式。黑板設計模式是讀者寫者模式的實現,同一時刻只能有一個writer更新資料,但可以有多個readers讀取資料。
2.舉例
用黑板模式實現讀者寫者的AADL圖形模式如圖3。
圖3 黑板模式
AADL文字模型如下:
DATA T_BlackBoard
FEATURES
Request_Read: SUBPROGRAM Read0.o;
Read: SUBPROGRAM Read1.o;
Release_Read: SUBPROGRAM Read2.o;
Request_Write: SUBPROGRAM Write0.o;
Write: SUBPROGRAM Write1.o;
Release_Write: SUBPROGRAM Write2.o;
END T_BlackBoard;
DATA IMPLEMENTATION T_BlackBoard.o
SUBCOMPONENTS
Contents: DATA T_Item;
Readers: DATA Behavior::Integer;
Is_Idle: DATA Behavior::Boolean;
Is_Reading: DATA Behavior::Boolean;
Is_Writing: DATA Behavior::Boolean;
END T_BlackBoard.o;
SUBPROGRAM IMPLEMENTATION Read0.o
ANNEX Behavior_Specification {**
states
s: initial return state;
transitions
s -[on me.Is_Idle and me.Readers=0 ]-> s {
me.Readers := me.Readers + 1;
me.Is_Reading := true;
me.Is_Idle := false;
};
**};
END Read0.o;
3.分析
這種模式下,在任何時刻只有最後寫入的訊息可用。
四、排隊緩衝(Queued buffer)模式
1.描述
排隊緩衝模式使得在任何時刻,所有的寫入資料都可用(即所有的寫入資料都儲存到記憶體),AADL通過事件資料埠(event data port)或共享data構件實現。假設buffer訊息的處理協議是FIFO。
2.舉例
以生產者-消費者為例闡釋排隊緩衝模式。生產者-消費者的AADL圖形模型如圖4所示。
圖4 排隊緩衝模式
AADL模型的文字表示如下:
DATA IMPLEMENTATION T_Buffer.others
SUBCOMPONENTS
Stack: DATA T_Item;
Current: DATA Behavior::Integer;
Max: DATA Behavior::Integer;
END T_Buffer.others;
SUBPROGRAM Push
FEATURES
me: IN OUT PARAMETER T_Buffer.others;
Item: IN PARAMETER T_Item;
END Push;
SUBPROGRAM IMPLEMENTATION Push.others
ANNEX Behavior_Specification {**
states
s: initial return state;
transitions
s-[on me.Current < me.Max]->s {
me.Stack(me.Current) := Item;
me.Current := me.Current+1;};
**};
END Push.others;
SUBPROGRAM Pop
FEATURES
me: IN OUT PARAMETER T_Buffer.others;
Item: OUT PARAMETER T_Item;
END Pop;
SUBPROGRAM IMPLEMENTATION Pop.others
ANNEX Behavior_Specification {**
states
s: initial return state;
transitions
s-[on me.Current > 1]->s {
Item := me.Stack(me.Current);
me.Current := me.Current-1;};
**};
END Pop.others;
THREAD IMPLEMENTATION Prod.others
PROPERTIES
Dispatch_Protocol => Sporadic;
Period => 10 ms;
ANNEX Behavior_Specification {**
state variables
v: T_Item;
states
s: initial complete state;
transitions
s-[]->s {Push!(Buffer,v);};
**};
END Prod.others;
THREAD IMPLEMENTATION Cons.others
PROPERTIES
Dispatch_Protocol => Periodic;
Period => 20 ms;
ANNEX Behavior_Specification {**
state variables
v: T_Item;
states
s: initial complete state;
transitions
s-[]->s {Pop!(Buffer,v);};
**};
END Cons.others;
3.分析
這種模式需要進行可排程性分析,此外,還需要分析記憶體使用情況,以確保當生產者速率大小消費者速率時不會丟失資料