ВПнМ, примеры задач/Задача 3
Материал из eSyr's wiki.
(Различия между версиями)
(→Пояснения) |
м (→Имитирование системных вызовов) |
||
| Строка 234: | Строка 234: | ||
Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них. | Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них. | ||
| - | + | === Имитирование системных вызовов === | |
Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения. | Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения. | ||
Версия 22:23, 25 апреля 2008
Содержание |
Задача
Дано:
- исходный текст функции
- свойства корректности
Требуется построить корректную модель функции, адекватную заданному свойству корректности. Требуется построить модель с двумя процессами: ядром, отвечающим на эти системные вызовы; функцией, работающей в цикле. Системные вызовы и ответ на них моделируются посылкой сообщения ядру и приёмом сообщения от ядра соответственно.
Результат:
- текст модели на языке Promela
- скриншот диаграммы состояний, полученной в результате моделирования (первые 40 шагов)
- вывод моделирования (первые 40 шагов)
Вариант 1
Исходный текст функции
PRIVATE int DspVersion[2];
PRIVATE int dsp_init()
{
int i, s;
if(dsp_reset () != OK) {
dprint("sb16: No SoundBlaster card detected\n");
return -1;
}
DspVersion[0] = DspVersion[1] = 0;
dsp_command(DSP_GET_VERSION); /* Get DSP version bytes */
for(i = 1000; i; i--) {
if(sb16_inb(DSP_DATA_AVL) & 0x80) {
if(DspVersion[0] == 0) {
DspVersion[0] = sb16_inb(DSP_READ);
} else {
DspVersion[1] = sb16_inb(DSP_READ);
break;
}
}
}
if(DspVersion[0] < 4) {
dprint("sb16: No SoundBlaster 16 compatible card detected\n");
return -1;
}
dprint("sb16: SoundBlaster DSP version %d.%d detected\n", DspVersion[0], DspVersion[1]);
/* set SB to use our IRQ and DMA channels */
mixer_set(MIXER_SET_IRQ, (1 << (SB_IRQ / 2 - 1)));
mixer_set(MIXER_SET_DMA, (1 << SB_DMA_8 | 1 << SB_DMA_16));
/* register interrupt vector and enable irq */
if ((s=sys_irqsetpolicy(SB_IRQ, IRQ_REENABLE, &irq_hook_id )) != OK)
panic("SB16DSP", "Couldn't set IRQ policy", s);
if ((s=sys_irqenable(&irq_hook_id)) != OK)
panic("SB16DSP", "Couldn't enable IRQ", s);
DspAvail = 1;
return OK;
}
Свойства корректности
Модель должна быть адекватной для проверки спецификации: всегда при вызове sys_irqenable верно DspVersion[0] < 4
Решение
Модель
#define OK 0
#define NOT_OK 1
#define SYS_IRQPOLICY 1
#define SYS_IRQENABLE 2
int DspVersion[2];
chan to_kernel_channel = [0] of {byte};
chan from_kernel_channel = [0] of {byte};
active proctype kernel()
{
int msg;
do
:: to_kernel_channel?msg ->
{
if
:: (msg == SYS_IRQPOLICY) ->
{
if
:: from_kernel_channel!OK;
:: from_kernel_channel!NOT_OK;
fi;
}
:: (msg == SYS_IRQENABLE) ->
{
if
:: from_kernel_channel!OK;
:: from_kernel_channel!NOT_OK;
fi;
}
:: (msg == SYS_END) -> break;
:: else -> skip;
fi;
}
od;
}
active proctype dsp_init()
{
do
::
byte result;
DspVersion[0] = 0;
DspVersion[1] = 0;
if
:: DspVersion[0] = 0;
:: DspVersion[0] = 1;
:: DspVersion[0] = 5;
fi;
if
:: DspVersion[1] = 0;
:: DspVersion[1] = 1;
fi;
if :: (DspVersion[0] < 4) ->
{
goto return;
}
:: else -> skip;
fi;
/* sys_irqsetpolicy(SB_IRQ, IRQ_REENABLE, &irq_hook_id); */
to_kernel_channel!SYS_IRQPOLICY;
from_kernel_channel?result;
if
:: (result != OK) ->
{
goto return;
}
:: else -> skip;
fi;
/* sys_irqenable(&irq_hook_id) */
to_kernel_channel!SYS_IRQENABLE;
from_kernel_channel?result;
if :: (result != OK) ->
{
goto return;
}
:: else -> skip;
fi;
return:
skip;
od;
}
Вывод симулирования
% spin -p -u40 model.pml
spin: line 34 "model.pml", Error: undeclared variable: SYS_END saw '')' = '41''
Starting kernel with pid 0
0: proc - (:root:) creates proc 0 (kernel)
Starting dsp_init with pid 1
0: proc - (:root:) creates proc 1 (dsp_init)
1: proc 1 (dsp_init) line 43 "model.pml" (state 38) [DspVersion[0] = 0]
2: proc 1 (dsp_init) line 48 "model.pml" (state 2) [DspVersion[1] = 0]
3: proc 1 (dsp_init) line 50 "model.pml" (state 6) [DspVersion[0] = 0]
4: proc 1 (dsp_init) line 56 "model.pml" (state 7) [.(goto)]
5: proc 1 (dsp_init) line 56 "model.pml" (state 10) [DspVersion[1] = 0]
6: proc 1 (dsp_init) line 61 "model.pml" (state 11) [.(goto)]
7: proc 1 (dsp_init) line 61 "model.pml" (state 17) [((DspVersion[0]<4))]
8: proc 1 (dsp_init) line 64 "model.pml" (state 14) [goto return]
9: proc 1 (dsp_init) line 92 "model.pml" (state 37) [(1)]
10: proc 1 (dsp_init) line 94 "model.pml" (state 39) [.(goto)]
11: proc 1 (dsp_init) line 43 "model.pml" (state 38) [DspVersion[0] = 0]
12: proc 1 (dsp_init) line 48 "model.pml" (state 2) [DspVersion[1] = 0]
13: proc 1 (dsp_init) line 50 "model.pml" (state 6) [DspVersion[0] = 1]
14: proc 1 (dsp_init) line 56 "model.pml" (state 7) [.(goto)]
15: proc 1 (dsp_init) line 56 "model.pml" (state 10) [DspVersion[1] = 0]
16: proc 1 (dsp_init) line 61 "model.pml" (state 11) [.(goto)]
17: proc 1 (dsp_init) line 61 "model.pml" (state 17) [((DspVersion[0]<4))]
18: proc 1 (dsp_init) line 64 "model.pml" (state 14) [goto return]
19: proc 1 (dsp_init) line 92 "model.pml" (state 37) [(1)]
20: proc 1 (dsp_init) line 94 "model.pml" (state 39) [.(goto)]
21: proc 1 (dsp_init) line 43 "model.pml" (state 38) [DspVersion[0] = 0]
22: proc 1 (dsp_init) line 48 "model.pml" (state 2) [DspVersion[1] = 0]
23: proc 1 (dsp_init) line 50 "model.pml" (state 6) [DspVersion[0] = 1]
24: proc 1 (dsp_init) line 56 "model.pml" (state 7) [.(goto)]
25: proc 1 (dsp_init) line 56 "model.pml" (state 10) [DspVersion[1] = 0]
26: proc 1 (dsp_init) line 61 "model.pml" (state 11) [.(goto)]
27: proc 1 (dsp_init) line 61 "model.pml" (state 17) [((DspVersion[0]<4))]
28: proc 1 (dsp_init) line 64 "model.pml" (state 14) [goto return]
29: proc 1 (dsp_init) line 92 "model.pml" (state 37) [(1)]
30: proc 1 (dsp_init) line 94 "model.pml" (state 39) [.(goto)]
31: proc 1 (dsp_init) line 43 "model.pml" (state 38) [DspVersion[0] = 0]
32: proc 1 (dsp_init) line 48 "model.pml" (state 2) [DspVersion[1] = 0]
33: proc 1 (dsp_init) line 50 "model.pml" (state 6) [DspVersion[0] = 5]
34: proc 1 (dsp_init) line 56 "model.pml" (state 7) [.(goto)]
35: proc 1 (dsp_init) line 56 "model.pml" (state 10) [DspVersion[1] = 1]
36: proc 1 (dsp_init) line 61 "model.pml" (state 11) [.(goto)]
37: proc 1 (dsp_init) line 61 "model.pml" (state 17) [else]
38: proc 1 (dsp_init) line 65 "model.pml" (state 16) [(1)]
39: proc 1 (dsp_init) line 69 "model.pml" (state 18) [.(goto)]
40: proc 1 (dsp_init) line 69 "model.pml" (state 19) [to_kernel_channel!1]
40: proc 0 (kernel) line 17 "model.pml" (state 1) [to_kernel_channel?msg]
-------------
depth-limit (-u40 steps) reached
#processes: 2
DspVersion[0] = 5
DspVersion[1] = 1
40: proc 1 (dsp_init) line 70 "model.pml" (state 20)
40: proc 0 (kernel) line 19 "model.pml" (state 18)
2 processes created
Пояснения
Абстрагирование
В модели необходимо абстрагироваться ото всего, что не влияет на спецификацию. При этом надо учитывать, что, на первый взгляд посторонние переменные могут значимо влиять на поток управления и при их абстрагировании корректность и адекватность модели могут нарушаться.
Недетерминизм
Если необходимо проверить все возможные варианты, индуцированные различными значениями переменных, надо выделить различимые множества значений этих переменных, выбрать по одному значению из каждого множества (допустим в результате выбрали числа i1, i2, i3) и записать нечто следующее:
if :: var = i1; :: var = i2; :: var = i3; fi;
Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них.
Имитирование системных вызовов
Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения.
