1

请我是 tihs 领域的大佬，如何将用 systemC 代码编写的经典示例 FIFO 转换为具有 LTL 属性的 PROMELA 语言满足以下三个属性：

互斥：生产者和消费者进程从不同时访问共享缓冲区。

非饥饿：消费者经常无限地访问缓冲区。（您可以假设生产者永远不会用完要提供的数据，而消费者永远不会停止尝试读取新数据。）

生产者-消费者：生产者永远不会覆盖数据缓冲区，除非消费者已经读取了当前数据消费者永远不会读取数据缓冲区，除非它包含新数据。生产者-消费者的常用算法使用单个标志位。标志位在数据准备好读取时由生产者设置，一旦读取数据由消费者取消设置。为了这个赋值，我们只需要建模数据缓冲区是否已经被读取，而不是建模数据的内容。我们将为此使用一个位。

您的任务是在 Promela 中对该算法进行建模，然后验证有关它的上述属性。记住 (1) 和 (3) 是安全属性，但 (2) 是活性属性，​​这将有所帮助。您可以在适当的情况下同时使用 LTL 和内联断言。

这是我第一次尝试解决这个问题：

#define NUMCHAN 4 

chan channels[NUMCHAN]; 
chan full[0]; 

init
{
    chan ch1 = [1] of { byte };
    chan ch2 = [1] of { byte };
    chan ch3 = [1] of { byte };
    chan ch4 = [1] of { byte };
    channels[0] = ch1;
    channels[1] = ch2;
    channels[2] = ch3;
    channels[3] = ch4;
    // Add further channels above, in accordance with NUMCHAN
    // First let the producer write something, then start the consumer
    run producer(); 
    atomic {
        _nr_pr == 1 -> run consumer();
    }
}

proctype read()
{
    byte var, i;
    chan theChan;
    do
        :: fread?1 ->
        if readptr == writeptr -> empty ! 1 
        fi  
        read ! 0 
        readptr = readptr+1 mod NUMCHAN
        ack ?1
    od 
    ack!1
    i = 0;
    do
        :: i == NUMCHAN -> break
        :: else -> theChan = channels[i];
        if
            :: skip // non-deterministic skip
            :: nempty(theChan) ->
                theChan ? var;
                printf("Read value %d from channel %d\n", var, i+1)
        fi;
        i++
    od
}

proctype consumer()
{
    do // empty
        if
            empty ? 0 // read // data 
            theChan ? data 
            :: fread!1 -> ack ?1 
    od 
}

我创建了两个基本流程，生产者和消费者。

生产者通过通道fwrite绑定到另一个名为write的进程，而消费者通过通道fread绑定到另一个名为read的进程。这里，read和write包含读写指针。

消费者是不完整的，我只是勾勒出我的想法。我希望在通道或FIFO表的总写入之后发生读取，并且生产者可以写入N个信息而不满足FIFO的大小。

4

1 回答 1

0

注意：从评论来看，您尝试解决的问题看起来非常复杂，并且可能会受益于被分解成更小更容易的部分。

片断 01：简单的生产者/消费者超过 FIFO + ltl 属性

恕我直言，这是处理模型检查和形式验证时的首选方法：您应该从要建模的系统中抽象出实现和语言相关的特性，并专注于其行为的核心方面。

考虑到这种方法，不言而喻的是，尽管在Promela中将生产者和消费者等活动代理建模为进程是有意义的，但对SystemC代码的类 FIFO建模毫无意义，尤其是考虑到Promela已经提供了可以作为同步和异步FIFO队列的chan 。

在这里，我提供了一个非常基本的系统模型，只有一个生产者和一个客户，它允许进行一些简化：

/**
 * Producer / Consumer 
 */

mtype = { PAYLOAD_MSG };

// Asynchronous Channel
chan fifo = [1] of { mtype, int };
bool data_read = true;

active [1] proctype producer()
{
  int v;
  do
    :: nfull(fifo) ->
        select(v : 0..16);
        printf("P[%d] - produced: %d\n", _pid, v);
access_fifo:
        atomic {
            fifo!PAYLOAD_MSG(v);
            data_read = false;
        }
  od
}

active [1] proctype consumer()
{
  int v;
  do
    :: nempty(fifo) ->
access_fifo:
        atomic {
            fifo?PAYLOAD_MSG(v);
            data_read = true;
        }
        printf("P[%d] - consumed: %d\n", _pid, v);
  od
}

#define prod_uses_fifo    (producer@access_fifo)
#define cons_uses_fifo    (consumer@access_fifo)
#define fair_production   ([]<> (_last == 0))
#define cons_not_starving ([]<> (_last == 1))
#define no_overwrite      ([] (prod_uses_fifo -> data_read))
#define no_invalid_read   ([] (cons_uses_fifo -> !data_read))

// Mutual Exclusion
ltl p1 { [] (!prod_uses_fifo || !cons_uses_fifo) }

// Non-Starvation
ltl p2 { fair_production && fair_production -> cons_not_starving }

// Producer-Consumer
ltl p3 { no_overwrite && no_invalid_read }

请注意，我选择将fifo声明为带有 的异步通道，chan fifo = [1]而不是带有 的同步通道，chan fifo = [0]因为您的互斥属性要求生产者和消费者不能同时访问fifo。在同步先进先出中，消费者和生产者总是[并且仅]同时访问先进先出，但没有竞争条件，因为消息直接从生产者移交给消费者。

片断02：作为进程的fifo

现在让我们将生产者、消费者和ltl 属性抛在脑后，关注如何将FIFO 队列建模为Process。

同样，重点应该放在抽象所需的行为上，而不是原始SystemC源代码的一对一映射。我会冒昧地丢弃时钟输入信号并合并所有输入[resp。输出] 成单线。由于在您的评论中您声明您想要一个同步的fifo，我也将禁止write-after-write事件并假设fifo的大小为1。 

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;
}

我选择让push/pop尝试失败安全：根据设计，不可能覆盖或读取无效数据。

把所有东西放在一起。

然后可以更新生产者和消费者进程以使用这个fifo进程而不是内置的 chan：

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;
}

你应该注意到这个实现依赖于繁忙的轮询，从性能的角度来看这不是一个明智的想法，尽管它是最简单的建模方法。

另一种方法是使用共享变量和互斥体，但这会破坏FIFO作为具有输入和输出的组件的概念，这显然是您想要建模的。

组件可以像这样连接在一起：

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 属性：

#define prod_uses_fifo    (producer@access_fifo)
#define cons_uses_fifo    (consumer@access_fifo)
#define fair_production   ([]<> (prod_uses_fifo && _last == 2))
#define cons_not_starving ([]<> (cons_uses_fifo && _last == 3))

// Mutual Exclusion
ltl p1 { [] (!prod_uses_fifo || !cons_uses_fifo) }

// Non-Starvation
ltl p2 { fair_production && fair_production -> cons_not_starving }

// Producer-Consumer
// assertions already guarantee that there is no attempt to 
// overwrite or read invalid data

现在，我不确定这种方法是否朝着您想要的方向发展，因此我将等待进一步的反馈，以防更新我的答案。

于 2016-12-19T11:27:50.060 回答