конвертировать программу fifo systemC в язык PROMELA с защищенными свойствами и активностью жизнедеятельности

Question

, пожалуйста, я являюсь гигантом домена tihs, как я могу преобразовать классический пример FIFO, написанный в коде systemC, на язык PROMELA со свойствами в LTL , удовлетворяющий следующим трем свойствам:

Взаимное исключение. Процессы производителя и потребителя никогда не получают доступ к общему буферу одновременно.

Non-starvation: Потребитель обращается к буферу бесконечно часто. (Вы можете предположить, что производитель никогда не исчерпывает данных на поставку, и потребитель никогда не прекращает попытки читать новые данные.)

Производитель-Потребитель: Производитель никогда не перезаписывает буфер данных, если потребитель не прочитанной текущие данные Пользователь никогда не читает буфер данных, если он не содержит новые данные. Обычный алгоритм для производителя-потребителя использует бит одного флага. Бит флага устанавливается производителем, когда данные готовы к чтению, и отменяется потребителем после его считывания. Для этого задания нам нужно только определить, был ли прочитан буфер данных, а не , моделирующий содержимое данных. Для этого мы будем использовать один бит.

Ваша задача - смоделировать этот алгоритм в 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 и потребитель связан с другим процессом называется чтения каналом Fread. Здесь читать и написать письмо и написать письмо указатели.

потребитель неполный, я только набросал идею, которую я имею. Я хотел бы иметь чтение произойдет после общего написания каналов или таблицы FIFO и что производителя может написать N количества информации, не будучи удовлетворен размером от FIFO.

Answer 1

Примечание: от комментариев, это выглядит как проблема, которую вы пытаетесь решить это довольно сложный и, вероятно, выиграют от были сломаны в меньше и легче штук.

---

Часть 01: простой производитель/потребитель над ФИФО + Ltl свойствами

ИМХИ, это предпочтительный подход при работе с модели проверки и формальной проверкой: вы должен абстрактная реализация и зависимая от языка функции от системы вы хочу модель, и сосредоточиться на основных аспектахповедение.

С этим подход в виду, что это довольно-много самоочевидным, что в то время как это имеет смысл моделировать в Promela активных агентов, таких как Producer и Потребителя как процессы, это делает мало смысл моделировать класса FIFO вашего SystemC кода, особенно если учесть, что Promela уже обеспечивает чан который может вести себя и как синхронный и асинхронныйFIFO очередь.

Здесь я приведу очень основную модель системы только один производитель и один клиента, что позволяет в течение нескольких упрощений:

/** 
* 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], потому что ваш взаимного исключения собственности требует производителя и потребитель не имеет доступа к ФИФО кон-временно. В синхронных ФИФО, в потребителя и производителя всегда [и только] доступ к ФИФО в то же самое время, но нет условия гонки, так как сообщение непосредственно передано от производителя до потребитель.

---

Часть 02: ФИФО как процесс

Теперь давайте поставить производителя, потребителей и свойства лт позади нас и сосредоточиться на том, как можно смоделировать FIFO очередь как Процесс.

Опять же, фокус должен быть на абстрагируясь желаемое поведение, а не отображение а один-к-одному оригинального SystemC исходного кода. Я позволю отказаться от входного сигнала и слить все входы [соотв. выходы] в один провод . Поскольку в комментариях Вы сказали, что вы хотели синхроннойФИФО, я также запретить записи после записи события и предполагаю ФИФО размера .

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

Вы должны заметить, что эта реализация опирается на занятый опрос, который не является мудрый идея с точки зрения o f вид производительность, хотя это самый простой подход к модели.

Альтернативный подход заключается в использовании общих переменных и мьютексы, но это нарушило бы понятие 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 
} 

и последнее, но не менее важно, свойства лт:

#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 

---

Теперь, я не совсем уверен, этот подход идет в том направлении, в котором вы хотели принять, поэтому я буду ждать дополнительной обратной связи и в случае обновления моего ответа.