基于離散控制器合成的異構多核系統資源管理方法

安 鑫，夏近偉，楊海嬌，歐陽一鳴，任福繼

（1.合肥工業大學計算機與信息學院，合肥 230601；2.情感計算與先進智能機器安徽省重點實驗室（合肥工業大學），合肥 230601）

（?通信作者電子郵箱xin.an@hfut.edu.cn）

0 引言

異構多核處理器（Heterogeneous Multi-Core Processor，HMP）現今已被廣泛應用于嵌入式系統以及云計算等多種領域。這種處理器除了具有傳統同構多核處理器的并行性特征以外，還可以根據應用的不同類型和需求選擇使用最合適的處理核，從而進一步優化系統對高性能和低功耗的需求。此外，當今的異構多核處理器通常配備了動態電壓和頻率調整（Dynamic Voltage and Frequency Scaling，DVFS）技術，這是由于現代處理器的功耗與處理核的頻率及其執行的任務的行為密切相關［1］，允許系統根據其運行狀態（如負載情況）來動態調整處理器平臺的電壓和/或頻率可以進一步在提高性能和降低功耗之間進行權衡。ARM（Advanced RISC Machines）處理器的big.LITTLE 架構就是這樣一種典型的異構多核系統，可以將不同類型的處理核組織為不同的簇，并以處理核簇為單位進行DVFS控制［2］。

現在典型的異構多核系統往往需要在并行運行多個應用的同時滿足每個應用的性能和服務質量等方面的需求。而一些復雜應用還可以以多線程的方式被執行，從而可以被映射到多個不同的處理核上并行運行以達到提高性能、降低單個處理器核功耗過大等目的。

因此，要充分發揮異構多核系統在提高性能和降低功耗等方面的潛能，需要解決的很重要的一個問題就是異構多核系統的資源管理問題，也就是如何根據系統運行狀態動態地為應用分配執行資源從而滿足系統性能、功耗等方面的需求［3-4］。然而隨著異構多核系統中資源數目和種類的不斷增加，其資源管理部件的設計也變得越來越復雜。設計人員往往面臨著一個（非常）大的選擇空間（例如應用劃分的線程數、使用的處理核類型和數量等），為了提高效率，現有的在線資源管理方法大部分采用啟發式的方法來對選擇空間進行評估和搜索［5-9］。然而這些方法對所設計的系統資源管理部件均缺少可靠性的支持，對于那些對可靠性要求比較高的場景，這類方法往往不被采用。鑒于此，一些形式化的方法和技術（比如模型檢測）被提出［10-11］，然而形式化的方法雖然可以確保可靠性，卻往往需要經歷一個對設計方案進行手動建模和編碼，當出錯時定位錯誤再進行修正直至不再出錯為止的一個迭代過程。隨著問題規模的變大，相對于這類方法，能夠自動化進行設計方案生成的方法無疑更加可取。

本文提出了一種基于離散控制器合成（Discrete Controller Synthesis，DCS）技術的通用模型和方法來解決異構多核系統的在線資源管理問題，該方法將離線分析和在線資源分配結合，通過有限狀態自動機（Finite State Automaton，FSA）模型對系統進行建模描述，并使用離散控制器合成（DCS）技術自動生成無需形式化驗證的控制部件代碼。相比文中提及的其他基于形式化的資源管理方法，該方法的特點是可以使設計者僅需通過描述系統行為模型及其需要滿足的控制目標便可以使用現有的合成工具和算法來進行自動的設計空間探索從而合成一個正確可靠的、滿足系統控制目標的控制部件。

本文的主要工作有以下兩點：

1）將異構多核系統的資源管理問題分解為硬件執行平臺行為、應用資源分配行為和資源管理策略/目標三部分，并將其建模為一個可以根據管理目標對應用的資源分配和執行平臺的DVFS等級進行管理控制的離散控制問題。

2）采用現有的離散控制器合成技術和工具對示例異構多核系統的資源管理部件進行了自動、可靠的生成和模擬驗證，并對所采用技術的可擴展性進行了評估。

1 相關工作

