Towards Certified Compilation of RTFM-core Applications

• Concurrent programming is dominated by threadbased solutions with lock based critical sections. Careful attentionhas to be paid to avoid race and deadlock conditions. Real-Timefor 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 canbe compiled to native C-code, and efficiently executed ontosingle-core platforms under the Stack Resource Policy (SRP)by the RTFM-kernel. In this paper we formally define thewell-formedness criteria for SRP based resource management,and develop a certified (formally proven) implementation ofthe corresponding compilation from nested critical sections ofthe input RTFM-core program to a resulting flat sequence ofprimitive operations and scheduling primitives. Moreover weformalise the properties for resource ceilings under SRP anddevelop a certified algorithm for their computation.The feasibility of the described approach is shown throughthe adoption of the Why3 platform, which allows the necessaryverification conditions to be automatically generated and dischargedthrough a variety of automatic external SMT-solversand interactive theorem provers. Moreover, Why3 supports theextraction of certified Ocaml code for proven implementationsin WhyML. As a proof of concept the certified extracteddevelopment is demonstrated on an example system.

Subject headings

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)

ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)

Keyword

Inbyggda system

Embedded System

Publication and Content Type

ref (subject category)

kon (subject category)