Simple Concurrency Analysis Plugin for Frama-C
==============================================

Introduction
------------

This project is an extension to the [Frama-C](http://frama-c.com)
software analyser for C, to provide a simple way to discover potential
concurrency problems in interrupt-driven C code. Command-line and GUI
versions are available.

This plugin was developed by [Adelard LLP](http://www.adelard.com) as
part of the FEAST research project, conducted on behalf of CINIF (the
Control and Instrumentation Nuclear Industry Forum).

### Goals ###

The Simple Concurrency Analysis Plugin is aimed at small, embedded
systems, typically without an operating system. These systems commonly
use interrupts to manage hardware and other interactions, and use
shared variables to communicate between the main thread and the
interrupt service routines. As interrupts can occur at any time, these
shared variables can be corrupted.

To help discover potential sources of problems, this plugin does three things:

1. *Help identify interrupt service routines.* These may not be
   obvious from the C source. The plugin identifies all functions
   which are not called from elsewhere in code as possible interrupt
   service routines.
2. *Identify shared variables.* For every combination of the main
   thread and an interrupt service routine, the plugin identifies
   variables which may be accessed by both. These are the global
   variables and other variables with static storage duration (e.g.,
   function local variables declared `static`).
3. *Identify where the variables are accessed.* For a given variable,
   the plugin lists all reads and writes to that variable, reachable
   from the main and chosen interrupt threads.

### Caveats ###

To keep the plugin simple and fast, it does not attempt to process
pointers. This means that variable accesses via pointers are not
identified by this plugin, and calls to function pointers are not
followed. See issue #1.

For programs where this is critical, the
[Mthread](http://frama-c.com/mthread.html) plugin provides a much more
advanced analysis.

The size information reported by `-accesses-for` (see below) is
dependent on Frama-C's `-machdep` option being set correctly.

Installation
------------

This plugin is compatible with Frama-C Neon (20140301). After
installing Frama-C, checkout this repository and run `make` and `make
install`.


Command Line Usage
------------------

The command line version provides three commands. Without any
additional flags, the plugin lists possible entry points for the code
(i.e., functions with no callers):

    $ frama-c -concur test.c test2.c
    [kernel] preprocessing with "gcc -C -E -I.  test.c"
    [kernel] preprocessing with "gcc -C -E -I.  test2.c"
    [concur] Starting concurrency
    [concur] ---Entry points---
    [concur] an_interrupt
    [concur] main
    [concur] an_interrupt2

The `-var-overlap` flag shows the variables accessed by combinations
of threads, together with their scope:

    $ frama-c -concur -var-overlap test.c test2.c
    [kernel] preprocessing with "gcc -C -E -I.  test.c"
    [kernel] preprocessing with "gcc -C -E -I.  test2.c"
    [concur] Starting concurrency
    [concur] ---Entry points---
    [concur] an_interrupt
    [concur] main
    [concur] an_interrupt2
    [concur] -----------------
    [concur] Variables shared by main and an_interrupt:
    [concur] global_val1 (global)
    [concur] global_val4 (global)
    [concur] -----------------
    [concur] Variables shared by main and an_interrupt2:
    [concur] global_val2 (global)
    [concur] global_val1 (global)
    [concur] global_val4 (global)

The `-accesses-for` flag shows where each variable is accessed, and
provides some additional information on the variable's size and type,
since this may make a difference to its interrupt-safety on some
architectures:

    $ frama-c -concur -accesses-for global_val4 test.c test2.c
    [kernel] preprocessing with "gcc -C -E -I.  test.c"
    [kernel] preprocessing with "gcc -C -E -I.  test2.c"
    [concur] Starting concurrency
    [concur] ---Entry points---
    [concur] an_interrupt
    [concur] main
    [concur] an_interrupt2
    [concur] ------------------
    [concur] Declaration: int global_val4[4]
    [concur] Basic size in bytes: 16
    [concur] Basic size in bits: 128
    [concur] ------------------
    [concur] Accesses to global_val4 from an_interrupt:
    [concur] write at test.c:26 in an_interrupt
    [concur] ------------------
    [concur] Accesses to global_val4 from main:
    [concur] write at test.c:13 in main
    [concur] write at test.c:14 in main
    [concur] read at test.c:17 in main
    [concur] ------------------
    [concur] Accesses to global_val4 from an_interrupt2:
    [concur] read at test2.c:12 in an_interrupt2


GUI Usage
---------

Once the plugin is installed, it adds an additional set of options to
the left-hand side of the screen. From here, you can choose a main
thread and an interrupt routine. This will populate the list of shared
variables; selecting a shared variable will highlight it in the source
tree.

*Further GUI examples to follow*