目前大多數涉及多核系統資源管理的研究都是針對應用任務在多核系統上的動態調度問題。由于需要在線進行調度，這些方法大部分采用啟發式的方法來產生一個快速、高效的解決方案［4-9，12］。然而這些方法大都針對事先未知的情況或狀態，通常只是通過模擬驗證來評估方案的一般性能，而無法確保解決方案達到最優或者嚴格滿足可靠性需求。

近些年來，基于機器學習技術進行性能預測和動態調度的方法引起了越來越多的關注并取得了良好效果。這類工作主要可以分為兩類：一類是使用機器學習技術預測不同調度方案的性能或功耗［13-16］，然后在此基礎上再結合某種搜索策略選來擇調度方案；另一類則是針對調度目標和系統狀態對調度方案進行學習來獲得調度模型用于預測符合條件的調度方案［17-20］。然而，基于機器學習的方法同樣面臨著無法提供嚴格的可靠性保證的問題，往往通過模擬以一定概率來確保目標達成。

相對于以上兩類基于模擬來進行設計可靠性驗證的方法，用基于形式化的方法（比如模型檢測）來解決多核系統的資源調度或分配問題顯然更有吸引力，特別是針對那些對可靠性要求比較高的場景。在文獻［10］中，作者提出了一種基于遺傳算法改進的靜態任務映射算法來解決云環境下靜態任務調度問題。為了驗證其設計的可靠性，作者通過建立形式化標簽傳遞系統（Labeled Transition System，LTS）模型，并采用模型檢查工具NuSMV 和PAT 進行了驗證。文獻［11］采用了具有時間拓展的狀態機對周期性的實時任務進行系統建模，然后采用模型檢測方法對硬實時系統的調度可行性進行了分析。這類方法為了采用基于模型檢測的方法來對設計進行驗證，往往需要在已經實現算法編碼的基礎上對設計方案進行手動建模并形式化驗證，當出錯時進行錯誤定位并再進行修正直至不再出現未知的迭代過程，這個過程往往是枯燥費時的。并且隨著問題規模的變大，其工作量將更加艱巨。

與本文更接近的是采用控制理論及其方法和技術來設計系統資源控制器部件的一些工作。在這類方法中，設計者能夠以系統化的方式對已知的知識和預期進行量化，從而產生一個符合設計目標的控制器。這方面的工作可以根據控制系統特征分為兩類：一類是在結構上采用單輸入單輸出（Single-Input Single-Output，SISO）控制系統［21-24］，并在系統內部采用某種控制技術（如PID（Proportion-Integral-Derivative）控制）來實現對某一個系統參數的控制；另一類則是在SISO 控制系統的基礎上考慮多控制目標的協同，使用多輸入多輸出（Multiple-Input Multiple-Output，MIMO）系統［25］。文獻［26］總結和比較了當前主流的多核系統資源管理方法，并提出了一種將啟發式算法和監督控制理論相結合的多核系統資源管理框架。

相比以上的動態資源管理方法，使用離散控制器合成技術的自動化設計方法無疑更加合適，特別是針對高可靠性要求的場景。該方法的主要優勢在于：1）提供了形式化的可靠性保證；2）提出的控制器可以在設計時由DCS工具自動生成，用戶無需關注和理解控制理論細節。據調研所知，目前還沒有使用離散控制器合成技術來自動生成用于異構多核系統的可靠資源管理部件的相關工作。在文獻［27］的工作中已經成功地使用基于DCS 的方法來處理現場可編程門陣列（Field-Programmable Gate Array，FPGA）系統上的可重配置資源的管理問題，本文針對異構多核處理器平臺，并將平臺的DVFS 特性及其管理作為一個設計因素。

2 建模方法和離散控制器合成技術

本文采用離散控制器合成技術（DCS）來解決異構多核系統的資源管理問題，在介紹DCS之前，本部分首先介紹對問題進行形式化描述的有限狀態自動機（FSA）模型。

2.1 有限狀態自動機

本文采用文獻［28-29］中定義的自動機來對系統進行建模。

定義1一個有限狀態自動機可以描述為一個元組：

