This program is tentative and subject to change.

Wed 23 Oct 2024 16:20 - 16:40 at IBR West - Performance Analysis and Optimisation 2 Chair(s): Matthew Flatt

Even though heavily researched, a full formal model of the x86-64 instruction set is still not available. We present libLISA, a tool for automated discovery and analysis of the ISA of a CPU. This produces the most extensive formal x86-64 model to date, with over 118000 different instruction groups. The process requires as little human specification as possible: specifically, we do not rely on a human-written (dis)assembler to dictate which instructions are executable on a given CPU, or what their in- and outputs are. The generated model is CPU-specific: behavior that is “undefined” is synthesized for the current machine. Producing models for five different x86-64 machines, we mutually compare them, discover undocumented instructions, and generate instruction sequences that are CPU-specific. Experimental evaluation shows that we enumerate virtually all instructions within scope, that the instructions’ semantics are correct w.r.t. existing work, and that we improve existing work by exposing bugs in their handwritten models.

This program is tentative and subject to change.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
Performance Analysis and Optimisation 2OOPSLA 2024 at IBR West
Chair(s): Matthew Flatt University of Utah
16:00
20m
Talk
Jmvx: Fast Multi-threaded Multi-Version eXecution and Record-Replay for Managed Languages
OOPSLA 2024
David Schwartz University of Illinois at Chicago, Ankith Kowshik University of Illinois Chicago, Luís Pina University of Illinois at Chicago
16:20
20m
Talk
libLISA: Instruction Discovery and Analysis on x86-64
OOPSLA 2024
Jos Craaijo Open Universiteit, Freek Verbeek Open Universiteit & Virginia Tech, Binoy Ravindran Virginia Tech
16:40
20m
Talk
Extending the C/C++ Memory Model with Inline Assembly
OOPSLA 2024
Paulo Emílio de Vilhena Imperial College London, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Azalea Raad Imperial College London
17:00
20m
Talk
TorchQL: A Programming Framework for Integrity Constraints in Machine Learning
OOPSLA 2024
Aaditya Naik University of Pennsylvania, Adam Stein University of Pennsylvania, Yinjun Wu University of Pennsylvania, Mayur Naik University of Pennsylvania, Eric Wong
17:20
20m
Talk
Verification of Neural Networks' Global Robustness
OOPSLA 2024
Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion