Barcelona RISC-V Workshop, 2018

Dynamic Language Runtimes on RISC-V

Author: Boris Shingarov
Affiliation: LabWare
Conference: 8th RISC-V Workshop, Barcelona, 2018

Abstract:

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.

Workshop Photos

Auditorium

The Tent

Mare Nostrum

Photos, Barcelona

Palau de la Música Catalana

Montserrat

Gaudi

Santa Maria del Pi

Barcelona

  RISC-V Summit, Santa Clara, 2018

  7th RISC-V Workshop, Milpitas, 2017

Author: Boris Shingarov
Affiliation: LabWare
Conference: 7th RISC-V Workshop, Milpitas, 2017

Abstract:

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.

CCS Concepts:

Keywords:

Workshop Photos

...coming...

Photos, Silicon Valley

...coming...

  RISC-V Summit, San Jose, 2019

JIT Superoptimization on RISC-V via Symbolic Execution
Author: Boris Shingarov, Jan Vrany
Conference: RISC-V Summit, San Jose, 2019

Abstract:

We present a dynamic-language JIT in which the backend is automatically inferred from the formal ISA specification and the formal semantics of the VM's Intermediate Language. The core of the JIT comprises a Symbolic Execution Engine, and a Search Engine. The SEE computes the algebraic effect of an instruction sequence on an input state given as symbolic variables; whereas the instruction sequence itself is also given algebraically. (This latter fact is crucial because in a JIT, the binary program text is not known ahead-of-time, making many known IL lifting algorithms inapplicable.) Based on CLP(FD) algorithms, the Search Engine traverses the space of instruction sequences to find a sequence whose effect unifies with the effect of the VM bytecode being translated. To the found sequence, the search procedure attaches the proof of its equivalence with the VM bytecode.

CCS Concepts:

Keywords:

Summit Photos

...coming...

Photos, Silicon Valley

...coming...