About: Synthesizing JIT Compilers for In-Kernel DSLs

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Synthesizing JIT Compilers for In-Kernel DSLs Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : covidontheweb.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Synthesizing JIT Compilers for In-Kernel DSLs
Creator	Wang, Xi Dillig, Isil Nelson, Luke Torlak, Emina Van Geffen, Jacob
Source	PMC
abstract	Modern operating systems allow user-space applications to submit code for kernel execution through the use of in-kernel domain specific languages (DSLs). Applications use these DSLs to customize system policies and add new functionality. For performance, the kernel executes them via just-in-time (JIT) compilation. The correctness of these JITs is crucial for the security of the kernel: bugs in in-kernel JITs have led to numerous critical issues and patches. This paper presents JitSynth, the first tool for synthesizing verified JITs for in-kernel DSLs. JitSynth takes as input interpreters for the source DSL and the target instruction set architecture. Given these interpreters, and a mapping from source to target states, JitSynth synthesizes a verified JIT compiler from the source to the target. Our key idea is to formulate this synthesis problem as one of synthesizing a per-instruction compiler for abstract register machines. Our core technical contribution is a new compiler metasketch that enables JitSynth to efficiently explore the resulting synthesis search space. To evaluate JitSynth, we use it to synthesize a JIT from eBPF to RISC-V and compare to a recently developed Linux JIT. The synthesized JIT avoids all known bugs in the Linux JIT, with an average slowdown of [Formula: see text] in the performance of the generated code. We also use JitSynth to synthesize JITs for two additional source-target pairs. The results show that JitSynth offers a promising new way to develop verified JITs for in-kernel DSLs.
has issue date	2020-06-16(xsd:dateTime)
bibo:doi	10.1007/978-3-030-53291-8_29
has license	cc-by
sha1sum (hex)	2f697b70b2e627210996fa8ceec131ef131e3d1d
schema:url	https://doi.org/10.1007/978-3-030-53291-8_29
resource representing a document's title	Synthesizing JIT Compilers for In-Kernel DSLs
has PubMed Central identifier	PMC7363179
schema:publication	Computer Aided Verification
resource representing a document's body	covid:2f697b70b2e627210996fa8ceec131ef131e3d1d#body_text
is schema:about of	named entity 'Applications' named entity 'numerous' named entity 'compilation' named entity 'SYSTEM' named entity 'OPERATING SYSTEMS' named entity 'NUMEROUS' named entity 'just-in-time' named entity 'performance' named entity 'security' named entity 'DSLs' named entity 'execution' named entity 'Modern operating systems' named entity 'DSLs' named entity 'in-kernel' named entity 'domain specific languages' named entity 'correctness' named entity 'kernel' named entity 'eBPF' named entity 'syntax' named entity 'in-kernel' named entity 'infinite set' named entity 'eBPF' named entity 'compiler' named entity 'compiler' named entity 'LLVM' named entity 'Linux kernel' named entity 'eBPF' named entity 'memory store' named entity 'subroutines' named entity '32-bit' named entity 'SMT' named entity 'generated code' named entity 'register machine' named entity 'PowerPC' named entity 'BPF' named entity 'Linux' named entity 'algorithm' named entity 'heuristics' named entity 'register machine' named entity 'JIT compiler' named entity 'compiler' named entity 'compiler' named entity 'register-register' named entity 'DSLs' named entity 'eBPF' named entity 'JIT' named entity 'SMT' named entity 'eBPF' named entity 'target field' named entity 'eBPF' named entity 'Coq' named entity 'semantics' named entity 'arithmetic' named entity 'compiler' named entity 'memory addresses' named entity 'JIT compilers' named entity 'language specification' named entity 'eBPF' named entity 'opcodes' named entity 'compiler' named entity 'JIT compiler' named entity 'kernel' named entity 'eBPF' named entity 'compiler' named entity 'compiler' named entity '32-bit' named entity 'search spaces' named entity 'target languages' named entity 'RISC-V' named entity 'bitvector' named entity 'automated verification' named entity 'target languages' named entity 'JIT compiler' named entity 'JIT' named entity 'equivalent states' named entity 'JIT compilers' named entity 'constant factor' named entity 'memory locations' named entity 'scalability'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software