ПРОМЕЛА: Будет ли это примером тупика? - PullRequest
Новая
       58

ПРОМЕЛА: Будет ли это примером тупика?

0 голосов
/ 19 декабря 2018

Будет ли это примером тупика? 

active proctype test(){

     bool one;
     byte x;

     one;
     x = x+11;
}

1 Ответ

0 голосов
/ 19 декабря 2018

ИМХО , №

Следует список необходимых условий для тупика , как показано в Википедии:

тупикСитуация с ресурсом может возникнуть тогда и только тогда, когда в системе одновременно выполняются все следующие условия:

  • Взаимное исключение: Как минимумодин ресурс должен храниться в режиме без общего доступа.В противном случае процессы не будут лишены возможности использовать ресурс при необходимости.Только один процесс может использовать ресурс в любой момент времени.

  • Удержание и ожидание или удержание ресурса: процесс в настоящее время удерживает хотя бы один ресурс и запрашиваетдополнительные ресурсы, которые удерживаются другими процессами.

  • Нет приоритет : ресурс может быть освобожден только добровольно процессом, который его удерживает.

  • Циклическое ожидание: каждый процесс должен ожидать ресурс, который удерживается другим процессом, который, в свою очередь, ожидает, пока первый процесс освободит ресурс,В общем, существует набор ожидающих процессов, P = {P1, P2,…, PN}, так что P1 ожидает ресурс, удерживаемый P2, P2 ожидает ресурс, удерживаемый P3и так далее до тех пор, пока PN не ожидает ресурс, содержащийся в P1.

Эти четыре условия известны как условия Кофмана из их первого описания в статье 1971 года Эдвард Дж. Коффман, мл.

Ваша модель включает в себя процесс, который зависает вечно , но нет общего ресурса , нет другого процесса s удерживает его, нет циклического ожидания и т. д. Другими словами, это просто процесс, которому нечего выполнять в течение бесконечного количества времени,потому что one назначается false по умолчанию, а выражение, оцениваемое как false, всегда блокируется в Promela .

Простой пример взаимоблокировки, взятый из лекции «Спин: Введение», проводимый в Университете Тренто ранееs год, следующий.

file: mutex_simple_flaw2.pml 

bit x, y;
byte cnt;


active proctype A() {
again:
  x = 1;
  y == 0; /* waits for process B to end: if y != 0, the execution of this
             statement is blocked here */
  cnt++;
  /* critical section */
  printf("Process A entered critical section.\n");
  assert(cnt == 1);
  cnt--;

  printf("Process A exited critical section.\n");
  x = 0;
  goto again
}


active proctype B() {
again:
  y = 1;
  x == 0;

  cnt++;
  /* critical section */
  printf("Process B entered critical section.\n");
  assert(cnt == 1);
  cnt--;

  printf("Process B exited critical section.\n");
  y = 0;
  goto again
}

Эта модель заходит в тупик, когда процессы A и B "современно " выполнить инструкции x = 1 и y = 1.

Об этом свидетельствует следующий проверочный поиск, который сигнализирует о существовании недопустимого конечного состояния , которое соответствуеттрассировка выполнения, удовлетворяющая всем условиям Кофмана : 

~$ spin -search -bfs mutex_simple_flaw2.pml

pan:1: invalid end state (at depth 2)
pan: wrote mutex_simple_flaw2.pml.trail

(Spin Version 6.4.8 -- 2 March 2018)
Warning: Search not completed
    + Breadth-First Search
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks            - (disabled by -DSAFETY)
    invalid end states      +

State-vector 20 byte, depth reached 2, errors: 1
        8 states, stored
           8 nominal states (stored-atomic)
        1 states, matched
        9 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
  128.195   total actual memory usage



pan: elapsed time 0 seconds

Следящая за ошибкой трассировка выполнения, найденная Spin, следует: 

~$ spin -t -p -g -l mutex_simple_flaw2.pml

using statement merging
  1:    proc  1 (B:1) mutex_simple_flaw2.pml:24 (state 1)   [y = 1]
        y = 1
  2:    proc  0 (A:1) mutex_simple_flaw2.pml:7 (state 1)    [x = 1]
        x = 1
  3:    proc  0 (A:1) mutex_simple_flaw2.pml:8 (state 2)    [((y==0))]
    transition failed
spin: trail ends after 3 steps
#processes: 2
        x = 1
        y = 1
        cnt = 0
  3:    proc  1 (B:1) mutex_simple_flaw2.pml:25 (state 2)
  3:    proc  0 (A:1) mutex_simple_flaw2.pml:8 (state 2)
2 processes created

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

...