Abstract

This is work in progress. Selfie is educational software that implements a self-compiling compiler of a tiny C subset, a self-executing emulator of a tiny MIPS subset targeted by the compiler, and a self-hosting hypervisor that virtualizes the emulated machine. There is also a port to RISC -V supported by the official RISC -V toolchain. The code in selfie that handles context switching and virtual memory is shared by both the emulator and the hypervisor. In fact their only difference is that upon context switching the emulator interprets code while the hypervisor has the emulator on which it runs interpret code. We are currently trying to leverage that design for validating the functional equivalence of emulation and virtualization in test runs. The long term goal is to verify functional equivalence formally for all input programs. The talk provides an overview of the existing system and then focuses on current development and the challenges ahead.

This is joint work with Alireza Abyaneh and Armin Biere, JKU Linz.

Bio:

Christoph Kirsch is Professor at the Department of Computer Sciences of the University of Salzburg, Austria. He received his Dr.Ing. degree from Saarland University, Saarbrücken, Germany, in 1999 while at the Max Planck Institute for Computer Science. From 1999 to 2004 he worked as Postdoctoral Researcher at the Department of Electrical Engineering and Computer Sciences of the University of California, Berkeley. He later returned to Berkeley as Visiting Scholar (2008-2013) and Visiting Professor (2014) at the Department of Civil and Environmental Engineering as part of a collaborative research effort in Cyber-Physical Systems. His research interests are in concurrent programming, memory management, virtualization, and automated theorem proving. Dr. Kirsch co-invented embedded programming languages and systems such as Giotto, HTL , and the Embedded Machine, and more recently co-designed high-performance, multicore-scalable concurrent data structures and memory management systems. He co-founded the International Conference on Embedded Software (EMSOFT) and served as ACM SIGBED chair from 2011 until 2013 and ACM TODAES associate editor from 2011 until 2014. He is currently associate editor of IEEE TCAD .