其中：Q是一個有限的狀態集；q0∈Q是S的初始狀態；I是一個有限的輸入事件集；O是一個有限的輸出事件集；T是一個變遷關系集合，它是Q×Bool(I) ×O*×Q的子集，其中Bool(I)是I的布爾表達式集合，O*是O的冪集。

將兩個并行的自動機進行組合的操作稱之為同步合成（synchronous composition），由“‖”表示。給定兩個自動機：，i=1，2，Q1∩Q2=?。它們的合成定義如下：

式中：

合成狀態(q1，q2)被稱為宏狀態，其中q1和q2是其兩個分狀態。

封裝操作［28］用于對組合到一起的兩個自動機進行同步，它通過一個定義到兩個自動機上的同步變量來達到這個目的，并且這個同步變量需要在其中一個狀態機中作為輸入，而在另一個自動機作為輸出。設為一個自動機，Γ?I∪O為S的輸入和輸出變量的集合，那么Γ對于S的封裝就可以定義為：

式中T'定義為：

其中：g+是單項式g中作為正元素出現的變量集，即g+={x∈g|(x∧g)=g}；g-是在單項式g中以負數形式出現的一組變量，即g-={x∈g|?(x∧g)=g}。圖1 給出了一個使用變量b封裝來使兩個自動機A和B強制同步的例子。

此外，還可以在自動機的狀態上定義權重來表示與狀態相關的數值信息。為此，可以通過定義一個代價函數C：Q→N+將自動機的每個狀態映射到一個正整數。在此基礎上，可以進一步為自動機的路徑定義權重，例如，路徑p的權重可以定義為其所經過的所有狀態的權重總和。當合成自動機時，全局狀態或者路徑的權重值則可以被定義為構成全局狀態或路徑的所有局部狀態權值的和或最大/最小值。

圖1 使用封裝同步兩個自動機的例子Fig.1 An example of synchronization of two automata by encapsulation

給定一個使用以上自動機模型所描述的系統后，就可以應用一些形式化的分析和驗證技術，下面介紹本文所采用的離散控制器合成技術。

2.2 離散控制器合成

離散控制器合成（DCS）［30］于20 世紀80 年代被提出，用于解決離散事件系統的控制與協同問題。離散事件系統（Discrete Event System，DES）［31］是一個由離散狀態構成、事件驅動的動態系統，這些離散事件發生的時機可以是隨機的、沒有固定的時間間隔。例如，事件可能是系統中某個應用的調用或完成，亦或者是處理器發生的某個故障。這類系統出現在我們日常生活的各個領域，如制造業、運輸、汽車、嵌入式系統和醫療保健等。這些系統都有自己的設計需求，并需要在運行中進行相應的管理和控制來確保系統能夠正確可靠地運行。

DCS 理論的主要優點是將目標離散事件系統（DES）與反饋控制分離開來，并允許針對給定的特定控制目標對目標系統進行自動化的、可靠的分析和控制。DCS 是一種可以應用于離散事件系統（比如通過2.1 節的自動機等模型進行描述的系統）的操作。為了能夠對目標離散事件系統（DES）進行控制，也就是控制DES系統運行行為的演化或變化，需要為這類系統定義可控制的事件。因此，DES 的事件集合Y可以被劃分為兩個子集：Yuc和Yc，分別表示不可控制的事件集和可控制的事件集。圖2 展示了DCS 的工作原理，DCS 的使用需要結合一個給定的控制目標：也就是由控制器去遵循實施、從而讓被控系統滿足的目標，控制目標一般通過系統的輸出（狀態）X表示。給定系統模型S 和控制目標后，控制器C 就可以通過相應的綜合算法自動得到。控制器綜合算法的基本原理與模型檢測技術類似，它通過遍歷系統的狀態空間來自動計算對可控變量Yc的約束（即控制器，可以看作是輸出X和不可控輸入Yuc的函數），從而控制系統的狀態轉移使其總是滿足給定控制目標。

