LTL性质与promela程序

Question

我有下面的程序，它用PROMELA中的进程来建模FIFO

mtype = { PUSH, POP, IS_EMPTY, IS_FULL };

#define PRODUCER_UID 0
#define CONSUMER_UID 1

proctype fifo(chan inputs, outputs)
{
    mtype command;
    int data, tmp, src_uid;
    bool data_valid = false;

    do
        :: true ->
            inputs?command(tmp, src_uid);
            if
                :: command == PUSH ->
                    if
                        :: data_valid ->
                            outputs!IS_FULL(true, src_uid);
                        :: else ->
                            data = tmp
                            data_valid = true;
                            outputs!PUSH(data, src_uid);
                    fi
                :: command == POP ->
                    if
                        :: !data_valid ->
                            outputs!IS_EMPTY(true, src_uid);
                        :: else ->
                            outputs!POP(data, src_uid);
                            data = -1;
                            data_valid = false;
                    fi
                :: command == IS_EMPTY ->
                    outputs!IS_EMPTY(!data_valid, src_uid);
                :: command == IS_FULL ->
                    outputs!IS_FULL(data_valid, src_uid);
            fi;
    od;
}

proctype producer(chan inputs, outputs)
{
    mtype command;
    int v;

    do
        :: true ->
            atomic {
                inputs!IS_FULL(false, PRODUCER_UID) ->
                outputs?IS_FULL(v, PRODUCER_UID);
            }
            if
                :: v == 1 ->
                    skip
                :: else ->
                    select(v: 0..16);
                    printf("P[%d] - produced: %d\n", _pid, v);
access_fifo:
                    atomic {
                        inputs!PUSH(v, PRODUCER_UID);
                        outputs?command(v, PRODUCER_UID);
                    }
                    assert(command == PUSH);
            fi;
    od;
}

proctype consumer(chan inputs, outputs)
{
    mtype command;
    int v;

    do
        :: true ->
            atomic {
                inputs!IS_EMPTY(false, CONSUMER_UID) ->
                outputs?IS_EMPTY(v, CONSUMER_UID);
            }
            if
                :: v == 1 ->
                    skip
                :: else ->
access_fifo:
                    atomic {
                        inputs!POP(v, CONSUMER_UID);
                        outputs?command(v, CONSUMER_UID);
                    }
                    assert(command == POP);
                    printf("P[%d] - consumed: %d\n", _pid, v);
            fi;
    od;
}

init {
    chan inputs  = [0] of { mtype, int, int };
    chan outputs = [0] of { mtype, int, int };

    run fifo(inputs, outputs);     // pid: 1
    run producer(inputs, outputs); // pid: 2
    run consumer(inputs, outputs); // pid: 3
}

我想在程序中添加wr_ptr和rd_ptr，以便在执行PUSH更新时指示与FIFO深度相关的写和读指针：

wr_ptr = wr_ptr % depth;
empty=0;
if
    :: (rd_ptr == wr_ptr) -> full=true; 
fi

以及POP更新的类似机会

你能帮我把这个加到这个节目里吗？

或者我应该让它成为一个ltl属性，并使用它来检查它？

注释:并且我想验证这个属性，例如，如果fifo是满的，就不应该有写请求，这是正确的语法吗? full意味着fifo是满的，wr_idx是写指针，我不知道如何访问完整的、空的、wr_idx的、rd_idx的、深入于属性ltl fifo_no_write_when_full {full -> ! wr_idx}的fifo进程。

Answer 1

下面是一个基于进程的FIFO与大小1的示例，我给您提供了适合于任意大小的这里，可以使用FIFO_SIZE进行配置。为了验证目的，我将尽可能地保持这个值(例如3)，因为否则您只是在扩大状态空间，而不包括任何更重要的行为。

mtype = { PUSH, POP, IS_EMPTY, IS_FULL };

#define PRODUCER_UID 0
#define CONSUMER_UID 1
#define FIFO_SIZE    10

proctype fifo(chan inputs, outputs)
{
    mtype command;
    int tmp, src_uid;
    int data[FIFO_SIZE];
    byte head = 0;
    byte count = 0;
    bool res;

    do
        :: true ->
            inputs?command(tmp, src_uid);
            if
                :: command == PUSH ->
                    if
                        :: count >= FIFO_SIZE ->
                            outputs!IS_FULL(true, src_uid);
                        :: else ->
                            data[(head + count) % FIFO_SIZE] = tmp;
                            count = count + 1;
                            outputs!PUSH(data[(head + count - 1) % FIFO_SIZE], src_uid);
                    fi
                :: command == POP ->
                    if
                        :: count <= 0 ->
                            outputs!IS_EMPTY(true, src_uid);
                        :: else ->
                            outputs!POP(data[head], src_uid);
                            atomic {
                                head = (head + 1) % FIFO_SIZE;
                                count = count - 1;
                            }
                    fi
                :: command == IS_EMPTY ->
                    res = count <= 0;
                    outputs!IS_EMPTY(res, src_uid);
                :: command == IS_FULL ->
                    res = count >= FIFO_SIZE;
                    outputs!IS_FULL(res, src_uid);
            fi;
    od;
}

不需要改变producer、consumer或init：

proctype producer(chan inputs, outputs)
{
    mtype command;
    int v;

    do
        :: true ->
            atomic {
                inputs!IS_FULL(false, PRODUCER_UID) ->
                outputs?IS_FULL(v, PRODUCER_UID);
            }
            if
                :: v == 1 ->
                    skip
                :: else ->
                    select(v: 0..16);
                    printf("P[%d] - produced: %d\n", _pid, v);
access_fifo:
                    atomic {
                        inputs!PUSH(v, PRODUCER_UID);
                        outputs?command(v, PRODUCER_UID);
                    }
                    assert(command == PUSH);
            fi;
    od;
}

proctype consumer(chan inputs, outputs)
{
    mtype command;
    int v;

    do
        :: true ->
            atomic {
                inputs!IS_EMPTY(false, CONSUMER_UID) ->
                outputs?IS_EMPTY(v, CONSUMER_UID);
            }
            if
                :: v == 1 ->
                    skip
                :: else ->
access_fifo:
                    atomic {
                        inputs!POP(v, CONSUMER_UID);
                        outputs?command(v, CONSUMER_UID);
                    }
                    assert(command == POP);
                    printf("P[%d] - consumed: %d\n", _pid, v);
            fi;
    od;
}

init {
    chan inputs  = [0] of { mtype, int, int };
    chan outputs = [0] of { mtype, int, int };

    run fifo(inputs, outputs);     // pid: 1
    run producer(inputs, outputs); // pid: 2
    run consumer(inputs, outputs); // pid: 3
}

现在，您应该有足够的材料进行工作，并准备好编写您自己的属性。在这方面，你在问题中写道：

我不知道如何访问完整、空、wr_idx、rd_idx进程深度在属性ltl fifo_no_write_when_full {full -> ! wr_idx}中的fifo进程。

First of，请注意，在我的代码中，rd_idx对应于head，depth (应该)对应于count，而我没有使用显式wr_idx，因为后者可以从前两者派生出来:它是由(head + count) % FIFO_SIZE给出的。这不仅仅是代码清洁度的选择，因为Promela模型中的变量较少实际上有助于内存消耗和验证过程的运行时间。

当然，如果您真的希望在您的模型中有wr_idx，您可以自己添加它。(：

Second，如果您查看用于ltl属性的Promela 手册，您会发现：

必须定义名称或符号来表示模型中全局变量上的布尔表达式。

换句话说，不可能将局部变量放入ltl表达式中。如果您想使用它们，那么您应该从进程的本地空间中取出它们，并将它们放到全局空间中。

因此，要检查fifo_no_write_when_full*，您可以：

• 将count的声明移出全局空间
• 在这里添加一个标签fifo_write:：

                :: command == PUSH ->
                    if
                        :: count >= FIFO_SIZE ->
                            outputs!IS_FULL(true, src_uid);
                        :: else ->
    fifo_write:
                            data[(head + count) % FIFO_SIZE] = tmp;
                            count = count + 1;
                            outputs!PUSH(data[(head + count - 1) % FIFO_SIZE], src_uid);
                    fi

• 检查财产：

    ltl fifo_no_write_when_full { [] ( (count >= FIFO_SIZE) -> ! fifo@fifo_write) }

第三次，在尝试使用常规命令验证任何属性之前，例如：

~$ spin -a fifo.pml
~$ gcc -o fifo pan.c
~$ ./fifo -a -N fifo_no_write_when_full

您应该修改producer和consumer，使它们都不会在无限长的时间内执行，从而使搜索空间保持在较小的深度。否则，您可能会得到这类错误。

error: max search depth too small

并且让验证耗尽您的所有硬件资源，而不得出任何合理的结论。

*实际上fifo_no_write_when_full这个名字是相当通用的，可能有多种解释。

• 当fifo已满时，它不会执行push。
• 如果producer是full，则fifo无法进行full

在我提供的示例中，我选择采用对该属性的第一种解释。