Dynamic Language Runtimes on RISC-V
Author: Boris Shingarov
Conference: 8th RISC-V Workshop, Barcelona, 2018
Dynamic programming languages, such as Java, Smalltalk, Python, Ruby, etc.,
are critical to RISC-V's adoption
in areas that go beyond embedded micro-controllers:
areas such as mobile devices, automotive applications,
IoT, edge computing, and data centers.
At a very minimum, RISC-V needs a modern, robust,
efficient JVM with a high performance JIT.
One of the most advanced JVMs in existence is IBM's J9.
Two important advances happened to J9 recently.
First, it has been factored into a language-semantic-neutral ("universal")
runtime "OMR" and a Java portion which implements the language-specific semantics.
Second, the whole OMR+OpenJ9 is now open-source.
The focus of this talk is two-fold.
We present preliminary results in porting OMR to RISC-V.
Beyond this short-term project,
we present a roadmap of our long-term vision
which combines a belief in runtime abstractions such as the OMR API,
with a strategy for the automated synthesis of the JIT back-end
from the formal specification of RISC-V by machne reasoning,
so that multiple dynamic languages simultaneously benefit
from the same formal verification of the runtime.
Palau de la Música Catalana
Santa Maria del Pi
Comparison of two JIT compiler approaches for RISC-V
Author: Boris Shingarov
Conference: 7th RISC-V Workshop, Milpitas, 2017
We demonstrate two experimental backends for a JIT compiler for a dynamic
language's Virtual Machine. The principal design goal of the first one is
target-ISA agnosticism: we use logic programming to automatically infer the
code generator from a formal specification of the ISA written in a Processor
Description Language. On the other hand, the distinguishing characteristic of
our second backend is formal verification; the generator is developed in the
Coq interactive proof assistant and its executable form is extracted from the
proof. Both backends produce code for a number of ISAs including RISC-V. In
this talk, we compare our experiences debugging the two backends on a GEM5
simulation of RISC-V as well as on a RISC-V implementation in an FPGA.
- Software and its engineering - Virtual machines
- Software and its engineering - Formal software verication
- Programming languages - Processors
- Virtual machine
- Certied compilation
- Program proof
- Coq theorem prover
- Curry–Howard correspondence
- Processor Description Language
- Retargetable compiler
- GDB Remote Serial Protocol
Photos, Silicon Valley