Редактирование: ВПнМ, примеры задач/Задача 3

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

== Задача ==
'''Дано:'''
* исходный текст функции
* свойства корректности

'''Требуется''' построить корректную модель функции, адекватную заданному свойству корректности. Требуется построить модель с двумя процессами: ядром, отвечающим на эти системные вызовы; функцией, работающей в цикле. Системные вызовы и ответ на них моделируются посылкой сообщения ядру и приёмом сообщения от ядра соответственно.

'''Результат:'''
* текст модели на языке Promela
* скриншот диаграммы состояний, полученной в результате моделирования (первые 40 шагов)
* вывод моделирования (первые 40 шагов)

== Вариант 1 ==

=== Исходный текст функции ===
<pre>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;
}</pre>

=== Свойства корректности ===
Модель должна быть адекватной для проверки спецификации: всегда при вызове sys_irqenable верно DspVersion[0] < 4

=== Решение ===
<pre>#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;
}</pre>

=== Вывод симулирования ===
[[Изображение:Screenshot-Sequence Chart.png|thumb|Cкриншот диаграммы состояний]]

<pre>% 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</pre>

=== Пояснения ===

==== Абстрагирование ====
В модели необходимо абстрагироваться ото всего, что не влияет на спецификацию. При этом надо учитывать, что, на первый взгляд посторонние переменные могут значимо влиять на поток управления и при их абстрагировании корректность и адекватность модели могут нарушаться.

==== Недетерминизм ====
Если необходимо проверить все возможные варианты, индуцированные различными значениями переменных, надо выделить различимые множества значений этих переменных, выбрать по одному значению из каждого множества (допустим в результате выбрали числа i1, i2, i3) и записать нечто следующее:
 if
   :: var = i1;
   :: var = i2;
   :: var = i3;
 fi;
Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них.

==== Имитирование системных вызовов ====
Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения.

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Шаблон:Курс ВПнМ

Получено с http://esyr.org/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_%D0%BF%D1%80%D0%B8%D0%BC%D0%B5%D1%80%D1%8B_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_3

Редактирование: ВПнМ, примеры задач/Задача 3

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 64: / Строка 64: @@
 === Решение ===
-==== Модель ====
 <pre>#define OK 0
 #define NOT_OK 1
@@ Строка 161: / Строка 159: @@
 }</pre>
-==== Вывод симулирования ====
+=== Вывод симулирования ===
 [[Изображение:Screenshot-Sequence Chart.png|thumb|Cкриншот диаграммы состояний]]
@@ Строка 220: / Строка 218: @@
 processes created</pre>
-== Пояснения ==
+=== Пояснения ===
-=== Абстрагирование ===
+==== Абстрагирование ====
 В модели необходимо абстрагироваться ото всего, что не влияет на спецификацию. При этом надо учитывать, что, на первый взгляд посторонние переменные могут значимо влиять на поток управления и при их абстрагировании корректность и адекватность модели могут нарушаться.
-=== Недетерминизм ===
+==== Недетерминизм ====
 Если необходимо проверить все возможные варианты, индуцированные различными значениями переменных, надо выделить различимые множества значений этих переменных, выбрать по одному значению из каждого множества (допустим в результате выбрали числа i1, i2, i3) и записать нечто следующее:
  if
@@ Строка 234: / Строка 232: @@
 Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них.
-=== Имитирование системных вызовов ===
+==== Имитирование системных вызовов ====
 Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения.
-== Полезная строка на шелле для обрезания вывода spin ==
-При помощи следующей нехитрой строчки можно ограничить вывод spin десятью пересылками:
- MKTEMP=`mktemp`;\
- sed -n 0,/^$(echo $(spin -p task3.pml | tee ${MKTEMP} | grep 'from?' | \
- head -n '''10'''\
- | tail -n 1 | cut -d: -f 1) + 1 | bc)\:/p ${MKTEMP} | head -n -1 > log.txt; rm ${MKTEMP}
-У выделенного head ключом -n <количество> можно задать другое количество строк для обрезания.
 <!-- TBD -->
 {{Курс ВПнМ}}