[發明專利]一種基于GPU的模型計數及其約束的求解方法

在審

• 申請號: 202010908484.5
• 申請日: 2020-09-02
• 公開（公告）號: CN112131583A
• 公開（公告）日: 2020-12-25
• 發明（設計）人: 宋富;高鵬飛;謝弘毅
• 申請（專利權）人: 上海科技大學
• 主分類號: G06F21/60
• 分類號: G06F21/60;G06F21/62
• 代理公司: 上海申匯專利代理有限公司 31001
• 代理人: 徐俊

本發明涉及一種基于GPU的模型計數及其約束的求解方法，其特征在于，包括以下步驟：利用編譯技術將邏輯公式及其約束翻譯到中間表示形式；根據GPU信息和邏輯公式，將程序變量劃分為三個集合分別用CPU、GPU線程標識符和GPU枚舉具體取值；生成GPU源代碼程序并編譯執行，GPU程序執行結果為邏輯公式及其約束的求解結果。本發明達到了顯著的性能提升效果。通過多個實驗，本發明達到了顯著的性能提升效果，本發明提出的方法比傳統基于CPU枚舉的和SMT求解器的方法相比，性能提升數百倍。

技術領域

本發明涉及一種基于GPU的模型計數及其約束的求解方法，可應用于差分隱私和隨機掩碼等程序的安全分析與驗證。

背景技術

近年來，隨著移動互聯網快速發展，信息安全和隱私數據的保護意識也逐步增強。國內外學者提出了各種技術方法用于保護隱私數據，其中差分隱私和隨機掩碼是兩種廣泛采用的有效防護方法。差分隱私和隨機掩碼保護通過引入隨機變量來消除或減少隱私數據和可觀察數據之間的相關性。然而，正確實現具有差分隱私或隨機掩碼保護的程序是一項困難且易于出錯的工作，因此國內外學者提出了各種驗證算法用于分析與驗證程序的差分隱私或隨機掩碼保護是否正確或滿足安全需求。在各種驗證算法中，基于模型計數及其約束的算法具有完備性和無誤報特點而被廣泛采用。然而，模型計數的計算復雜性非常高，在實際應用中無法高效地對差分隱私或隨機掩碼保護的程序進行驗證。

發明內容

本發明的目的是：利用GPU強大的并行計算能力快速地求解模型計數及其約束問題，從而可以在實際應用中高效地的驗證差分隱私或隨機掩碼保護的程序是否安全。

為了達到上述目的，本發明的技術方案是提供了一種基于GPU的模型計數及其約束的求解方法，其特征在于，包括以下步驟：

步驟1、對于任意給定一個或一組邏輯公式表示的模型計數或模型計算約束問題，利用編譯技術將公式翻譯為中間結果表達式；

步驟2、根據邏輯公式變量數和GPU的架構信息，將變量劃分為三類：CPU枚舉變量、GPU線程標識符對應變量、GPU線程枚舉變量；

步驟3、根據變量劃分，通過遍歷邏輯公式的中間結果形式，自動生成GPU程序，從而將模型計數及其約束問題轉化為GPU程序執行，調用GPU程序編譯器進行編譯并運行GPU可執行文件，根據模型計數或模型計算約束問題給出執行結果，其中，GPU程序生成過程包括以下步驟：

步驟3.1、對邏輯公式中的邏輯運算符，判斷是不是GPU程序支持的運算符，如果是GPU中不支持的運算符，則在GPU程序中生成一個對應的__device__類型的函數實現該運算，供后續調用；如果是GPU程序中支持的運算符，則直接使用GPU程序中對應的運算符；

步驟3.2、對每一個邏輯表達式，通過遍歷其中間表示形式，在GPU程序中生成一個對應的__device__類型的函數用于計算邏輯表達式的值，其參數分別是CPU和GPU枚舉變量的一組具體值以及線程標識符，表達式的計算通過GPU內置的運算符和步驟3.1中定義的__device__類型的函數實現；

步驟3.3、在GPU程序中生成一個核函數，該核函數枚舉GPU線程枚舉變量的取值，對每一組取值，調用對應邏輯公式的__device__函數計算所有邏輯公式的具體值；在數組中以所有邏輯公式的值為索引的模型數量加1；

步驟3.4、在GPU程序中生成一個主函數，該主函數設置GPU流處理器線程網絡模式，將核函數布置到線程網絡，初始化保存模型計數的數組使得每個索引的模型數量為0；枚舉CPU枚舉變量的取值，對每一組枚舉的變量取值，調用核函數并把變量取值以參數形式傳遞給核函數；