ВПнМ, примеры задач/Задача 3

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

Версия 17:55, 25 апреля 2009

Задача

Дано:

• исходный текст функции
• свойства корректности

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

Результат:

• текст модели на языке 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;
}

Вывод симулирования

Cкриншот диаграммы состояний

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

Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них.

Имитирование системных вызовов

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

Полезная строка на шелле для обрезания вывода spin

При помощи следующей нехитрой строчки можно ограничить вывод spin десятью строками:

MKTEMP=`mktemp`;\
sed -n 0,/^$(echo $(spin -p task3.pml | tee ${MKTEMP} | grep 'from?' | \ 
head \
| tail -n 1 | cut -d: -f 1) + 1 | bc)\:/p ${MKTEMP} | head -n -1 > log.txt; rm ${MKTEMP}

У выделенного head ключом -n <количество> можно задать другое количество строк для обрезания.