时间戳

首页 > 解决方案 > Promela: Why is not this atomic block equivalent to an assignment statement?

promela - Promela: Why is not this atomic block equivalent to an assignment statement?

问题描述

I wrote following Promela code. This code simulates the situation where two processes increment a shared counter.

I expected the assert in the code must be true, but SPIN says "assertion violated". Strangely, when I replaced the atomic block with count = count + 1, the error has been gone.

Why is not this atomic block equivalent to an assignment statement?

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);
}

Execution result:

$ 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

标签： promelaspin

解决方案

This is a known bug, it has been fixed (at least) since version 6.4.8 of Spin.

Keep the tool updated.

Note: added answer as requested by @Brishna Batool.

推荐阅读