3

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

1 回答 1

1

这似乎是 CBMC 的误报。

我们可以看到主线程会修改a[0], a[1], b[0], 和b[1].

Threadthr1修改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. 但是，即使最后写入的值处于状态 57 中，状态 64 也显示0被分配给。a[1]b[1]1

于 2018-10-22T06:33:41.497 回答