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.
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