CBMC обнаружил ошибку подтверждения в моей программе Pthreads, это правильно?

Question

Я использую CBMC для проверки моей программы Pthreads, она обнаружила некоторые ошибки подтверждения, которые, я думаю, не существовали. Ошибка возникает только тогда, когда я запускаю два потока одновременно. То есть, когда я помещаю один из операторов, который вызывает функцию потока (func или же func1) в комментариях, CBMC может проверить его успешность. Есть ли конфликт в присваивании массива a а также b?

int a[4], b[4];

static void * func(void * me)
{
  int i;
  for(i=0; i<2; i++){
    a[i] = b[i] = i;
    assert( a[i] == i ); //failed
  }
  return ((void *) 0);
}

static void * func1(void * me)
{
  int i;
  for(i=2; i<4; i++){
    a[i] = b[i] = i;
    assert( a[i] == i ); //failed
  } 
  return ((void *) 0);
}

int main(){
  pthread_t thr1;
  pthread_create(&thr1, NULL, func1, (void *)0);
  (*func)(0);
  pthread_join(thr1,NULL);

  return 0;
}

Выход CBMC выглядит следующим образом:

Violated property:
  file pthreads4.c line 25 function func1
  assertion a[i] == i
  a[(signed long int)i] == i

VERIFICATION FAILED

Answer 1

Это выглядит как ложный позитив со стороны CBMC.

Мы видим, что основной поток будет изменять a[0], a[1], b[0], а также b[1],

Нить thr1 модифицирует a[2], a[3], b[2], а также b[3],

На самом деле нет никакого перекрывающегося доступа между потоками, и поэтому эта программа должна вести себя так, как будто она запускается последовательно.

Трассировка ошибок, создаваемая CBMC, также не имеет большого смысла:

Counterexample:

State 19 file test.c line 27 function main thread 0
----------------------------------------------------
  thr1=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

State 22 file test.c line 28 function main thread 0
----------------------------------------------------
  thread=&thr1!0@1 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 23 file test.c line 28 function main thread 0
----------------------------------------------------
  attr=((union pthread_attr_t { char __size[56l]; signed long int __align; } *)NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 24 file test.c line 28 function main thread 0
----------------------------------------------------
  start_routine=func1 (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 25 file test.c line 28 function main thread 0
----------------------------------------------------
  arg=NULL (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 47 file test.c line 29 function main thread 0
----------------------------------------------------
  me=NULL (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 48 file test.c line 8 function func thread 0
----------------------------------------------------
  i=0 (00000000 00000000 00000000 00000000)

State 49 file test.c line 9 function func thread 0
----------------------------------------------------
  i=0 (00000000 00000000 00000000 00000000)

State 51 file test.c line 10 function func thread 0
----------------------------------------------------
  b[0l]=0 (00000000 00000000 00000000 00000000)

State 52 file test.c line 10 function func thread 0
----------------------------------------------------
  a[0l]=0 (00000000 00000000 00000000 00000000)

State 54 file test.c line 9 function func thread 0
----------------------------------------------------
  i=1 (00000000 00000000 00000000 00000001)

State 57 file test.c line 10 function func thread 0
----------------------------------------------------
  b[1l]=1 (00000000 00000000 00000000 00000001)

State 58 file test.c line 20 function func1 thread 1
----------------------------------------------------
  b[2l]=2 (00000000 00000000 00000000 00000010)

State 59 file test.c line 20 function func1 thread 1
----------------------------------------------------
  a[2l]=2 (00000000 00000000 00000000 00000010)

State 61 file test.c line 19 function func1 thread 1
----------------------------------------------------
  i=3 (00000000 00000000 00000000 00000011)

State 64 file test.c line 10 function func thread 0
----------------------------------------------------
  a[1l]=0 (00000000 00000000 00000000 00000000)

Violated property:
  file test.c line 11 function func
  assertion a[i] == i
  a[(signed long int)i] == i


VERIFICATION FAILED

Этот встречный пример утверждает, что a[1] == 0, Тем не менее, состояние 64 показывает 0 быть назначенным на a[1] хотя последнее записанное значение b[1] является 1 в состоянии 57.