當然，可能存在有多個控制器均可以使系統滿足同樣控制目標的情況。在極端情況下，控制器可以禁止任何狀態轉換從而避免系統進入不合法的狀態，但這顯然是不可取的。用戶往往對最大允許的控制器感興趣，也就是能夠保留原始不受控制系統中的最大可能正確行為集的控制器，本文所采用的合成算法和工具就是基于這個原則。總體而言，DCS 的優勢體現在：可以進行高層的控制策略描述和聲明，自動可靠地合成滿足控制目標的控制器，以及在所有可能正確行為中進行最優化。相對于其他形式的驗證技術（如模型檢測），DCS 面臨同樣的可擴展性問題。然而，DCS 更有建設性，也就是能夠自動產生一個正確的解決方案，而不需要像模型檢測一樣需要一個可能易錯的手工編碼階段，然后再進行冗長的驗證［32］。

圖2 離散控制器合成的工作原理Fig.2 Principle of discrete controller synthesis

本文主要使用兩類不同合成算法相對應的DCS操作來合成控制器［33］：一類是確保系統始終處于狀態空間中的一個子集中（即始終處于安全狀態中）；另一類是控制系統根據系統狀態所關聯的開銷進行單步最優的演化，也就是讓系統在進行狀態轉換時選擇可達系統中相應開銷最小或最大的那個狀態。這兩類操作已在DCS工具BZR［31］和ReaX［33］中實現，它們可以使用2.1 節介紹的自動機形式來描述系統行為，并使用一個專用的結構（稱之為合約contract）來描述系統所要滿足的控制目標，最后BZR的編譯過程就可以自動調用ReaX工具中的算法來合成一個正確的控制器（以C 或者Java 源代碼的形式從而可以方便地在實際系統中部署使用）。

3 基于DCS的異構多核系統資源管理方法

首先通過一個示例系統描述了本文所針對的異構多核系統的資源管理問題，然后介紹如何通過第2 章介紹的自動機和DCS 技術來將該問題建模為一個DCS 問題，最后介紹了如何使用現有的DCS工具BZR來對該模型進行代碼描述。

3.1 問題描述

本文從硬件執行平臺、系統應用及其資源分配、資源分配目標三個方面描述所針對的異構多核系統的資源管理問題。

3.1.1 硬件執行平臺

考慮一個由若干個簇構成的異構多核平臺，每個簇由若干個（架構）相同的處理核構成。圖3 給出了一個這樣一個例子，它包含兩個處理核簇（大核簇和小核簇）和一個共享存儲器MEM，每個簇包含兩個相應的大或者小處理核，每個處理核具有獨立的L1 緩存以及簇內共享的L2 緩存。考慮到節約能耗，每個簇在不用的時候都可以設置為睡眠模式，并且每個簇上的處理核在使用時均具有統一調節簇內的電壓和頻率（DVFS）等級的能力來達到降低功耗或者提升執行性能的目的。

另外，本文假設系統平臺是電池供電的，對于這類系統，用戶往往希望系統能夠根據電池電量狀態的變化來調整所運行應用的模式和服務質量。

3.1.2 系統應用及其資源分配

典型的異構多核系統往往需要在多核系統平臺上同時運行多個應用，并同時滿足每個應用的性能等方面的需求。而這些應用往往又是多線程的，從而具有充分利用多個處理核來提高其性能的潛力。另外需要指出的是，為了確保應用執行的可預測性和系統穩定，同大部分異構多核系統的資源管理和調度研究［13，34］一樣，本文約定每個處理核在同一時刻只能執行一個線程。

圖3 平臺架構Fig.3 Architecture of platform

在本文的研究方案中，假定每個應用的執行過程中有如下的控制點（事件）。

1）被請求：應用請求被執行。

2）被執行：應用被調度到執行資源上開始執行。

3）執行結束：應用執行完畢后發出結束通知。

在這些控制事件中的請求和結束事件的發生時機是不可控的，而當應用被執行時選擇使用什么的執行資源則是由系統資源管理部件依據系統的管理策略或者目標來確定的。

當某個應用被啟動時，其執行可以有多種不同的資源分配方案，而不同的資源分配方案所導致的應用性能和功耗也不一樣。圖4 展示了將一個來自PARSEC benchmark 的Blackscholes 應用映射到一個包含兩種類型的處理核（大核B和小核L）的異構多核架構的運行情況［34］。圖4 中，橫軸給出了不同的資源分配情況，橫坐標中的組數（1，2，…，8）為所分配處理核資源總數目，即B和L的和。

