Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Well formed Control-flow for Critical Sections in RTFM-core
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Embedded Internet Systems Lab.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Embedded Internet Systems Lab.ORCID iD: 0000-0002-1791-535X
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Embedded Internet Systems Lab.
ISEP, Instituto Superior de Engenharia do Porto.
Show others and affiliations
2015 (English)In: IEEE International Conference on Industrial Informatics: INDIN 2015, Cambridge, UK, July 22-24, 2015. Proceedings, Piscataway, NJ: IEEE Communications Society, 2015, 1438-1445 p., 7281944Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE Communications Society, 2015. 1438-1445 p., 7281944
National Category
Embedded Systems
Research subject
Embedded System
Identifiers
URN: urn:nbn:se:ltu:diva-39799DOI: 10.1109/INDIN.2015.7281944Local ID: eae53a46-72bd-4b6e-a12a-d656a1b025b8ISBN: 9781479966493 (electronic)OAI: oai:DiVA.org:ltu-39799DiVA: diva2:1013317
Conference
IEEE International Conference on Industrial Informatics : 22/07/2015 - 24/07/2015
Note
Validerad; 2016; Nivå 1; 20150917 (maalin)Available from: 2016-10-03 Created: 2016-10-03 Last updated: 2017-11-25Bibliographically approved

Open Access in DiVA

fulltext(220 kB)35 downloads
File information
File name FULLTEXT01.pdfFile size 220 kBChecksum SHA-512
0f53fb8556f0c8dd1b67ae58bd06bafcd45885272a39b8a8d4fe97f2dca30baa52c1692986e3e0a57ec1a15085cb20890005cc1c3053ac605ad126a141d3f8ec
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Lindgren, PerLindner, MarcusLindner, Andreas
By organisation
Embedded Internet Systems Lab
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 35 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 109 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf