How to find issues related to Data consistency in an Embedded C code base?

Question

Let me explain what I mean by data consistency issue. Take following scenario for example

uint16 x,y;
x=0x01FF;
y=x;

Clearly, these variables are 16 bit but if an 8 bit CPU is used with this code, read or write operations would not be atomic. Thereby an interrupt can occur in between and change the value.This is one situation which MIGHT lead to data inconsistency.

Here's another example,

if(x>7) //x is global variable
{
 switch(x)
        {
           case 8://do something
                   break;
           case 10://do something
                   break;
           default: //do default
        }
}

In the above excerpt code, if an interrupt is changing the value of x from 8 to 5 after the if statement but before the switch statement,we end up in default case, instead of case 8.

Please note, I'm looking for ways to detect such scenarios (but not solutions)

Are there any tools that can detect such issues in Embedded C?

Answer 1

It is possible for a static analysis tool that is context (thread/interrupt) aware to determine the use of shared data, and that such a tool could recognise specific mechanisms to protect such data (or lack thereof).

One such tool is Polyspace Code Prover; it is very expensive and very complex, and does a lot more besides that described above. Specifically to quote (elided) from the whitepaper here:

With abstract interpretation the following program elements are interpreted in new ways:

[...]

• Any global shared data may change at any time in a multitask program, except when protection mechanisms, such as memory locks or critical sections, have been applied

[...]

It may have improved in the long time since I used it, but one issue I had was that it worked on a lock-access-unlock idiom, where you specified to the tool what the lock/unlock calls or macros were. The problem with that is that the C++ project I worked on used a smarter method where a locking object (mutex, scheduler-lock or interrupt disable for example) locked on instantiation (in the constructor) and unlocked in the destructor so that it unlocked automatically when the object went out of scope (a lock by scope idiom). This meant that the unlock was implicit and invisible to Polyspace. It could however at least identify all the shared data.

Another issue with the tool is that you must specify all thread and interrupt entry points for concurrency analysis, and in my case these were private-virtual functions in task and interrupt classes, again making them invisible to Polyspace. This was solved by conditionally making the entry-points public for the abstract analysis only, but meant that the code being tested does not have the exact semantics of the code to be run.

Of course these are non-problems for C code, and in my experience Polyspace is much more successfully applied to C in any case; you are far less likely to be writing code in a style to suit the tool rather than the tool working with your existing code-base.