圖4 不同資源分配情況下的性能和能耗值Fig.4 Performance and power consumption under different resource distributions

3.1.3 資源分配目標

資源分配目標定義了進行資源管理和分配時需要實現的需求，下面給出本文所考慮的異構多核系統的資源管理目標。

1）資源數量約束：任何時刻系統運行所分配的處理核的數量和種類不能多于硬件平臺相應總數。

2）節能約束：當簇內的處理核上沒有線程運行時，將簇的狀態設置為睡眠狀態。

3）功耗約束：系統運行時的功耗受到平臺總功耗的限制。

4）電池電量狀態相關的運行約束：為了延長系統運行時間、延長系統使用壽命等，不同電量狀態對功耗值的限制額度不同。

5）功耗限制下的性能優化：在系統當前功耗限制情況下，最大化運行應用的性能或服務質量。

3.2 離散控制器合成

針對資源管理問題，本節介紹如何基于自動機來對系統行為及其控制進行建模，并在此基礎上對系統目標進行定義，從而將其描述為一個DCS問題。

3.2.1 硬件執行平臺

系統硬件執行平臺由一個大處理核簇（A0、A1）和一個小處理核簇（A2、A3）以及為平臺供電的電池構成。每個簇可以在睡眠狀態以及不同的電壓/頻率工作狀態進行切換，這些狀態之間的切換是可控的。假定大核簇除了睡眠狀態（表示為SleB）外，還有高頻、中頻和低頻三個工作模式（分別表示為HB、MB和LB），那么其行為可以采用圖5 中的狀態機來表示。而小核簇模型與大核類似，這里假定小處理核簇有睡眠、高頻和低頻（SleL、HL、LL）三個狀態。

從圖5 中可以看出，出于節能考慮，大處理核簇的初始狀態為SleB，表示沒有被任何應用使用。當簇中某個核被分配給應用時，選用簇的何種DVFS 等級進行工作則受可控變量c1、c2、c3控制，例如當c1有效時那么簇就進入DVFS 為高的工作狀態HB。輸出變量F_levelB（被定義到狀態中）用于表示該簇所處的工作狀態或DVFS 等級。另外，考慮到簇在不同狀態下的靜態功耗是不同的，同時定義輸出變量S_powerB來表示其當前狀態的靜態功耗。小處理核簇的行為可以用類似的狀態機來相應地建模表示。

圖5 大核簇行為模型Fig.5 Model for big cluster behaviors

假定系統電池的電量由高、中、低三個等級（狀態）構成，并且系統配備了可以檢測電量等級變化并發出等級上升up和下降事件down的電量傳感器，那么其行為就可以用圖6 的狀態機Battery 模型來描述。初始時，電池電量滿額處于H 狀態，隨著等級上升up和下降down事件的變化電池當前的電量級別也產生相應變化，輸出變量B_level、power_limit用來表示當前的電池狀態和功耗限制。

圖6 電池行為模型Fig.6 Model for battery behaviors

3.2.2 應用行為及其資源分配

當系統收到一個應用的執行請求時，由于其在使用不同資源組合時的性能和功耗表現往往不同，資源管理模塊就需要根據當前的系統可用資源情況和系統目標為其選擇適宜的資源分配方案。圖7 給出了具有兩種資源分配方案的應用APPA的行為模型。初始時應用處于空閑狀態IdleA，當應用被請求（也就是接受到req信號）時，應用可能進入狀態V1A或V2A，分別表示APPA的兩種執行狀態（資源使用方案）。而如何選擇應用的執行狀態則是資源管理部件通過可控變量c來進行控制的，這里模型進行定義：1）輸出變量num_big和num_little來表示所使用的大核和小核的數量；2）性能perf和功率power變量表示該應用在運行時的性能參數和功耗值。此外，在應用的執行過程中，由于系統運行環境的變化，比如電池電量變低，應用還可能在兩種執行狀態之間進行切換從而滿足功耗等方面需求，其轉換同樣由資源管理部件通過可控變量c來進行控制。當收到表示應用執行結束的end信號時，應用再次回到IdleA狀態。

