Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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