--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on February 2012 ---
On Tue, Feb 7, 2012 at 7:18 AM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > The value analysis is not one of the plug-ins that handle multithread > programs, but it is used to analyze the effects of a single thread at a time > by the undistributed Frama-C plug-in for semantic analysis of multithreaded > programs. That plug-in gives a meaning to pthread_create(), amongst other > primitives. As an example, this is the current result of the unreleased plugin Pascal alludes to on Boris Hollas's example [...] [mt] ***** Threads computed. [mt] * Computing live threads and locked mutexes [mt] * threads and mutexes computed [mt] ***** Computing shared variables [mt] Imprecise locations to watch: g [mt] _main_ reads g ? {1} [mt] &thread writes g ? {0} [mt] Possible read/write data races: g: read by _main_ at tests/hollas.c:21, unprotected, // main (tests/hollas.c:17) write by &thread at tests/hollas.c:9, unprotected, // thread1 (tests/hollas.c:9) [mt] Shared memory: g [mt] Mutexes for concurrent accesses: [g] unprotected [mt] ***** Shared variables computed [mt] ******* Analysis performed, 2 iterations g is correctly detected as a shared variable. Since no mutex protects it, a race condition is reported. The plugin is not completely finished, so the values written by thread1 in g are not currently reinjected inside the main thread. Once this is done, the value for g after the call for pthread_create will be \Top. Had g been protected by a mutex, its value would be {0; 1}. Notice that in both cases, the assertion //@ assert g == 1 does not hold, as this depends on the scheduling policy. This would however be correct if pthread_join had been been used instead of sleep. Hope this helps, -- Boris