Sökning: WFRF:(Lindner Andreas) >
Well formed Control...
Well formed Control-flow for Critical Sections in RTFM-core
-
- Lindgren, Per (författare)
- Luleå tekniska universitet,EISLAB
-
- Lindner, Marcus (författare)
- Luleå tekniska universitet,EISLAB
-
- Lindner, Andreas (författare)
- Luleå tekniska universitet,EISLAB
-
visa fler...
-
- Pereira, David J. (författare)
- ISEP, Instituto Superior de Engenharia do Porto
-
- Pinho, Luis Miguel (författare)
- ISEP, Instituto Superior de Engenharia do Porto
-
visa färre...
-
(creator_code:org_t)
- Piscataway, NJ : IEEE Communications Society, 2015
- 2015
- Engelska.
-
Ingår i: IEEE International Conference on Industrial Informatics. - Piscataway, NJ : IEEE Communications Society. - 9781479966493 ; , s. 1438-1445
- Relaterad länk:
-
https://ltu.diva-por... (primary) (Raw object)
-
visa fler...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
Nyckelord
- Inbyggda system
- Embedded System
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas