2

我有以下程序使用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时相对于 FIFO 深度的写入和读取指针：PUSH

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

以及类似的POP更新机会

你能帮我把这个添加到这个程序中吗？

还是我应该将其设为 ltl 属性并使用它来检查它？

来自评论：我想验证这个属性，例如如果fifo已满，不应该有写请求，这是正确的语法吗？full表示fifo已满，wr_idx是写指针，我不知道如何在属性 ltl fifo_no_write_when_full {[] (full -> !wr_idx)} 中访问 fifo 进程的完整、空、wr_idx、rd_idx、深度

4

1 回答 1

1

这是一个基于进程的 FIFO1示例，我在这里给您的大小适用于任意大小，可以配置为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
}

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

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

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

当然，如果你真的想wr_idx在你的模型中添加它，你可以自己添加它。（：

其次，如果您查看 ltl properties 的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则不能pushfifofull

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

于 2017-02-11T22:39:19.283 回答