ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Mon 16 Nov 2020 01:00 - 01:20 at SPLASH-I - S-4 Chair(s): Atsushi Igarashi, Elisa Gonzalez Boix
Sun 15 Nov 2020 13:00 - 13:20 at SPLASH-I - S-4 Chair(s): Karim Ali, Eli Tilevich

LLVM is designed for the compile-time, link-time and run-time optimization of programs written in various programming languages. The language supported by LLVM targeted by modern compilers is LLVM IR. In this paper we define K-LLVM, a reference semantics for LLVM IR. To the best of our knowledge, K-LLVM is the most complete formal LLVM IR semantics to date, including all LLVM IR instructions, intrinsic functions in the LLVM documentation and Standard-C library functions that are necessary to execute many LLVM IR programs. Additionally, K-LLVM formulates an abstract machine that executes all LLVM IR instructions. The machine allows to describe our formal semantics in terms of simulating a conceptual virtual machine that runs LLVM IR programs, including non-deterministic programs. Even though the K-LLVM memory model in this paper is assumed to be a sequentially consistent memory model and does not include all LLVM concurrency memory behaviors, the design of K-LLVM’s data layout allows the K-LLVM abstract machine to execute some LLVM IR programs that previous semantics did not cover, such as the full range of LLVM IR behaviors for the interaction among LLVM IR casting, pointer arithmetic, memory operations and some memory flags (e.g. readonly) of function headers. Additionally, the memory model is modularized in a manner that supports investigating other memory models. To validate K-LLVM, we have implemented it in K [41], which generated an interpreter for LLVM IR. Using this, we ran tests including 1,385 unit test programs and 2,156 concrete LLVM IR programs, and K-LLVM passed all of them.

Sun 15 Nov
Times are displayed in time zone: Central Time (US & Canada) change

13:00 - 14:20: S-4Research Papers at SPLASH-I +12h
Chair(s): Karim AliUniversity of Alberta, Eli TilevichVirginia Tech
13:00 - 13:20
Talk
Research Papers
Liyi LiUniversity of Illinois at Urbana-Champaign, Elsa GunterUniversity of Illinois
Link to publication DOI Media Attached
13:20 - 13:40
Talk
Research Papers
Xuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong
Link to publication DOI Media Attached
13:40 - 14:00
Talk
Research Papers
Davide AnconaDIBRIS, University of Genova, Italy, Francesco DagninoDIBRIS, University of Genova, Italy, Jurriaan RotRadboud University Nijmegen, Elena ZuccaUniversity of Genova
Link to publication DOI Media Attached
14:00 - 14:20
Talk
Research Papers
Raphaël MonatSorbonne Université — LIP6, Abdelraouf OuadjaoutSorbonne Université, Antoine MinéSorbonne Université
Link to publication DOI Media Attached File Attached

Mon 16 Nov
Times are displayed in time zone: Central Time (US & Canada) change

01:00 - 02:20: S-4Research Papers at SPLASH-I
Chair(s): Atsushi IgarashiKyoto University, Japan, Elisa Gonzalez BoixVrije Universiteit Brussel, Belgium
01:00 - 01:20
Talk
Research Papers
Liyi LiUniversity of Illinois at Urbana-Champaign, Elsa GunterUniversity of Illinois
Link to publication DOI Media Attached
01:20 - 01:40
Talk
Research Papers
Xuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong
Link to publication DOI Media Attached
01:40 - 02:00
Talk
Research Papers
Davide AnconaDIBRIS, University of Genova, Italy, Francesco DagninoDIBRIS, University of Genova, Italy, Jurriaan RotRadboud University Nijmegen, Elena ZuccaUniversity of Genova
Link to publication DOI Media Attached
02:00 - 02:20
Talk
Research Papers
Raphaël MonatSorbonne Université — LIP6, Abdelraouf OuadjaoutSorbonne Université, Antoine MinéSorbonne Université
Link to publication DOI Media Attached File Attached