Towards Certified Compilation of RTFM-core Applications
Ref: CISTER-TR-161105 Publication Date: 6 to 9, Sep, 2016
Towards Certified Compilation of RTFM-core Applications
Ref: CISTER-TR-161105 Publication Date: 6 to 9, Sep, 2016Abstract:
Concurrent programming is dominated by thread
based solutions with lock based critical sections. Careful attention
has to be paid to avoid race and deadlock conditions. Real-Time
for The Masses (RTFM) takes an alternative language approach,
introducing tasks and named critical sections (via resources)
natively in the RTFM-core language. RTFM-core programs can
be compiled to native C-code, and efficiently executed onto
single-core platforms under the Stack Resource Policy (SRP)
by the RTFM-kernel. In this paper we formally define the
well-formedness criteria for SRP based resource management,
and develop a certified (formally proven) implementation of
the corresponding compilation from nested critical sections of
the input RTFM-core program to a resulting flat sequence of
primitive operations and scheduling primitives. Moreover we
formalise the properties for resource ceilings under SRP and
develop a certified algorithm for their computation.
The feasibility of the described approach is shown through
the adoption of the Why3 platform, which allows the necessary
verification conditions to be automatically generated and discharged
through a variety of automatic external SMT-solvers
and interactive theorem provers. Moreover, Why3 supports the
extraction of certified Ocaml code for proven implementations
in WhyML. As a proof of concept the certified extracted
development is demonstrated on an example system.
Per Lindgren
Marcus Lindner
David Pereira
Luis Miguel Pinho21st International Conference on Emerging Technologies and Factory Automation (ETFA 2016).
Berlin, Germany.
DOI:10.1109/ETFA.2016.7733551.
Record Date: 21, Nov, 2016