CBMC在我的P螺纹程序中检测到一个断言错误，是正确的吗？

Question

我使用CBMC来验证我的线程程序，它检测到了一些我认为不存在的断言错误。只有当我同时运行这两个线程时，才会发生错误。也就是说，当我将调用线程函数(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]的最后一个写入值是状态57中的1。