圖7 應用執行行為模型Fig.7 Model for application execution behaviors

需要指出的是，獲取可行的資源方案及其性能指標可以通過類似3.1.2 節中的探索方式得到，本文假定選取的均是滿足應用最低性能要求的方案，并且這些方案及其性能和功率指標均是通過將各個簇運行在最低頻率值情況下模擬獲得的。

3.2.3 系統全局行為及控制目標定義

由于系統資源分配的目標（見3.1.3 節）往往是針對整個全局系統而言的，因此需首先構建系統全局行為模型。通過把本部分描述的各個模型進行并行組合就可以得到系統的全局行為模型S：

全局行為模型定義了系統所有可能的運行狀態和行為，包括在外部事件發生時（例如某個應用被啟動、電池電量變化）可能引起的運行狀態和行為變化，其所有可能狀態可以表示為Qf：

其中，q(·)表示相關狀態機的任意狀態。

基于第2 章描述的DCS 技術，在以上系統模型基礎上定義控制目標后便可以采用合成工具和算法來自動地合成一個正確的資源管理控制模塊。由于系統目標涉及一些運行時狀態的開銷，因而首先需要基于前面各個模塊模型上定義的局部開銷來定義整個系統模型的全局（總）開銷。給定一個系統全局狀態q，其由一系列的局部狀態(q1，q2，…，qn)組成，那么可以定義全局開銷如下（如果開銷變量未在局部模型上定義那么就為0）。

1）統計已分配的大（或者相應小）處理核個數：

2）系統性能，即系統正在執行的所有應用性能值的和：

3）系統功耗，即系統硬件平臺的靜態功耗（大核簇和小核簇靜態功耗的和）和所執行應用的動態功耗的和：

基于以上定義的系統自動機模型以及系統開銷，下面對3.1.3 節給出的系統資源分配目標進行定義。結合DCS 合成算法，這里區分了兩種類型合成目標：邏輯控制和單步最優控制。

1）邏輯控制。對于任意的系統狀態q，需滿足：

①資源約束。系統分配的大處理器核或小處理器核數目不能超出平臺相應總的處理器數量：

其中numbig表示系統總的大核數量。

其中numlittle表示系統總的小核數量。

②節能約束。

a）當簇內的處理核上沒有線程運行時，將簇的狀態設置為睡眠狀態：

b）當簇內的處理核上有線程運行時，將簇的狀態設置為工作狀態：

③功耗約束。

其中，power_limit表示系統當前的功耗約束。

④在電池電量狀態不同的情況下限制不同的平臺功耗：

2）單步最優控制。在滿足邏輯控制目標的系統狀態中選擇能使某個開銷最大或最小化的狀態。

⑤功率限制下的性能優化。

其中：q'表示q可能達到的下一個狀態；max(perf(q'))表示從可能狀態中選擇性能值最大的那個狀態。

3.3 BZR代碼描述和離散控制器合成

給定3.2 節定義的系統行為模型和系統目標后，就可以直接使用DCS 工具和語言BZR（http：//bzr.inria.fr）中的語法和語義來分別對它們進行代碼描述。BZR是一種同步數據流（synchronous data-flow）編程語言，屬于同步語言（synchronous language）［35］的一種，它使用node（節點）作為基本編程單元，并定義了contract（合同）結構來描述控制目標。

3.3.1 系統行為描述

代碼1 為對圖7 的自動機也就是應用執行行為進行BZR代碼描述的例子。如第1）行所示，該APPa 模塊被聲明為一個節點（node），其輸入變量c、req、ed（bool 型）被定義到節點名APPa后面的括號中，關鍵字returns用于給出該模塊（或節點）的輸出（也就是power、perf等）。第3）～17）行使用關鍵字let和tel定義了節點的主體部分，let后的automaton關鍵字指明了該節點是一個自動機。在自動機中使用關鍵字state 描述其狀態，關鍵字do指明與該狀態相關聯的行為，unless-then則指示狀態的轉換條件和目標狀態。

代碼1 APPA的自動機代碼描述。

