[發明專利]一種檢測軟件定義網絡中數據競爭的預測性方法

有效

• 申請號: 202010135830.0
• 申請日: 2020-03-02
• 公開（公告）號: CN111431737B
• 公開（公告）日: 2022-07-12
• 發明（設計）人: 陸公正
• 申請（專利權）人: 蘇州市職業大學
• 主分類號: H04L41/147
• 分類號: H04L41/147;H04L41/40;G06F11/36
• 代理公司: 南京眾聯專利代理有限公司 32206
• 代理人: 葉涓涓

本發明提出了一種檢測軟件定義網絡中數據競爭的預測性方法，首先記錄事件跡；其次針對每個事件跡文件，根據各約束的編碼規則，構建RC約束、MHB約束、AN約束以及CP約束；隨后調用約束求解器SMT檢查約束文件的可滿足性，針對約束公式求解其是否滿足，如果約束文件可滿足，則表示跡中的事件存在數據競爭；如果約束文件不滿足則采用約束求解器SMT檢測分析的事件跡是否存在合理性跡，如果存在，則在滿足RC約束、MHB約束和AN約束的前提下重排序分析的事件跡，針對每個合理性跡重復編碼和求解是否滿足約束公式。本發明方法具有更高的數據競爭檢測能力，能夠檢測到更多的競爭，且具有較好的可擴展性。

技術領域

本發明屬于計算機軟件技術領域，涉及程序分析技術，具體涉及檢測軟件定義網絡中數據競爭的預測性方法。

背景技術

軟件定義網絡(Software Defined Networks,SDN)是一種便于網絡管理和可以由可編程網絡配置的新型網絡典范。SDN由控制平面和數據平面組成。控制平面對于數據包如何發送作出決定，而數據平面根據控制平面作出的決定發送數據包。控制平面和數據平面是相互獨立的。SDN控制器基于如OpenFlow這樣的北面接口實現控制邏輯來計算、維護和填充網絡中每個SDN交換機的轉發流表。

SDN控制器是整個網絡的核心，在異步和分布式環境開發可靠的控制器軟件是至關重要的。然而，由于異步性會導致比如數據競爭這樣的并發缺陷，使得開發這樣高度異步的軟件是很困難的。在SDN中數據包的轉發和消息傳送非常頻繁，數據包和OpenFlow消息之間會存在大量的數據競爭。

在SDN中，并發缺陷會發生在兩個地方：(1)控制平面內(控制器軟件是多線程的或分布式的)；(2)控制平面和數據平面之間的接口(兩個事件并發地訪問交換機中相同的流表，且至少有一個事件是控制器產生的寫事件)。SDN中的并發缺陷很難檢測到，因為它們只在特定的事件序列中暴露。然而，檢測這些缺陷又是很重要的，因為它們會導致丟包、增加包轉發的延時以及交換機和控制器上的處理負載。這些問題都會大大地降低SDN的性能。

第一類并發缺陷被Xu等進行了研究，他們使用SDN控制器的Happen-Before因果模型進行數據競爭檢測。第二類并發缺陷可以被動態分析器SDNRacer檢測到，該分析器也是使用事件間的Happen-Before關系來進行數據競爭檢測。

但是基于Happen-Before的方法具有有限的檢測能力并會導致誤報。究其原因，是因為既有方法只是在執行跡(也就是原始跡)上檢測數據競爭，只考慮了并發線程在執行時的交互。

發明內容

為解決上述問題，我們經過研究發現，基于Happen-Before的方法只能檢測觀察到的事件跡(即分析的事件跡)中的數據競爭，主要思想是在Happen-Before圖(描述事件間Happen-Before關系的圖)中的兩個并發事件之間是否存在路徑，如果不存在路徑，則兩個事件不存在Happen-Before關系，即它們之間存在數據競爭，否則它們之間不存在數據競爭。如果我們在某些約束條件下重排序觀察到的事件跡中的事件，存在Happen-Before關系的兩個并發事件可能在重排序的跡中形成數據競爭。但基于Happen-Before的方法不能找到這樣的數據競爭。

基于上述研究，本發明提出了一種檢測軟件定義網絡中數據競爭的預測性方法(SDN-Predict)，以軟件定義網絡中的控制器軟件作為研究對象，采用預測性分析技術檢測控制器軟件生成的事件跡中存在的數據競爭。在滿足讀一致性約束、Must Happen Before約束和異步不確定性約束的條件下，重排序分析的事件跡，把事件之間的約束編碼成一階邏輯公式，通過SMT約束求解器Z3求解公式的可滿足性，根據公式是否可滿足來分析兩個并發事件之間是否存在數據競爭，最后使用SDNRacer中提出的過濾規則過濾無害的數據競爭。

為了達到上述目的，本發明提供如下技術方案：

一種檢測軟件定義網絡中數據競爭的預測性方法，包括如下步驟：