基于限定步长的消息队列并发程序可达性算法研究

南佳辉

摘 要 消息队列并发程序在执行期间，容易产生可达性不确定问题，若能将消息队列转化为多栈下推系统，可以构建逆向格局有限自动计算模式，提供解决办法。基于此，本文先对基于限定步长的消息队列可达性进行分析，随后，结合具体问题，探讨了限定步长下消息队列并发程序可达性算法优化，具体如下。

关键词 消息队列;限定步长;并发程序

引言

伴随电子计算机和信息技术领域多核处理器高速发展，以消息队列作为进程的交互方式，成为一种通用的并发系统模型。但是，在实际应用中，这种系统模型存在显著不确定性特征，会导致系统内部隐藏错误显现出来。加强系统规划，优化可达性算法，提高消息传达精准性和有效性十分必要。

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-），男，陕西兴平人;学历：本科，现就职单位：西安寰宇卫星测控与数据应用有限公司，研究方向：数据处理、网络通信。