Abstract

Abstract

Abstract

Abstract

Abstract
Real-Time For the Masses (RTFM) is a set of languages and tools being developed to facilitate embedded software development and provide highly efficient implementations geared to static verification. The RTFM-kernel is an architecture designed to provide highly efficient and predicable Stack Resource Policy based scheduling, targeting bare metal (singlecore) platforms. We contribute beyond prior work by introducing a platform independent timer abstraction that relies on existing RTFM-kernel primitives. We develop two alternative implementations for the ARM Cortex-M family of MCUs: a generic implementation, using the ARM defined SysTick- /DWT hardware; and a target specific implementation, using the match compare/free running timers. While sacrificing generality, the latter is more exible and may reduce overall overhead. Invariants for correctness are presented, and methods to static and run-time verification are discussed. Overhead is bound and characterized. In both cases the critical section from release time to dispatch is less than 2us on a 100MHz MCU. Queue and timer mechanisms are directly implemented in the RTFM-core language and can be included in system-wide scheduling analysis.

Abstract