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

Dear Sylvain,

Your goal seems very close to that of the CerCo project [1], which
aims at building a formally verified C compiler that adds cost
annotations in the source code. These annotations are added at
specific program points so that every piece of code that executes in
constant time is covered. They have the form of an update of the
so-called cost variable by an amount computed at the assembly level.
The technique mainly relies on a mapping between some specific control
points of the source and object code [2].

For now, the compiler targets the 8051, a micro-controller that has
some common properties with the one you described: it is used in
embedded software and an accurate time prediction per assembly
instruction is possible.

One particular part of the project is to design a Frama-C plug-in that
first runs the CerCo compiler on a source file, and then, for each
function, synthesizes the annotations added by CerCo into an ACSL
specification that represents a WCET of the function. The result can
be fed to WP or Jessie for further trust.

Our first experiments are encouraging. The plug-in is able to
statically compute a WCET for a good range of functions (even in the
presence of nested loops), though we are still working towards better
support through more generic techniques (such as abstract
interpretation).

The sources of the project are not publicly available yet, but we will
make an announcement on Frama-C's mailing list as soon as they will
be.

Cheers,

Nicolas

[1] http://cerco.cs.unibo.it/
[2] Certifying cost annotations in compilers. Roberto M. Amadio,
Nicolas Ayache, Yann R?gis-Gianas and Ronan Saillard. Technical
Report, Universit? Paris Diderot (Paris 7)


On Mon, Oct 10, 2011 at 2:50 PM, sylvain nahas
<sylvain.nahas at googlemail.com> wrote:
> 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
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>