当前位置：首页 > news >正文

【SPIN】PROMELA语言编程入门同步机制（SPIN学习系列--4）

news 来源：原创 2025/5/20 5:14:07

在这里插入图片描述

同步机制

PROMELA 不包含信号量、锁或监控器等常见的同步原语，而是通过语句的**可执行性（executability）**概念来建模同步机制。计算机系统的架构限制了同步机制的设计：本章主要介绍适用于共享内存系统的同步机制，第7章将讨论分布式系统中通过通信实现同步的通道（channel）。

4.1 阻塞式同步

清单4.1尝试通过忙等待（busy-waiting）解决临界区问题：

bool wantP = false, wantQ = false;
active proctype P() {do:: printf("非临界区 P\n");wantP = true;do :: !wantQ -> break; :: else -> skip; od; // 忙等待循环printf("临界区 P\n");wantP = false;od
}
// 进程Q的代码与P对称

忙等待的缺点：循环不执行有效计算，仅反复检查条件（如!wantQ），浪费处理器资源。理想情况下，系统应通过**阻塞（blocking）**释放处理器，允许其他进程运行。

在PROMELA中，if和do语句可通过 保护条件（guard） 实现阻塞。例如，将忙等待循环简化为单个条件语句：

do :: !wantQ -> break; od // 若wantQ为true，进程P阻塞在此处

阻塞的本质：

模拟模式下，SPIN不会选择阻塞进程的语句执行；
验证模式下，SPIN不会从阻塞状态继续搜索反例，直到其他进程改变状态解除阻塞。

4.2 语句的可执行性

PROMELA中，表达式语句的可执行性取决于其值：

赋值语句（如n=1）和printf始终可执行；
条件表达式（如!wantQ）仅当值为true（非零）时可执行，否则阻塞进程。

清单4.2通过简化条件语句实现阻塞同步：

active proctype P() {do:: printf("非临界区 P\n");wantP = true;!wantQ; // 阻塞直到wantQ为falseprintf("临界区 P\n");wantP = false;od
}

关键逻辑：进程在!wantQ处阻塞，直到另一进程将wantQ设为false。

4.3 状态转移图

状态转移图用于可视化并发程序的可达状态。以清单4.3为例，其状态由进程位置计数器和变量值构成：

active proctype P() { do :: wantP = true; !wantQ; wantP = false; od }
active proctype Q() { do :: wantQ = true; !wantP; wantQ = false; od }

初始状态：(P在第4行, Q在第11行, wantP=0, wantQ=0)
可达状态数：8种（远小于理论可能的36种）
死锁状态：(P在!wantQ, Q在!wantP, wantP=1, wantQ=1)，此时双方互相阻塞。

状态转移图的作用：

验证互斥性：检查是否存在双方同时进入临界区的状态；
检测死锁：识别无有效转移的阻塞状态。

4.4 原子语句序列

通过atomic或d_step关键字确保语句序列原子执行，避免干扰。例如，清单4.4将“检查条件+赋值”作为原子块：

active proctype P() {do:: printf("非临界区 P\n");atomic { // 原子块确保互斥!wantQ; // 检查条件wantP = true; // 赋值}printf("临界区 P\n");wantP = false;od
}

atomic与d_step的区别：

d_step：确定性执行，仅第一个有效分支被选择，适合顺序代码；
atomic：支持非确定性，适用于同步原语建模。

4.5 信号量模拟

通过原子操作模拟信号量（semaphore）：

byte sem = 1; // 初始值为1（表示可用资源数）
active proctype P() {do:: printf("非临界区 P\n");atomic { // wait操作sem > 0; // 检查资源可用sem--; // 占用资源}printf("临界区 P\n");sem++; // signal操作，释放资源od
}

信号量特性：

wait(sem)：仅当sem>0时执行，原子递减；
signal(sem)：无条件执行，原子递增。

4.6 非确定性建模

SPIN通过非确定性选择模拟任意输入或事件。例如，生成随机消息类型：

active proctype Client() {do:: request = 1; // 非确定性选择请求类型1:: request = 2; // 非确定性选择请求类型2od
}

注意：SPIN的非确定性用于验证所有可能路径，而非生成概率随机数。通过do循环可模拟无限序列的非确定选择。

4.7 进程终止与死锁

死锁检测：SPIN默认检查“无效终止状态”（进程未正常结束却无法继续执行）。例如，清单4.2中双方阻塞导致死锁，SPIN报告timeout。
合法终止：使用end标签标记允许的终止点，或通过-E参数忽略无效终止检查：
```
spin -a -E model.pml # 忽略无效终止状态
```
进程生命周期：进程按“后进先出（LIFO）”顺序终止，主动进程（active proctype）需显式结束循环或通过阻塞自然终止。