The emergence of the open RISC-V instruction set architecture has enabled the design of highly efficient processor cores by extending the relatively simple architecture with custom functionality specific to the application. The design and simulation of such extensions is traditionally done using hardware description languages (HDLs) which is time-consuming and cumbersome. SyncRim, the synchronous circuit simulation tool presented in this thesis takes a high-level approach to digital circuit design, omitting irrelevant implementation details in a simulator model of a processor, which allows for rapid prototyping of anything from architecture extensions to entire processor cores. We show how a synchronous circuit simulator can be implemented using the Rust programming language, and showcase how such a simulator can be used to aid in hardware/software co-design by implementing a RISC-V core, extending it with the bleeding edge Core-Local Interrupt Controller(CLIC), and porting a Rust real-time operating system, the RTIC framework to the CLIC-extended RISC-V.
In this thesis, the proof-of-concept tool RAUK for automatically analyzing RTIC applications for schedulability using symbolic execution is presented. The RTIC framework provides a declarative executable model for building embedded applications, which behavior is based on established formal methods and policies. Because of this, RTIC applications are amenable for both worst-case execution time (WCET) and scheduling analysis techniques. Internally, RAUK utilizes the symbolic execution tool KLEE to generate test vectors covering all feasible execution paths in all user tasks in the RTIC application. Since KLEE also checks for possible program errors e.g. arithmetic or array indexing errors, it can be used via RAUK to verify the robustness of the application in terms of program errors. The test vectors are replayed on the target hardware to record a WCET estimation for all user tasks. These WCET measurements are used to derive a worst-case response time (WCRT) for each user task, which in turn is used to determine if the system is schedulable using formal scheduling analysis techniques. The evaluation of this tool shows a good correlation between the results from RAUK and manual measurements of the same tasks, which showcases the viability of this approach. However, the current implementation can add some substantial overhead to the measurements, and sometimes certain types of paths in the application can be completely absent from the analysis. The work in this thesis is based on previous research in this field for WCET estimation using KLEE on an older iteration of the RTIC framework. Our contributions include a focus on an RTIC 1.0 pre-release, a seamless integration with the Rust ecosystem, minimal changes required to the application itself, as well as an included automatic schedulability analyzer. Currently, RAUK can verify simple RTIC applications for both program errors and schedulability with minimal changes to the application source code. The groundwork is laid out for further improvements that are required to function on larger and more complex applications. Solutions for known problems and future work are discussed in Chapters 6, 7 respectively.
Real-time systems are a segment of embedded systems that have remained dominated by proprietary hardware architectures, despite the continuing growth of the open-source RISC-V instruction set architecture (ISA). The introduction of core-local interrupt controller (CLIC) extensions to the RISC-V architecture presents a promising opportunity to bridge the technological gap with ARM in low-latency interrupt handling. Regarding software, the real-time interrupt-driven concurrency (RTIC) framework enables ever lighter hard real-time systems with formal compile-time guarantees for memory safety, response time and overall schedulability. In this publication we adapt Ibex, a small, open-source RISC-V processor for CLIC support and present Atalanta, a lightweight microcontroller designed around the RTIC framework. Atalanta implements a localized memory architecture that enables low-latency context switching together with a large number of supported interrupt inputs and levels provided by the CLIC specification. We evaluate Atalanta for real-time performance and implementation feasibility through simulation-based measurements and FPGA prototyping, respectively. We are able to demonstrate an interrupt latency of 5 cycles with minimal jitter and a context switch latency of 21 cycles, placing it competitively against current state-of-the-art solutions. Furthermore, we implement an FPGA prototype for the Xilinx PYNQ-Z1 and VCU118 boards, targeting a frequency of 45 MHz. We publish the sources and implementation scripts of Atalanta under a permissive open-source license.
Work done at Luleå Technical University regarding the RTIC RTOS framework is expanded upon to yield a convenient toolset for event-based instrumentation by exploiting debug peripherals available on the ARMv7-M platform.
By parsing the source of an RTIC application and recovering instrumentation metadata from user-supplied information, the target-emitted trace stream is decoded and mapped to RTIC task events, yielding a timeline of events that can be analyzed live and postmortem by help of a recording host-side daemon.
Relevant sections of the ARMv7-M standard are covered, and peripheral configuration covered in detail.
An instrumentation result of a trivial RTIC application is presented and graphically plotted to exemplify the value of the toolset, and topics of future work to improve the toolset are outlined.
To ensure the correctness of real time systems, it is important to determine the execution time of tasks. The worst case execution time of each task needs to be found in order to determine if the system is schedulable. This thesis aims at bounding the execution time of programs analyzed by KLEE, a symbolic execution engine. This is done by estimating the cycles required on the Cortex-M4 processor. A custom fork of KLEE has been created which outputs additional information about the program under analysis. This information is used by a tool written in Rust which reconstructs the corresponding control flow in optimized assembly code. KLEE analyzes an intermediate representation language, LLVM IR. This representation is used in the compilation process of many programming languages. One of these languages is Rust which has been the primary focus of the tool. Testing has been done on applications written with the RTIC framework. The measured cycles of these applications has been correctly bounded for all test cases.
Embedded systems are commonplace, often with real-time requirements, limited resources and increasingly complex workloads with high demands on security and reliability. The complexity of these systems calls for extensive developer experience and many tools has been created to aid in the development of the software running on such devices. One of these tools, the Real-Time For the Masses (RTFM) concurrency framework developed at Luleå University of Technology (LTU), is built upon a pre-existing, well established and theoretically underpinned execution model providing deadlock free execution and strong guarantees about correctness. The framework is further enhanced by the memory safety provided by Rust, a modern systems programming language. This thesis documents the work done towards improving the framework by studying the possibility to make it extendable. For this, a model of the present layout is required, which in turn requires a solid understanding of Rust's way to structure code. To realise such a large structural change it was advisable to join the open-source RTFM community as a core developer. This role included new responsibilities and required work within different areas of the framework, not only directly related to the primary goal. It also provided the insight that in order to reach the desired extendable structure, many other improvements had to be done first, including the removal of large experimental features. To aid the development, usage of state of the art Continuous Integration testing (CI) were key. Changes to such systems are also part of the development process. The name of the project changed in the middle of this thesis work, going from RTFM to Real-Time Interrupt-driven Concurrency (RTIC). The implemented features and usability fixes detailed in this thesis improves the user experience for embedded system developers resulting in increased productivity while making the development process of such systems more accessible. These general improvements will be part of the next release of the framework. A version v0.6.0-alpha.0 of the framework has been released for testing. The experiences gained related to open-source project governance during this work are also presented.
Calculating WCET for schedulability analysis of RTIC applications is today performed with a hybrid approach with both static analysis of code and hardware measurements. A fully static analysis tool would allow for a easier integration into a CI/CD pipeline without the actual hardware. This thesis attempts to compute WCET statically, using symbolic execution engine KLEE to generate all the possible paths of execution for a task and then analyses these paths to approximate the worst-case for each path which would yield a approximate WCET for the analysed program.
To analyze a path in a program the low-level intermediary assembly language used by the LLVM optimization infrastructure (called LLVM IR) is compared to the finished assembly language to draw conclusions on how an LLVM IR instruction is processed into assembly. To be able to perform this mapping from LLVM IR to assembly, the symbolic execution engine KLEE has been extended to also log each LLVM IR instruction run in a path. These logs combined with a translation table is how the approximations are calculated.
The resulting approximations correlate with the actual cycles when the analysed program is run on actual hardware, which indicates that tool could actually be used to approximate WCET. There are however no guarantees and the tool has not been tested for larger scale programs.