基于限定步長的消息隊(duì)列并發(fā)程序可達(dá)性算法研究

南佳輝

摘 要 消息隊(duì)列并發(fā)程序在執(zhí)行期間，容易產(chǎn)生可達(dá)性不確定問題，若能將消息隊(duì)列轉(zhuǎn)化為多棧下推系統(tǒng)，可以構(gòu)建逆向格局有限自動計(jì)算模式，提供解決辦法?；诖耍疚南葘谙薅ú介L的消息隊(duì)列可達(dá)性進(jìn)行分析，隨后，結(jié)合具體問題，探討了限定步長下消息隊(duì)列并發(fā)程序可達(dá)性算法優(yōu)化，具體如下。

關(guān)鍵詞 消息隊(duì)列;限定步長;并發(fā)程序

引言

伴隨電子計(jì)算機(jī)和信息技術(shù)領(lǐng)域多核處理器高速發(fā)展，以消息隊(duì)列作為進(jìn)程的交互方式，成為一種通用的并發(fā)系統(tǒng)模型。但是，在實(shí)際應(yīng)用中，這種系統(tǒng)模型存在顯著不確定性特征，會導(dǎo)致系統(tǒng)內(nèi)部隱藏錯誤顯現(xiàn)出來。加強(qiáng)系統(tǒng)規(guī)劃，優(yōu)化可達(dá)性算法，提高消息傳達(dá)精準(zhǔn)性和有效性十分必要。

1限定步長消息隊(duì)列可達(dá)性分析

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

在研究中，將自動機(jī)設(shè)為A，多棧下推系統(tǒng)設(shè)為M，則A為接收M當(dāng)前格局集合CA的自動機(jī)，得到ci∈CA。

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

2限定步長下的消息隊(duì)列并發(fā)程序可達(dá)性算法優(yōu)化

2.1 問題描述

假設(shè)有限消息字母表II為體系結(jié)構(gòu)，則進(jìn)程p∈P，動作形式如下：第一，發(fā)送信號p：send（q，m），其中m∈II，q∈Q，而且sender（q）=p。第二，接收信號rec（q，m），m∈II，q∈Q[2]。

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

2.2 算法優(yōu)化

（1）排隊(duì)

基于限定步長消息隊(duì)列并發(fā)程序?qū)儆诹夹蚺抨?duì)系統(tǒng)，當(dāng)且僅當(dāng)選定程序p∈P局部個棧為空閑狀態(tài)時，可以從對應(yīng)消息隊(duì)列中獲取并讀取消息。通過優(yōu)化排隊(duì)模式，能確保良序排隊(duì)下，遞歸隊(duì)列并發(fā)程序能按照如下動作執(zhí)行：

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

對于進(jìn)程處理業(yè)務(wù)來說，直到當(dāng)前所執(zhí)行的任務(wù)結(jié)束時，才能展開后續(xù)任務(wù)，而且在任務(wù)執(zhí)行的過程中，并不允許被中斷，所以，合理的排序方法，對于消息隊(duì)列的約束性十分必要。

（2）下推

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

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

2.3 方法檢驗(yàn)

（1）并發(fā)觀察

定義觀察實(shí)驗(yàn)參數(shù)模板，并將其設(shè)定為：

在程序運(yùn)行期間，用戶通過在主窗口位置進(jìn)行選擇，可以創(chuàng)建出獨(dú)立的發(fā)送與接收線程，各線程運(yùn)行，在各窗口輸出結(jié)果，運(yùn)行過程中，用戶隨時單擊窗口可以暫停進(jìn)程。這種操作方法有利于在發(fā)送線程群間執(zhí)行并發(fā)操作，而且還能在接收線程群間執(zhí)行相同的操作。

（2）正確性驗(yàn)證

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

3結(jié)束語

綜上，將基于限定步長的消息隊(duì)列并發(fā)程序作為優(yōu)化方向，轉(zhuǎn)換并推出可達(dá)性較高的多棧下推系統(tǒng)，結(jié)合限定步長模式加以改良，同時，提出多種有效的改進(jìn)算法。利用算法下推自動技術(shù)描述系統(tǒng)格局遷移問題，結(jié)合模型基本原則，計(jì)算可達(dá)性和可逆性，整合構(gòu)造自動機(jī)過程，結(jié)合算法能實(shí)現(xiàn)系統(tǒng)的進(jìn)一步優(yōu)化。

參考文獻(xiàn)

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

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

作者簡介

南佳輝（1992-），男，陜西興平人;學(xué)歷：本科，現(xiàn)就職單位：西安寰宇衛(wèi)星測控與數(shù)據(jù)應(yīng)用有限公司，研究方向：數(shù)據(jù)處理、網(wǎng)絡(luò)通信。