基于限定步長的消息隊列并發程序可達性算法研究

南佳輝

摘 要 消息隊列并發程序在執行期間，容易產生可達性不確定問題，若能將消息隊列轉化為多棧下推系統，可以構建逆向格局有限自動計算模式，提供解決辦法。基于此，本文先對基于限定步長的消息隊列可達性進行分析，隨后，結合具體問題，探討了限定步長下消息隊列并發程序可達性算法優化，具體如下。

關鍵詞 消息隊列;限定步長;并發程序

引言

伴隨電子計算機和信息技術領域多核處理器高速發展，以消息隊列作為進程的交互方式，成為一種通用的并發系統模型。但是，在實際應用中，這種系統模型存在顯著不確定性特征，會導致系統內部隱藏錯誤顯現出來。加強系統規劃，優化可達性算法，提高消息傳達精準性和有效性十分必要。

1限定步長消息隊列可達性分析

將消息隊列并發程序轉換為多棧下推系統，之后根據多棧下推系統上逆向格局模式，完成程序遷移和轉化，并接受多棧下推系統上逆向格局集合的非確定性有限自動機[1]。通過這種方式，證明多棧下推系統具有逆向可達性，進而得出消息隊列并發程序同樣存在逆向可達性。

在研究中，將自動機設為A，多棧下推系統設為M，則A為接收M當前格局集合CA的自動機，得到ci∈CA。

通過模擬多棧下推系統內某一個棧上的操作系統，可以構造出自動機，且其屬于總自動機中的一個組成部分，能接受多棧下推系統中個棧格局集合。當已知各部分格局集合存在遷移關系時，借助自動機屬性，能模擬分析出在自動機上與戲弄狀態，并得到對應接收格局自動機，通過迭代方式，可以構造出自動機優先模式，并可以用于接收單個步長內多棧下推系統中的某個個棧逆向格局集合。

2限定步長下的消息隊列并發程序可達性算法優化

2.1 問題描述

假設有限消息字母表II為體系結構，則進程p∈P，動作形式如下：第一，發送信號p：send（q，m），其中m∈II，q∈Q，而且sender（q）=p。第二，接收信號rec（q，m），m∈II，q∈Q[2]。

發送信號p表示的是進程p相對隊列q中輸入消息，m表示被預先定義為進程p接收隊列。接收信號p表示的是進程p從隊列q中讀取消息。除此之外，還存在p：int，p：call和p：ret，分別表示的是不處理內部動作、局部過程調用動作、調動過程返回彈出和遷移到新狀態的動作。

2.2 算法優化

（1）排隊

基于限定步長消息隊列并發程序屬于良序排隊系統，當且僅當選定程序p∈P局部個棧為空閑狀態時，可以從對應消息隊列中獲取并讀取消息。通過優化排隊模式，能確保良序排隊下，遞歸隊列并發程序能按照如下動作執行：

其中，actn-1與p：recv（q，m）相等，表示進程局部個棧為非空閑狀態時，無法執行接收動作。

對于進程處理業務來說，直到當前所執行的任務結束時，才能展開后續任務，而且在任務執行的過程中，并不允許被中斷，所以，合理的排序方法，對于消息隊列的約束性十分必要。

（2）下推

下推系統是將三元組合Ρ=（G，Γ，Δ），三者分別表示的是①全局狀態集合，即包括進程控制、局部變量以及所訪問的共享內存賦值;②棧字母表;③有限遷移關系集合。下推系統格局c是元組，其中，g表示的是一種全局狀態，w表示的是包含空串字符在內的有限字符串。各部分格局之間的遷移系統對于所有字符串均成立，而且存在自反傳遞閉包關系。

遷移關系△具有三種不同的下推規則：①描述棧pop操作，能描述某個函數調用或者遞歸過程調用，并將局部變量數值存儲到棧頂。②描述棧push操作，描述函數調用返回，調用函數或者過程執行結束，從棧頂彈出并被調用函數地址和局部變量賦值，返回之后能繼續執行。若被調用的函數有返回值，則可以使用某個新定義變量以實現返回值傳遞并對調用全局狀態進行監控。③描述遞歸過程調用與函數返回以外的操作，例如，通過改變當前全局狀態而保持棧內容不變的賦值語句。

2.3 方法檢驗

（1）并發觀察

定義觀察實驗參數模板，并將其設定為：

在程序運行期間，用戶通過在主窗口位置進行選擇，可以創建出獨立的發送與接收線程，各線程運行，在各窗口輸出結果，運行過程中，用戶隨時單擊窗口可以暫停進程。這種操作方法有利于在發送線程群間執行并發操作，而且還能在接收線程群間執行相同的操作。

（2）正確性驗證

通過觀察發送線程中最后在執行緩沖區的編號，可以了解到內部選擇中，并發執行不同操作，會與緩沖區操作產生互斥情況。接收線程群中，以最后進行觀察的緩沖區編號進行分析，得到接收線程對任意緩沖區操作均為互斥。將二者聯系起來進行分析，得到在同步與互斥機制作用下，運行結果能顯示出任何發送端線程都沒有將信號數據放入到滿緩沖區，同時也是沒有放入到空閑緩沖區。證明，主線線程程序在各種情況下，都可以檢測到接收端與發送端的線程信號結束標志，并給出相應提示，避免出現死鎖現象。

3結束語

綜上，將基于限定步長的消息隊列并發程序作為優化方向，轉換并推出可達性較高的多棧下推系統，結合限定步長模式加以改良，同時，提出多種有效的改進算法。利用算法下推自動技術描述系統格局遷移問題，結合模型基本原則，計算可達性和可逆性，整合構造自動機過程，結合算法能實現系統的進一步優化。

參考文獻

[1] 張楊，孫仕欣，張冬雯.面向并發程序的重構一致性檢測方法[J].河北師范大學學報（自然科學版），2020，44（3）：200-208.

[2] 操旺根.并發程序數據競爭檢測方法研究和分析[J].信息技術與信息化，2019（12）：171-173.

作者簡介

南佳輝（1992-），男，陜西興平人;學歷：本科，現就職單位：西安寰宇衛星測控與數據應用有限公司，研究方向：數據處理、網絡通信。