Well formed Control-flow for Critical Sections in RTFM-core

The mainstream of embedded software development as of today is dominated by C programming. To aid the development, hardware abstractions, libraries, kernels and lightweight operating systems are commonplace. Such kernels and operating systems typically impose a thread based abstraction to concurrency. However, in general thread based programming is hard, plagued by hazards of race conditions and dead-locks. For this paper we take an alternative outset in terms of a language abstraction, RTFM-core, where the system is modelled directly in terms of tasks and resources. In compliance to the Stack Resource Policy (SRP) model, the language enforces (well formed) LIFO nesting of claimed resources, thus SRP based analysis and scheduling can be readily applied. For the execution onto bare-metal single core architectures, the rtfm-core compiler performs SRP analysis on the model, and render an executable that is deadlock free and (through RTFM-kernel primitives) exploits the underlying interrupt hardware for efficient scheduling. The RTFM-core language embeds C-code and links to C-object files and libraries, and is thus applicable to the mainstream of embedded development. However, while the language enforces well formed resource management, control flow in the embedded C-code may violate the LIFO nesting requirement, thus correctness is left with the programmer to ensure well formed nesting (through restricted control flow). In this paper we address this issue by lifting a subset of C into the RTFM-core language allowing arbitrary control flow at the model level. In this way well formed LIFO nesting can be enforced, and models ensured to be correct by construction. We demonstrate the feasibility trough a prototype implementation in the rtfm-core compiler. Additionally, we develop a set of running examples, and show in detail how control flow is handled at compile time and during run-time execution.Validerad; 2016; Nivå 1; 20150917 (maalin