how to use thread_local clause when a function will be called more than once

Jun 2, 2011 at 1:14 AM

struct GS
	int a;
	int b;

struct GS g[10];
struct GS ga[4];

void write_fun(int idx)
	requires (idx >= 0 && idx < 4)
	requires (thread_local(&g[idx]))
	ga[idx].a = g[idx].b;
	ga[idx].b = g[idx].a;

void call_write(void)
	requires(is_thread_local_array(g, 10))	
	writes(array_range(ga, 4))

The VCC reports that:

Error    1    Call 'write_fun(1)' did not verify. 
Error    2    (related information) Precondition: '_vcc_thread_local2(&g[idx])'.   
Error    3    Call 'write_fun(2)' did not verify.   
Error    4    (related information) Precondition: '_vcc_thread_local2(&g[idx])'.   
Error    5    Call 'write_fun(3)' did not verify.   
Error    6    (related information) Precondition: '_vcc_thread_local2(&g[idx])'.   

It seems that in the first function, the "thread_local" pre-condition in function "write_fun" is valid. But when it is called again, the pre-condition is violated.

Jun 7, 2011 at 9:22 PM

It is the same issue you had in the other thread: you need to let the caller know that the modifications write_fun does to the memory do not change the fact that the memory location is thread local. Try replacing the "requires" inm requires(thread_local(...))" with a "maintains(thread_local(...))".

As a side note, you probably want to use mutable() instead of thread_local, as thread locality is much harder to keep track of in general, and especially through function calls.