【SPIN】PROMELA并发编程（SPIN学习系列--3）

一、active与run：Promela的进程创建基石

在Promela语言中，**active和run**是构建并发模型的核心关键字，分别用于定义主动进程和动态创建被动进程：

1. active proctype <进程名>()

   • 作用：声明主动进程类型，模型启动时自动实例化，无需显式调用。
   • 特点：
     • 适用于独立运行的组件（如传感器采集、设备控制）。
     • 多个主动进程并行执行，调度顺序由SPIN的非确定性机制决定。
   • 示例：

     active proctype SensorSampler() { // 循环采样传感器数据 do :: read_sensor(); :: printf("Sample taken\n"); od 
     }
     

2. run <进程名>(参数)

   • 作用：在init或其他进程中显式创建被动进程，支持参数传递。
   • 特点：
     • 被动进程需通过run触发，适合动态生成差异化实例（如带ID的工作者进程）。
     • 返回进程ID（_pid），用于跟踪进程状态。
   • 示例：

     proctype Worker(int id) { printf("Worker %d started\n", id); 
     }init { run Worker(1); // 创建进程并传递参数 run Worker(2); 
     }
     

二、并发系统建模：交错执行与原子性

1. 交错执行（Interleaving）的本质

并发程序的核心是进程语句的非确定性交错执行。以两个进程修改全局变量n为例：

byte n = 0;
active proctype P() { n = 1; printf("P: n=%d\n", n); }
active proctype Q() { n = 2; printf("Q: n=%d\n", n); }

可能的执行路径有6种，例如：

• P先执行：P写n=1→打印→Q写n=2→打印（最终n=2）。
• Q先执行：Q写n=2→打印→P写n=1→打印（最终n=1）。

SPIN通过状态表记录变量值与进程位置计数器的变化，例如：

状态1: P执行n=1 → n=1, P在第5行, Q在第9行  
状态2: Q执行n=2 → n=2, P在第5行, Q在第10行  

2. 原子性保证与潜在风险

Promela语句默认原子执行，如n=1不可中断，确保不会出现中间值。但在条件语句中，条件判断与执行可能被打断：

if :: a != 0 -> c = b / a; // 风险：判断后a可能被其他进程改为0  
:: else -> c = b;  
fi

此时需通过atomic块显式保护关键代码：

atomic { if :: a != 0 -> c = b / a; :: else -> c = b; fi 
}

三、JSPIN工具与交互式模拟

1. JSPIN的可视化调试

JSPIN是SPIN的图形化界面，支持：

• 执行轨迹可视化：在右侧面板显示进程输出，如：

  Process Q, n = 2  
  Process P, n = 1  
  2 processes created  
  

• 状态表查看：通过Options/Common/Set all显示状态表，包含进程ID、执行语句、变量值：

  0 P 4 n = 1  
  1 Q 9 n = 2  
  

2. 命令行与交互式模拟

• 命令行输出：

  spin -a model.pml && gcc -o pan pan.c && ./pan -r  
  

  SPIN自动缩进printf输出，区分不同进程来源。使用-T关闭缩进，-p -g显示详细变量变化。

• 交互式模拟：

  • JSPIN：选择“Interactive”，通过弹窗手动选择执行语句，支持键盘导航（Tab切换，Space选择）。
  • 命令行：使用spin -i，逐行选择执行路径：

    Select a statement  
    choice 1: proc 1 (Q) line 9 [n = 2]  
    choice 2: proc 0 (P) line 4 [n = 1]  
    Select [1-2]:  
    

四、进程干扰与验证技术

1. 共享资源干扰案例

当多个进程通过临时变量操作共享资源时，可能引发意外结果。例如，两个进程尝试自增n：

byte n = 0;
active proctype Incrementer() { byte temp; temp = n + 1; // 读取旧值  n = temp;      // 写入新值  
}

若进程A读取n=0→计算temp=1，进程B此时读取n=0→计算temp=1，最终两者依次写入n=1，导致预期n=2变为n=1。这种干扰源于未同步的读写操作。

2. SPIN验证流程

• 断言（Assertion）：通过assert(n == 2)检测预期结果，SPIN会搜索反例。例如，在清单3.5中添加assert(n > 2)，SPIN将自动查找导致n≤2的执行路径。
• 反例追踪：验证失败时，SPIN生成跟踪文件（.trail），通过spin -t可视化违规路径。

五、进程集合与临界区问题

1. 批量创建进程实例

使用active [N] proctype声明多个相同进程，通过_pid区分实例：

active [3] proctype Worker() { printf("Worker %d started\n", _pid); // _pid自动为0、1、2  
}

2. 临界区与互斥验证

临界区问题要求确保同一时刻仅一个进程访问共享资源。通过幽灵变量critical统计临界区进程数，并结合断言assert(critical <= 1)验证互斥性：

byte critical = 0;
active proctype Task() { critical++; assert(critical <= 1); // 验证互斥  critical--; 
}

SPIN检测到critical=2时，会报告断言失败，揭示并发违规。

六、SPIN建模全流程与最佳实践

1. 定义进程：
   • 主动进程：active proctype自动启动。
   • 被动进程：proctype配合run动态创建，支持参数传递。
2. 初始化与调度：

   init { atomic { // 确保进程全部启动后执行  run Worker(1); run Worker(2); } 
   }
   

3. 验证与调试：
   • 随机模拟：./pan -r探索随机路径。
   • 交互式模拟：spin -i手动构造特定交错场景。
   • LTL属性验证：使用-l参数验证死锁、活性等属性（如[]<> !deadlock）。

总结

active与run是Promela并发建模的基础，分别实现自动启动进程与动态参数化实例创建。理解进程交错执行、原子性边界及JSPIN的可视化调试工具，是有效分析并发系统干扰问题的关键。通过断言验证与交互式模拟，SPIN为复杂并发系统的正确性验证提供了完整工具链，而临界区问题的建模则凸显了同步机制在并发编程中的核心地位。后续章节将深入探讨分布式系统建模、信号量机制及LTL属性的形式化验证。