WFRF:(Lindnér Per)
Search: WFRF:(Lindnér Per) > (2015-2019) > Well formed Control...
- 6 of 78
- Previous record
- Next record
- To hitlist
Well formed Control-flow for Critical Sections in RTFM-core
-
- Lindgren, Per (author)
- Luleå tekniska universitet,EISLAB
-
- Lindner, Marcus (author)
- Luleå tekniska universitet,EISLAB
-
- Lindner, Andreas (author)
- Luleå tekniska universitet,EISLAB
- show more...
- show less...
- (creator_code:org_t)
- Piscataway, NJ : IEEE Communications Society, 2015
- 2015
- English.
- In: IEEE International Conference on Industrial Informatics. - Piscataway, NJ : IEEE Communications Society. - 9781479966493 ; , s. 1438-1445
- Conference paper (peer-reviewed)
Abstract
Subject headings
Close
- 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.
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)
Find in a library
- IEEE International Conference on Industrial Informatics (Search for host publication in LIBRIS)
To the university's database
- 6 of 78
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Lindgren, Per
- Lindner, Marcus
- Lindner, Andreas
- Pereira, David J ...
- Pinho, Luis Migu ...
- About the subject
-
- ENGINEERING AND TECHNOLOGY
- ENGINEERING AND ...
- and Electrical Engin ...
- and Embedded Systems
- Articles in the publication
- IEEE Internation ...
- By the university
- Luleå University of Technology
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
