convert fifo systemC program to PROMELA language with safety properties and liveness property

Question

please i am a biginner on tihs domain how can i convert a classical example FIFO written in systemC code to PROMELA language with properties in LTL satisfy the following three properties:

Mutual exclusion: The producer and consumer processes never access the shared buffer simultaneously.

Non-starvation: The consumer accesses the buffer infinitely often. (You may assume that the producer never runs out of data to supply, and the consumer never stops attempting to read new data.)

Producer-consumer: The producer never overwrites the data buffer unless the consumer has already read the current data The consumer never reads the data buffer unless it contains new data. The usual algorithm for producer-consumer uses a single flag bit. The flag bit is set by the producer when data ready to be read, and unset by the consumer once it has read the data. For the sake of this assignment, we only need to model whether the data buffer has been read, rather than modeling the contents of the data. We will use a single bit for this.

Your task is to model this algorithm in Promela, and then verify the above properties about it. It will help to remember that (1) and (3) are safety properties, but (2) is a liveness property. You may use both LTL and in-line assertions where appropriate.

---

This is my first attempt at solving this problem:

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

I created two fundamental processes, a producer and a consumer.

The producer is bound to another process called write by a channel fwrite and the consumer is bound to another process called read by a channel fread. Here, read and write contain read and write pointers.

The consumer is incomplete, I have only sketched the idea I have. I would like to have the reading to happen after the total writing of the channels or the table of the FIFO and that the producer can write N number of information without being satisfied with the size of the FIFO.

Answer 1

Note: from the comments, it looks like the problem you are trying to solve is quite complex and would probably benefit from being broken down into smaller and easier pieces.

---

Piece 01: simple producer/consumer over FIFO + ltl properties

IMHO, this is the preferred approach when dealing with model checking and formal verification: you should abstract away implementation and language dependent features from the system you want to model, and focus over the core aspects of its behaviour.

With this approach in mind, it is pretty-much self-evident that whereas it makes sense to model in Promela active agents such as the Producer and the Consumer as processes, it makes little sense to model the class FIFO of your SystemC code, especially considering that Promela already provides chan which can behave both as a synchronous and asynchronous FIFO queue.

Here, I provide a very basic model of the system with only one producer and one customer, which allows for several simplifications:

/**
 * 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 }

Please notice that I chose to declare fifo as an asynchronous channel with chan fifo = [1], rather than as a synchronous channel with chan fifo = [0], because your mutual exclusion property requires the producer and the consumer not accessing the fifo con-temporarily. In a synchronous fifo, the consumer and the producer always [and only] access the fifo at the exact same time, but there is no race condition because the message is directly handed over from the producer to the consumer.

---

Piece 02: fifo as a process

Now let's put the producer, consumers and ltl properties behind us and focus on how it is possible to model a FIFO queue as a Process.

Again, the focus should be on abstracting the desired behaviour rather than a one-to-one mapping of the original SystemC source code. I will take the liberty to discard the clock input signal and merge all inputs [resp. outputs] into a single wire. Since in your comments you stated that you wanted a synchronous fifo, I will also disallow write-after-write events and assume a fifo of size 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;
}

I chose to make push/pop attempts fail-safe: by design, it's impossible to overwrite or read invalid data.

Putting everything together.

Then one can update the producer and consumer processes to use this fifo process instead of the built-in 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;
}

You should notice that this implementation relies on busy polling, which is not a wise idea from the point of view performance, though it is the easiest approach to model.

An alternative approach would be to use shared variables and mutexes, but this would disrupt the concept of the FIFO as a component with inputs and outputs, which apparently you want to model.

The components can be connected together like this:

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
}

and last, but not least, the ltl properties:

#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

---

Now, I am not exactly sure this approach heads in the direction you wanted to take, so I'll wait for further feedback and in case update my answer.