Daniel Schwyn

Last Name

Schwyn

First Name

Daniel

ORCID

0000-0002-4412-9004

Show all metadata

Search Results

Publications1 - 10 of 19

Low-Overhead Reinforcement Learning-Based Power Management Using 2QoSM
Giardino, Michael; Schwyn, Daniel; Ferri, Bonnie; et al. (2022)
Journal of Low Power Electronics and Applications
With the computational systems of even embedded devices becoming ever more powerful, there is a need for more effective and pro-active methods of dynamic power management. The work presented in this paper demonstrates the effectiveness of a reinforcement-learning based dynamic power manager placed in a software framework. This combination of Q-learning for determining policy and the software abstractions provide many of the benefits of co-design, namely, good performance, responsiveness and application guidance, with the flexibility of easily changing policies or platforms. The Q-learning based Quality of Service Manager (2QoSM) is implemented on an autonomous robot built on a complex, powerful embedded single-board computer (SBC) and a high-resolution path-planning algorithm. We find that the 2QoSM reduces power consumption up to 42% compared to the Linux on-demand governor and 10.2% over a state-of-the-art situation aware governor. Moreover, the performance as measured by path error is improved by up to 6.1%, all while saving power.
Generating Trustworthy Hardware/Software I²C Drivers for Board Management Controllers
Schwyn, Daniel; Liu, Zikai; Roscoe, Timothy (2024)
seL4 Summit 2024 Abstracts
2QoSM: A Q-Learner QoS Manager for Application-Guided Power-Aware Systems
Giardino, Michael Joseph; Schwyn, Daniel; Ferri, Bonnie; et al. (2021)
2021 IEEE 14th International Symposium on Embedded Multicore/Many-core Systems-on-Chip (MCSoC)
This paper describes the design and performance of Q-learning-based quality-of-service manager (2QoSM) for compute-aware applications (CAAs) as part of platform-agnostic resource management framework. CAAs and hardware are able to share metrics of performance with the 2QoSM and the 2QoSM can attempt to reconfigure CAAs and hardware to meet performance targets. This enables many co-design benefits while allowing for policy and platform portability. The use of QLearning allows online generation of the power management policy without requiring details about system state or actions, and can meet different goals including error, power minimization, or a combination of both. 2QoSM, evaluated using an embedded MCSoC controlling a mobile robot, reduces power compared to the Linux on-demand governor by 38.7-42.6% and a situation-aware governor by 4.0-10.2%. An error-minimization policy obtained a reduction in path-following error of 4.6-8.9%.
From Sound to Sight: Using Audio Processing to enable Visible Light Communication
Schmid, Stefan; Schwyn, Daniel; Akşit, Kaan; et al. (2014)
2014 IEEE Globecom Workshops (GC WKshps)
Mobile phones can use their cameras and flashlight Light Emitting Diodes (LEDs) to exchange messages with low-complex Visible Light Communication (VLC) networks, but these interfaces impose serious restrictions when used in a VLC network. In this paper we discuss how to extend mobile phones or tablets with a small peripheral device that is battery-free, uses only passive components, and offers VLC capabilities at the required data rate (kilobit per second). This device plugs into the audio jack; on-board audio signal processing generates the outgoing light signals as well as decodes the incoming light signals. The device is powered from the phone's audio jack output signal, no additional battery is required. The audio signals directly modulate light emissions of an LED. Incoming light is detected by a photodiode and the generated electrical signals are fed into the microphone input. This simple device enables use of existing communication protocols and therefore makes it possible to integrate mobile phones or tablets into existing VLC LED-to-LED networks.
Generating correct initial page tables from formal hardware descriptions
Achermann, Reto; Cock, David; Haecki, Roni; et al. (2021)
PLOS '21: Proceedings of the 11th Workshop on Programming Languages and Operating Systems
Specifying the de-facto OS of a production SoC
Fiedler, Ben; Meier, Roman; Schult, Jasmin; et al. (2023)
KISV '23: Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification
Verification of any operating system is inevitably relative to a model of the underlying hardware. Within the context of kernel verification, the underlying hardware model usually comprises of architectural correctness of the executing cores, but pays little attention to devices underneath barring the assumption that they are "trusted".Recent work has pointed out that the de facto operating system of a machine includes not only the kernel and processes running on top, but the multitude of other devices driving the actual hardware: security (co-)processors, DMA engines, network firmware, and more. The concept of the de facto OS shines light on a critical boundary between a kernel and the rest of hardware which is crucial to reasoning about both kernel isolation, and the security properties of the whole operating system. In this paper we report on our experience to date in specifying the de facto OS environment of a production System-on-Chip, and the implications of this effort so far for assured kernel isolation.
Hardware Configuration With Dynamically-Queried Formal Models
Schwyn, Daniel (2017)
Putting out the hardware dumpster fire
Fiedler, Ben; Schwyn, Daniel; Gierczak-Galle, Constantin; et al. (2023)
HOTOS '23: Proceedings of the 19th Workshop on Hot Topics in Operating Systems
The immense hardware complexity of modern computers, both mobile phones and datacenter servers, is a seemingly endless source of bugs and vulnerabilities in system software.Classical OSes cannot address this, since they only run on a small subset of the machine. The issue is interactions within the entire ensemble of firmware blobs, co-processors, and CPUs that we term the de facto OS. The current "whac-a-mole"approach will not solve this problem, nor will clean-slate redesign: it is simply not possible to replace some firmware components and the engineering effort is too great.Our response, instead, is to build a high-level model of exactly what a given real hardware and software platform consists of, and captures for the first time the necessary and assumed trust relationships between the software contexts executing on different components (CPUs, devices, etc.).This principled but pragmatic approach allows us to make rigorous statements about the hodgepodge of soft- and firmware at the heart of modern computers. We expect these statements to be, at first, depressingly weak, but it may be the only way to identify changes that provably increase the trustworthiness of a real system, and quantify the benefits of these changes.
Efeu: generating efficient, verified, hybrid hardware/software drivers for I²C devices
Schwyn, Daniel; Liu, Zikai; Roscoe, Timothy (2025)
EuroSys '25: Proceedings of the Twentieth European Conference on Computer Systems
Writing device drivers is notoriously hard, and driver bugs are a major cause of system failures and vulnerabilities. The problem is particularly acute in bus-based protocols like I²C, where driver correctness is only half the story: correct functioning of the complete subsystem depends on all components on the bus interoperating correctly. Unfortunately, developers cannot control all aspects of a platform, and must interact with existing devices (peripherals and/or hardware bus controllers) which may misbehave. Failures in a protocol like I²C, often used in critical low-level system management, can result in permanent damage to the hardware, whether a server or a satellite. Existing techniques for creating high assurance drivers rarely tackle this interoperability issue. We present Efeu, a framework for implementing verifiably interoperable drivers for I²C devices. Using model checking-based verification, Efeu generates driver implementations in software, reconfigurable logic for FPGAs, and, notably, combinations of both. The split between software and hardware can be varied at implementation time and the hardware/software interface is generated automatically, enabling efficient exploration of the design space. Using Efeu, we design and evaluate a verified I²C driver stack, and demonstrate that Efeu finds optimal hardware/software tradeoffs to favor either throughput, CPU usage or FPGA footprint. For each objective, Efeu generates drivers with performance comparable with hand-optimized hardware/software drivers.
A Model-Checked I2C Specification
Humbel, Lukas; Schwyn, Daniel; Hossle, Nora; et al. (2021)
Lecture Notes in Computer Science ~ Model Checking Software
I2C is a pervasive bus protocol used for querying sensors and actuators, but it is plagued with incompatible devices, violating the specification at various levels. Interacting with partially compliant devices poses several challenges. Compatibility of the controller interface, as well as the driver code, must be checked manually and potentially changed. This is a difficult process, as interactions with other bus devices must also be considered. We propose a model checking approach to quickly write high-assurance drivers and layers of the I2C stack. We do not propose a single, true formalization of I2C, but a framework that allows rapid modelling of non-compliant devices and verify the correct interaction with a host driver process. Our contribution is twofold: First, we develop a framework that allows the specification of device and driver behavior together, and verification of their correct interaction. Second, we provide already verified, fine-grained building blocks, representing layers of the I2C stack that can be reused to interact with partially-compliant devices, as well as reducing model checking complexity. Our specifications are stated in a machine-readable, executable, and layered DSL. From the DSL, we generate both Promela and C code. The Promela is used to apply model checking to ensure the layer implementations follow the abstract specifications. The C code is used to build and verify an EEPROM model and driver running on a Raspberry Pi.

Publications1 - 10 of 19

Daniel Schwyn

Last Name

First Name

ORCID

Organisational unit

Filters

Search Results