Промела: Почему этот атомарный блок не эквивалентен оператору присваивания? - PullRequest
Новая
       20

Промела: Почему этот атомарный блок не эквивалентен оператору присваивания?

0 голосов
/ 02 февраля 2019

Я написал следующий код Promela.Этот код моделирует ситуацию, когда два процесса увеличивают общий счетчик.

Я ожидал, что assert в коде должно быть истинным, но SPIN говорит "утверждение нарушено".Как ни странно, когда я заменил блок atomic на count = count + 1, ошибка исчезла.

Почему этот атомарный блок не эквивалентен оператору присваивания? 

byte count = 0;
bool finished[2];

proctype Increment(byte index) {
    atomic {
        byte c = count;
        c = c + 1;
        count = c;
    }
    finished[index] = true;
}

init {
    run Increment(0);
    run Increment(1);

    (finished[0] && finished[1]);
    assert(count == 2);
}

Результат выполнения: 

$ spin -a counter.pml
$ gcc -o pan pan.c
$ ./pan
pan:1: assertion violated (count==2) (at depth 9)
pan: wrote counter.pml.trail

(Spin Version 6.4.6 -- 2 December 2016)
Warning: Search not completed
        + Partial Order Reduction

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        acceptance   cycles     - (not selected)
        invalid end states      +

State-vector 36 byte, depth reached 11, errors: 1
       28 states, stored
        3 states, matched
       31 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.002       equivalent memory usage for states (stored*(State-vector + overhead))
    0.292       actual memory usage for states
  128.000       memory used for hash table (-w24)
    0.534       memory used for DFS stack (-m10000)
  128.730       total actual memory usage



pan: elapsed time 0 seconds
...