以第4）～7）行描述的Idle狀態及其轉換行為為例，當處于Idle 狀態時，其功耗power、使用的大核數目num_big等變量被賦值為0；一旦有請求信號req到達，那么取決于可控變量c的取值，自動機可以轉換到V1 或者V2 狀態。狀態V1 和V2 的描述類似，在此不再贅述。

3.3.2 控制目標描述

代碼2為使用BZR中的contract結構對3.2.3節中系統的資源約束控制目標進行代碼描述的例子。contract 結構使用contract關鍵字進行聲明（第1）行），與控制目標相關而系統模型中未定義的變量需要通過緊隨其后的關鍵字var 給出。這里第2）行定義了與資源約束控制目標相關、表示系統中已分配的大、小處理核數目的局部變量num_big和num_little。關鍵字let和tel之間的部分用于將這些局部變量與系統模型（也就是自動機模型）中定義的變量進行關聯，比如這里的num_big就是系統當前所執行應用A 和應用B 所分配的大處理核數目（表示為num_bigA和num_bigB）之和，見代碼第4）行。第5）行的num_little定義類似。關鍵字enforce 用于聲明DCS 所要執行的控制目標，這里確保使用的大小核數均不超過2 個（即小于3 個），見代碼第7）行。第8）行的with 關鍵字給出DCS 為了確保系統能夠滿足enforce 聲明的控制目標所能夠控制的控制變量列表。

對3.2節中所有系統行為模型和控制目標進行BZR 代碼描述后，使用BZR 工具進行編譯就可以自動調用其所關聯ReaX 工具中的DCS 算法來自動生成一個滿足控制目標的控制器，而且用戶還可根據需要選擇采用C 或者Java 作為所生成控制器的源代碼。

代碼2 contract結構描述。

4 模擬驗證和評估實驗

本章首先使用BZR 工具對文中的展示系統和模型進行模擬驗證，然后對本文采用的DCS 方法進行可拓展性（scalability）評估。

4.1 模擬驗證

在DCS 工具BZR 自動生成一個滿足系統需求的控制器后，為了展示所合成的控制器的正確性，該工具還提供了將合成的控制器與原先系統進行整合并對控制后的系統行為進行模擬驗證的部件。通過該部件，設計者可以通過交互的方式在任意時刻對外部不可控變量進行隨機賦值，從而驗證目標系統行為是否進行相應變化從而滿足系統需求。

圖8 給出了其中一個模擬場景的模擬結果截圖，這里假設在電池電量處于高、中和低狀態時系統的功率約束分別為30、25 和15。圖中最左邊第1 列是系統的輸入變量r_A、r_B、e_A、e_B、up、down（分別表示：應用A請求、應用B請求、應用A結束、應用B結束、電池狀態提高、電池狀態降低）和輸出變量num_bigA、num_littleA、num_bigB、num_littleB、f_levelb、f_levell、b_lv、power_limit、power_sum、perf_sum（分別表示：A 分配大核數、A 分配小核數、B 分配大核數、B 分配小核數、大核簇DVFS 等級、小核簇DVFS 等級、電池電量等級、系統功耗限制、系統功耗、系統總體性能）。從第2 列開始分別代表當前時刻系統的輸入和輸出值。

可以看到，初始時刻（第2列）變量num_bigA、num_littleA、num_bigB、num_littleB均為0，表示系統的處理核都沒有被使用，系統還沒有應用啟動。因此此時大核簇和小核簇均被設置為睡眠狀態，即f_levelb、f_levell均為0，滿足3.2.3節定義的目標2；另外，電池狀態初始是滿額，處于高狀態，即b_lv是3，此時power_limit限額是30。

在下一時刻（第3 列），r_A、r_B均為1，表示應用A 和應用B 同時請求執行，控制器的b_lv為3（電池高電量），相應的平臺功耗限制power_limit此時為30。可以看到，此時控制部件為應用的資源分配情況（如標簽1 所示）：應用A 使用一個小核，應用B使用一個大核和一個小核，系統分配的大核和小核總數沒有超出總的可用數量，滿足3.2.3 節定義的資源限制（目標1）。另外，此時平臺功耗為27，滿足功耗限制（目標3和4），而且此時系統性能perf_sum和滿足功耗約束的大小核簇的DVFS等級也均為最高，滿足目標5。

