Конвертировать программу fifo systemC в язык PROMELA со свойствами безопасности и живучести
Пожалуйста, я большой специалист в этой области. Как я могу преобразовать классический пример FIFO, написанный на коде systemC, в язык PROMELA со свойствами в LTL, удовлетворяющих следующим трем свойствам:
Взаимное исключение: процессы производителя и потребителя никогда не обращаются к совместно используемому буферу одновременно.
Неголодание: потребитель обращается к буферу бесконечно часто. (Вы можете предположить, что у производителя никогда не хватает данных для поставки, и потребитель никогда не прекращает попытки прочитать новые данные.)
Производитель-потребитель: производитель никогда не перезаписывает буфер данных, если потребитель уже не прочитал текущие данные. Потребитель никогда не читает буфер данных, если он не содержит новые данные. Обычный алгоритм для производителя-потребителя использует бит одного флага. Бит флага устанавливается производителем, когда данные готовы для чтения, и сбрасывается потребителем, как только он прочитает данные. Для этого назначения нам нужно только смоделировать, был ли считан буфер данных, а не моделировать содержимое данных. Мы будем использовать один бит для этого.
Ваша задача - смоделировать этот алгоритм в 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, а потребитель связан с другим процессом, который называется чтением канального фреда. Здесь чтение и запись содержат указатели чтения и записи.
Потребитель неполон, я только набросал идею, которая у меня есть. Я хотел бы, чтобы чтение происходило после полной записи каналов или таблицы FIFO, и чтобы продюсер мог записать N номеров информации, не будучи удовлетворенным размером FIFO.
1 ответ
Примечание. Судя по комментариям, проблема, которую вы пытаетесь решить, достаточно сложна и, вероятно, будет полезна , если разбить ее на более мелкие и простые части.
Часть 01: простой производитель / потребитель по свойствам FIFO + ltl
ИМХО, это предпочтительный подход при проверке модели и формальной проверке: вы должны абстрагироваться от реализации и зависящих от языка функций от системы, которую хотите моделировать, и сосредоточиться на основных аспектах ее поведения.
Учитывая этот подход, очевидно, что хотя имеет смысл моделировать в Promela активные агенты, такие как Producer и Consumer, как процессы, не имеет особого смысла моделировать класс FIFO вашего кода SystemC, особенно учитывая, что Promela уже предоставляет chan, которая может вести себя как синхронная и асинхронная очередь 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] потому что ваше свойство взаимного исключения требует от производителя и потребителя одновременного доступа к fifo. В синхронном fifo потребитель и производитель всегда [и только] получают доступ к fifo в одно и то же время, но условия гонки отсутствуют, поскольку сообщение напрямую передается от производителя к потребителю.
Часть 02: fifo как процесс
Теперь давайте оставим производителя, потребителей и свойства ltl позади себя и сосредоточимся на том, как можно смоделировать очередь FIFO как процесс.
Опять же, основное внимание следует уделять абстракции желаемого поведения, а не индивидуальному отображению исходного исходного кода SystemC. Я позволю себе отказаться от входного сигнала часов и объединить все входы [соотв. выходы ] в один провод. Так как в ваших комментариях вы указали, что хотите синхронный fifo, я также запрещаю события записи после записи и предполагаю, что 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
Сейчас я не совсем уверен, что этот подход движется в том направлении, в котором вы хотели пойти, поэтому я буду ждать дальнейших отзывов и в случае обновления моего ответа.