CBMC Test Threads Writing to Adjacent Data

test_thread_adjacent_data.c

#include <assert.h>
#include <pthread.h>
#include <stdlib.h>

unsigned long data[2];

void *thread0(void *arg)
{
	data[0] = 1;
	return NULL;
}

void *thread1(void *arg)
{
	data[1] = 1;
	return NULL;
}

int main(int argc, char *argv[])
{
	pthread_t t0;
	pthread_t t1;

	if (pthread_create(&t0, NULL, thread0, NULL))
		abort();
	if (pthread_create(&t1, NULL, thread1, NULL))
		abort();
	if (pthread_join(t0, NULL))
		abort();
	if (pthread_join(t1, NULL))
		abort();

	assert(data[0] == 1);
	assert(data[1] == 1);

	return 0;
}

test_thread_adjacent_data.log

CBMC version 5.4 64-bit x86_64 linux
Parsing test_percpu3.c
Converting
Type-checking test_percpu3
Generating GOTO Program
Adding CPROVER library (x86_64)
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Adding SC constraints
size of program expression: 425 steps
no slicing due to threads
Generated 2 VCC(s), 2 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
6259 variables, 17176 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.078s
Building error trace

Counterexample:

State 19  thread 0
----------------------------------------------------
  argv'[2050]=irep("(\"nil\")")[2050] (?)

State 22 file test_percpu3.c line 19 thread 0
----------------------------------------------------
  argc=2050 (00000000000000000000100000000010)

State 23 file test_percpu3.c line 19 thread 0
----------------------------------------------------
  argv=argv' (0000001000000000000000000000000000000000000000000000000000000000)

State 24 file test_percpu3.c line 21 function main thread 0
----------------------------------------------------
  t0=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 25 file test_percpu3.c line 22 function main thread 0
----------------------------------------------------
  t1=0 (0000000000000000000000000000000000000000000000000000000000000000)

State 115 file test_percpu3.c line 9 function thread0 thread 1
----------------------------------------------------
  data[0]=1 (0000000000000000000000000000000000000000000000000000000000000001)

State 127 file test_percpu3.c line 15 function thread1 thread 2
----------------------------------------------------
  data[1]=1 (0000000000000000000000000000000000000000000000000000000000000001)

Violated property:
  file test_percpu3.c line 33 function main
  assertion data[0] == 1
  data[(signed long int)0] == (unsigned long int)1

VERIFICATION FAILED