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] Worst case path computation

  • Subject: [Frama-c-discuss] Worst case path computation
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Mon, 10 Oct 2011 14:50:08 +0200
  • In-reply-to: <CAOH62Jji2hdhq0AsLcz4T1GjLJ=TjnYEZpRRxFDbOV0bFz5jVQ@mail.gmail.com>
  • References: <CAFaEDLCyERTXG2eUUewW73YM3gSCfYeaEdsSTw4e93RzzTMynw@mail.gmail.com> <CAOH62Jji2hdhq0AsLcz4T1GjLJ=TjnYEZpRRxFDbOV0bFz5jVQ@mail.gmail.com>
Hi Pascal,

thank you for reacting so swiftly!

First, I'd like to say this question is relative to a very concrete
problem of a project I am working on: being able to statically
estimate the maximal execution time an embedded software will take in
a given configuration, to verify it is able to hold it's real time
requirement, and if not, of how much we are off. The chipset producer
does not provide a tool to do that, so I am studying the possibility
to implement it with open-source software.

> Since you are interested in this question, I do not need to tell you
> that it is difficult to work only at the source level for worst case
> execution time verification.

One obviously needs information from the result of the compilation,
since concrete execution time can only be computed at the assembly
instruction level.

Let me explain what I have in mind as a possible solution
architecture. I would very much appreciate your feedback on it.

1. Be able to link disassembles binaries with original source code, so
that each instruction in the C source can be joined to the one or
several corresponding assembly instructions
(When using GNU tools, objdump can do that in a parsable form).
2. Generates a parsable list of the C instructions executed in worst case
3. Join both set of information so that to generate the set of
assembly instructions executed in WCEP.
4. Compute the WCE Time by using the information from the
processor/board architecture (processor cycles per instruction,
working frequency of the processor)

(1) can be done by "objdump" when using GNU toolchain.
(2) is where where Frama-C could enter the play.
(3) and (4) could be done by ad-hoc scripts, architecture dependant

IYO, does that make sense?

> Please read:
> http://blog.frama-c.com/index.php?post/2011/10/10/Execution-path-dependencies

Allow me some time to digest it :)

> Using -experimental-path-deps -deps, you can obtain a list of
> memory locations that influence the execution path of your function.
>
> but because it doesn't account for the various levels of
> data caches).

One can nonetherless _measure_ the cost of cache-misses, and use it as
a base for estimating worst-case computation.
In this peculiar case, the processor is a very simple 16 bits
processor whose architecture does not contain caches, so as far as I
can tell execution time per assembly instruction is deterministic.

> This is probably not going to be satisfactory as such, but I hope
> it gives an idea of what Frama-C can offer.

Looks better than I first thought.

It seems you already put some thought on this use-case? Do you find it
generally interesting for Frama-C?
In any case, it seems that there is currently no open-source software
that have this capacity. Unless I have overlooked something?

Thanks,
Sylvain