使用远程变量引用时Spin模型检测器未发现有bug的Peterson算法互斥模型缺陷

Let's break down why Spin isn't catching the bug in your Peterson implementation, and fix the issue step by step.

1. The Root Bug in Your Peterson Algorithm #

First, let's confirm the actual bug in your code: you've reversed the order of operations in the trying section. The correct Peterson algorithm requires you to set your own flag to true first, then set the turn variable to the other process. Your code does it the opposite way:

// Wrong order (causes mutex violation)
turn = other;
flag[_pid] = true;

// Correct order
flag[_pid] = true;
turn = other;

This reversal allows both processes to enter the critical section simultaneously—but Spin isn't picking this up because of how you're tracking critical section state in your LTL property.

2. Spin's Limitation with Local Process Variables #

The key issue here is how you're referencing the in_cs variable in your LTL property. In Spin, you can't directly reference a local variable of another process using the syntax agent[0]:in_cs. Local variables are scoped to their process instance, and Spin's LTL model checker doesn't resolve this syntax correctly for visibility across processes.

Fix: Use a Global Array to Track Critical Section State #

Replace the local in_cs variable with a global array that tracks each process's critical section status. This makes the state visible to the LTL property:

/* Mutex with (bugged) Peterson algorithm - Fixed State Visibility */
bool flag[2];
int turn = -1;
bool in_cs[2]; // Global array to track each agent's CS state

active [2] proctype agent() {
    int other = 1 - _pid;
    do
    :: true ->
        /* Trying section (BUG: reversed order remains) */
        turn = other;
        flag[_pid] = true;
        !( flag[other] && (turn == other));
        /* Critical section */
        in_cs[_pid] = true;
        printf("Agent %d in CS\n", _pid);
        in_cs[_pid] = false;
        /* Exit section */
        flag[_pid] = false;
    od;
}

ltl mutex { [] ! (in_cs[0] && in_cs[1]) }

3. Verify the Fixed Model #

Now when you run Spin on this modified code, it will correctly detect the mutex violation:

1. Generate the verification code: spin -a model.pml
2. Compile the code: gcc -o pan pan.c
3. Run the model checker: ./pan -a

You'll get an error trace showing both processes entering the critical section at the same time, which is exactly the bug we expected to catch.

4. Why the Original Code Failed #

In your original code, the local in_cs variable wasn't visible to the LTL property in the way you wrote it. Spin couldn't resolve agent[0]:in_cs to a valid state, so your LTL property effectively wasn't checking the condition you intended. This is why it didn't flag the mutex violation, even though the bug existed.

As an alternative to using a global array, you could also add an assert directly inside the critical section to check for mutual exclusion (e.g., assert(!in_cs[other]) if using a global array), but the global array approach makes the LTL property explicit and easy to reason about.

内容的提问来源于stack exchange，提问作者Patrick Trentin