圖8 模擬驗證Fig.8 Simulation and verification

接下來的第4 列的時刻，系統收到表示電池電量下降的事件down有效（即為1），從而導致電池的電量等級b_lv降低到2，此時相應的功耗限制power_limit變為25。此時，控制器通過優先降低兩個處理核簇的DVFS 等級f_levelb和f_levell到1從而滿足系統功耗限制25（目標3和4）。

在第5 列表示的時刻，電量進一步降低（down為1，b_lv降到1），此時的功耗限制power_limit為15，而目前兩個簇的DVFS等級已經降到最低，此時控制器通過對兩個應用所用資源資源進行了重分配（如標簽5中所示），將應用B第4列所在時刻使用的一個大核和一個小核調整為僅使用1 個小核來滿足功率限制。值得指出的是這個時候小核簇的DVFS 被提高為2，其原因在于控制部件在當前功耗額度下可以進一步提高小核簇的功率來達到系統當前約束下性能的最優（目標5）。

在最后兩列對應的兩個時刻，隨著電量增加信號up變量的值為1，電池的電量水平b_lv也依次提升到2和3，同時系統的功率限制也相應提高，最終又達到了第3 列時刻對應的性能最佳分配方案。

圖9 不同狀態下系統性能和功率變化情況Fig.9 Change of system performance and power under different states

圖9 更直觀地展示了所設計生成的控制器部件可以在保證系統滿足性能約束前提下達到最好的性能。從圖9 中可以看出，系統在不同時刻（狀態）下的功率值（power_sum）始終滿足功率約束（power_limit），并且各個狀態下系統達到的性能值（perf_sum）均為最優值（perf_max）。

4.2 可拓展性評估

跟其他形式化方法（比如模型檢測）一樣，離散控制器合成算法同樣是通過遍歷系統所有狀態空間來確保設計的正確性和可靠性，因而對于本文方法，另外一個需要考慮的問題就是所使用合成算法（工具）的可拓展性（scalability）。在本文所提出的模型的基礎上，通過不斷增加多核平臺核數和允許并行執行的應用數來對其可拓展性進行評估。特別的，由于所使用的BZR 和ReaX 工具支持同時定義多個目標并進行整體控制器綜合，因而本文所做的評估實驗是將邏輯和優化目標綜合算法的時間開銷同時考慮在內的。

所有實驗是在一臺配備了Intel Core I5 6500 CPU 和16 GB 內存的PC 上進行的，表1 中給出了針對不同系統規模進行控制器合成所統計的合成時間。從表1 中可以看出，當處理核的數目和任務數目都為8 時，系統狀態空間達到了2.8×106，此時合成時間需要7 200 s以上。為了處理具有更多處理核和應用數的系統、提高本文方法的可擴展性，用戶除了可以使用性能更加強大的計算機、花費更多時間外，還可以提高合成算法的效率或者使用模塊化合成技術［31］。

表1 不同系統規模的合成時間Tab.1 Synthesis time for different system sizes

5 結語

針對異構多核系統的資源管理問題，本文提出了一個將該問題形式化描述為一個離散控制問題的通用模型，并在此基礎上采用離散控制器合成技術自動生成一個滿足系統需求的資源管理部件，并為其提供了可靠性保證。此外，本文還通過使用現有的離散控制器綜合（DCS）工具和算法對文中的示例系統進行了設計和模擬驗證。最后，針對DCS 技術所面臨的系統狀態空間遍歷問題，通過對不同規模的系統進行控制部件綜合實驗對其可擴展性進行了評估。

相較于其他形式化的方法，本文提供了一種形式化的、自動構建式的解決方案來對異構多核系統的資源管理模塊進行可靠設計。然而，目前我們的工作還缺乏實際系統和環境的部署和驗證，下一步希望一方面將本文方法在一個實際的硬件平臺中進行實現和驗證，另一方面采用模塊化合成技術［31］來進一步提升本文方法的可擴展性。