Static analysis techniques can be used to compute safe bounds on the worst-case execution time (WCET) of programs. For large programs, abstractions are often required to curb computational ...complexity. These abstractions may introduce infeasible paths which result in significant overestimation. These paths can be eliminated by adding additional constraints to the static analysis. Such constraints can be found manually but this is labour-intensive and error-prone. Automated methods of finding infeasible path constraints are thus highly desirable. In this paper we present Trickle: a method to automatically detect infeasible paths on compiled binary programs, in order to refine WCET estimates. We build upon the Sequoll framework and apply satisfiability modulo theory (SMT) solvers to find classes of infeasible paths. Unlike other techniques, Trickle can find infeasible paths which contain an arbitrary number of conflicting conditions. We also integrate the compute all minimal unsatisfiable subsets (CAMUS) algorithm to reduce the number of refinement iterations required. We show the practicality of Trickle by applying it to a WCET analysis of the seL4 microkernel. We also evaluate its effectiveness on the Mälardalen WCET benchmarks.
Microarchitectural timing channels use variations in the timing of events, resulting from competition for limited hardware resources, to leak information in violation of the operating system's ...security policy. Such channels also exist on a simple in-order RISC-V core, as we demonstrate on the open-source RV64GC Ariane core. Time protection, recently proposed and implemented in the seL4 microkernel, aims to prevent timing channels, but depends on a controlled reset of microarchitectural state. Using Ariane, we show that software techniques for performing such a reset are insufficient and highly inefficient. We demonstrate that adding a single flush instruction is sufficient to close all five evaluated channels at negligible hardware costs, while requiring only minor modifications to the software stack.
System virtualization, which enjoys immense popularity in the enterprise and personal computing spaces, is recently gaining significant interest in the embedded domain. Starting from a comparison of ...key characteristics of enterprise systems and embedded systems, we will examine the difference in motivation for the use of system virtual machines, and the resulting differences in the requirements for the technology. We find that these differences are quite substantial, and that virtualization is unable to meet the special requirements of embedded systems. Instead, more general operating-systems technologies are required, which support virtualization as a special case. We argue that high-performance microkernels, specifically L4, are a technology that provides a good match for the requirements of next-generation embedded systems.
A Scalable Lock Manager for Multicores Jung, Hyungsoo; Han, Hyuck; Fekete, Alan ...
ACM transactions on database systems,
12/2014, Letnik:
39, Številka:
4
Journal Article
Recenzirano
Modern implementations of DBMS software are intended to take advantage of high core counts that are becoming common in high-end servers. However, we have observed that several database platforms, ...including MySQL, Shore-MT, and a commercial system, exhibit throughput collapse as load increases into oversaturation (where there are more request threads than cores), even for a workload with little or no logical contention for locks, such as a read-only workload. Our analysis of MySQL identifies latch contention within the lock manager as the bottleneck responsible for this collapse.
We design a lock manager with reduced latching, implement it in MySQL, and show that it avoids the collapse and generally improves performance. Our efficient implementation of a lock manager is enabled by a staged allocation and deallocation of locks. Locks are preallocated in bulk, so that the lock manager only has to perform simple list manipulation operations during the acquire and release phases of a transaction. Deallocation of the lock data structures is also performed in bulk, which enables the use of fast implementations of lock acquisition and release as well as concurrent deadlock checking.
Component-based software engineering promises to provide structure and reusability to embedded-systems software. At the same time, microkernel-based operating systems are being used to increase the ...reliability and trustworthiness of embedded systems. Since the microkernel approach to designing systems is partially based on the componentisation of system services, component-based software engineering is a particularly attractive approach to developing microkernel-based systems. While a number of widely used component architectures already exist, they are generally targeted at enterprise computing rather than embedded systems. Due to the unique characteristics of embedded systems, a component architecture for embedded systems must have low overhead, be able to address relevant non-functional issues, and be flexible to accommodate application specific requirements. In this paper we introduce a component architecture aimed at the development of microkernel-based embedded systems. The key characteristics of the architecture are that it has a minimal, low-overhead, core but is highly modular and therefore flexible and extensible. We have implemented a prototype of this architecture and confirm that it has very low overhead and is suitable for implementing both system-level and application level services.
Tutorial: Using the seL4 Microkernel Heiser, Gernot; Velickovic, Ivan
2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S),
2023-June
Conference Proceeding
The seL4 microkernel 3 is the first general-purpose operating system (OS) kernel with a formal proof of implementation correctness. By now, its verification covers functional correctness to the ...binary (taking the compiler out of the trust chain), proofs of security enforcement and worst-case execution-time bounds, and span three architectures (32-bit Arm and 64-bit RISC-V and x86) 1. All this while featuring unbeaten performance. seL4 is now being deployed in safety- and security-critical systems around the world, and is backed by the non-profit seL4 Foundation 2.
File systems deserve verification too Keller, Gabriele; Murray, Toby; Amani, Sidney ...
Operating systems review,
05/2014, Letnik:
48, Številka:
1
Journal Article
File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file ...system implementations-we need verified correctness but at reasonable cost. This paper presents our vision and ongoing work to achieve this goal for a new high-performance flash file system, called BilbyFs. BilbyFs is carefully designed to be highly modular, so it can be verified against a high-level functional specification one component at a time. This modular implementation is captured in a set of domain specific languages from which we produce the design-level specification, as well as its optimised C implementation. Importantly, we also automatically generate the proof linking these two artefacts. The combination of these features dramatically reduces verification effort. Verified file systems are now within reach for the first time.
Modern smartphones are increasingly performant and feature-rich but remain highly power-constrained. Effective energy management demands an informed policy, and to that end we present a detailed ...power analysis of the Samsung Galaxy S III smartphone. We measure power consumption by instrumentation at the circuit level, and present a breakdown by the major components including CPU, RAM, display, GPU, wireless radios, camera, GPS and environmental sensors.
This paper presents an improved method for measuring the total lumped series resistance (Rs) of high‐efficiency solar cells. Since this method greatly minimizes the influence of non‐linear ...recombination processes on the measured Rs values, it is possible to determine Rs as a function of external current density over a wide range of illumination levels with a significantly improved level of accuracy. This paper furthermore explains how resistive losses in the emitter, the base, the metal/silicon contacts and the front metal grid can be separately determined by combining measurements and multidimensional numerical simulations. A novel combination of device simulation and circuit simulation is introduced in order to simulate complete 2 × 2 cm2 PERL (‘passivated emitter and rear locally‐diffused’) silicon solar cells. These computer simulations provide improved insight into the dynamics of resistive losses, and thus allow new strategies for the optimization of resistive losses to be developed. The predictions have been experimentally verified with PERL cells, whose resistive losses were reduced to approximately half of their previous values, contributing to a new efficiency world record (24.0%) for silicon solar cells under terrestrial illumination. The measurement techniques and optimization strategies presented here can be applied to most other types of solar cells, and to materials other than silicon.
Towards trustworthy computing systems Heiser, Gernot; Elphinstone, Kevin; Kuz, Ihor ...
Operating systems review,
07/2007, Letnik:
41, Številka:
4
Journal Article
As computer systems become increasingly mission-critical, used in life-critical situations, and relied upon to protect intellectual property, operating-system reliability is becoming an ever growing ...concern. In the past, mission- and life-critical embedded systems consisted of simple microcontrollers running a small amount of software that could be validated using traditional and informal techniques. However, with the growth of software complexity, traditional techniques for ensuring software reliability have not been able to keep up, leading to an overall degradation of reliability. This paper argues that microkernels are the best approach for delivering truly trustworthy computer systems in the foreseeable future. It presents the NICTA operating-systems research vision, centred around the L4 microkernel and based on four core projects. The
seL4
project is designing an improved API for a secure microkernel,
L4, verified
will produce a full formal verification of the microkernel, Potoroo combines execution-time measurements with static analysis to determine the worst case execution profiles of the kernel, and
CAmkES
provides a component architecture for building systems that use the microkernel. Through close collaboration with
Open Kernel Labs
(a NICTA spinoff) the research output of these projects will make its way into products over the next few years.
PDF
