ICSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
Thu 18 Apr 2024 11:15 - 11:30 at Glicínia Quartin - Dependability and Formal methods 2 Chair(s): Jácome Cunha

We present TurboTV, a translation validator for the JavaScript (JS) just-in-time (JIT) compiler of V8. While JS engines have become a crucial part of various software systems, their emerging adaption of JIT compilation makes it increasingly challenging to ensure their correctness. We tackle this problem with an SMT-based translation validation (TV) that checks whether a specific compilation is semantically correct. We formally define the semantics of IR of TurboFan (JIT compiler of V8) as SMT encoding. For efficient validation, we design a staged strategy for JS JIT compilers. This allows us to decompose the whole correctness checking into simpler ones. Furthermore, we utilize fuzzing to achieve practical TV. We generate a large number of JS functions using a fuzzer to trigger various optimization passes of TurboFan and validate their compilation using TurboTV. Lastly, we demonstrate TurboTV can also be used for cross-language TV. We show that TurboTV can validate the translation chain from LLVM IR to WebAssembly, to TurboFan IR collaborated with a TV tool for LLVM. We evaluated TurboTV on various sets of JS and LLVM programs. TurboTV effectively validated a large number of compilations of TurboFan with a low false positive rate and discovered new miscompilations in LLVM.

Thu 18 Apr

Displayed time zone: Lisbon change

11:00 - 12:30
Dependability and Formal methods 2Research Track / Software Engineering Education and Training / Demonstrations / Software Engineering in Practice at Glicínia Quartin
Chair(s): Jácome Cunha University of Porto & HASLab/INESC
11:00
15m
Talk
Enabling Runtime Verification of Causal Discovery Algorithms with Automated Conditional Independence Reasoning
Research Track
Pingchuan Ma HKUST, Zhenlan Ji The Hong Kong University of Science and Technology, Peisen Yao Zhejing University, Shuai Wang The Hong Kong University of Science and Technology, Kui Ren Zhejiang University
11:15
15m
Talk
Translation Validation for JIT Compiler in the V8 JavaScript Engine
Research Track
11:30
15m
Talk
Assessing the impact of hints in learning formal specification
Software Engineering Education and Training
Alcino Cunha University of Minho; INESC TEC, Nuno Macedo University of Porto; INESC TEC, José Creissac Campos University of Minho & HASLab/INESC TEC, Iara Margolis Center for Computer Graphics, Emanuel Sousa Center for Computer Graphics
11:45
15m
Talk
GWP-ASan: Sampling-Based Detection of Memory-Safety Bugs in Production
Software Engineering in Practice
12:00
15m
Talk
Dynamic Alert Suppression Policy for Noise Reduction in AIOps
Software Engineering in Practice
karan bhukar IBM Research, Harshit Kumar IBM Research, Ruchi Mahindru IBM Research, Rohan Arora IBM Research, Seema Nagar IBM Research, Pooja Aggarwal IBM Research, Amit Paradkar IBM Watson Research Center
12:15
7m
Talk
What Do You Mean by Memory? When Engineers Are Lost in the Maze of Complexity
Software Engineering in Practice
Gunnar Kudrjavets Amazon Web Services, USA, Aditya Kumar Google, Jeff Thomas Meta Platforms, Inc., Ayushi Rastogi University of Groningen, The Netherlands
DOI Pre-print
12:22
7m
Talk
SpotFlow: Tracking Method Calls and States at Runtime
Demonstrations
Pre-print Media Attached