零担属性和普罗梅拉程序

我有以下程序，它使用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: %dn", _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: %dn", _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是写入指针，我不知道如何在属性 ltl fifo_no_write_when_full {[] (full -> ！ wr_idx)} 中访问 fifo 进程的完整、空、wr_idx、rd_idx、深度

这是我在这里为您提供的基于进程的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: %dn", _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: %dn", _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，您可以自己添加它。(:

其次，如果您查看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无法pushfifo是否full

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

相关内容

最新更新

热门标签：