--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Can the tools be used with intrinsic in customer simulators



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