CBMC 在我的 Pthreads 程序中检测到一个断言错误，是否正确？答案

【问题标题】：CBMC detected an assert error in my Pthreads program, is it correct?CBMC 在我的 Pthreads 程序中检测到一个断言错误，是否正确？
【发布时间】：2018-10-22 14:33:41
【问题描述】：

我使用 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

【问题讨论】：

标签： c pthreads cbmc

【解决方案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] 的值是状态 57 中的 1。

【讨论】：