The HotSpot Java Virtual Machine is one of the most popular runtime environments for numerous programming languages. A large portion of web services and other software depend on HotSpot’s correctness and safety. However, various bugs and exploits have been discovered over HotSpot’s three decades of development. This raises the question of how we can effectively detect and prevent bugs within HotSpot. In this thesis, we focus on the verification of an important component of HotSpot, the C2 compiler, which carries out the heaviest optimizations. Traditional ways of testing compilers include unit tests, integration tests, fuzzing, and formal verification. While these methods have been widely used in practice, they suffer from the problem of either being too costly to exhaust all search space or being too difficult to scale up in the size of the compiler. Translation validation is an emerging approach that takes a middle ground between these methods and uses formal techniques to fully verify individual compilations over all possible inputs. Translation validation has been successfully applied to a number of compilers, including JavaScript’s V8 engine and LLVM, and has been able to detect hundreds of new bugs within them. This thesis explores applying translation validation to the HotSpot C2 compiler by designing, implementing, and evaluating a verification tool. Our evaluation results show that our tool is capable of detecting bugs in HotSpot, and the verification time of our tool has good scalability in the size of randomly generated programs.

Den virtuella Java-maskinen HotSpot är en av de mest populära körtidsmiljöerna för flera olika programmeringsspråk. En stor del av webbtjänster och annan mjukvara beror på HotSpots korrekthet och säkerhet. Olika buggar och exploateringar har dock uppdagats under HotSpots tre årtionden av utveckling. Detta väcker frågan om hur vi effektivt kan upptäcka och förebygga buggar i HotSpot. Det här arbetet fokuserar på verifieringen av en viktig komponent i HotSpot, C2-kompilatorn, som utför de tyngsta optimeringarna. Traditionella sätt att testa kompilatorer på inkluderar enhetstester, integrationstester, fuzzing och formell verifiering. Även om dessa metoder har använts i stor utsträckning i praktiken lider de av problemet att antingen vara för kostsamma för att uttömma allt sökutrymme, eller att vara för svåra att skala upp i kompilatorns storlek. Översättningsvalidering är en framväxande metod som tar en medelväg mellan dessa metoder och använder formella tekniker för att fullständigt verifiera individuella kompileringar över alla möjliga indata. Översättningsvalidering har tillämpats framgångsrikt på ett antal kompilatorer, inklusive JavaScripts V8-motor och LLVM, och har kunnat upptäcka hundratals nya buggar i dem. Det här arbetet utforskar tillämpningen av översättningsvalidering för C2-kompilatorn i HotSpot genom att designa, implementera och utvärdera ett verifieringsverktyg. Våra utvärderingsresultat visar att vårt verktyg kan upptäcka buggar i HotSpot, och att verifieringstiden för vårt verktyg har god skalbarhet i storleken av slumpmässigt genererade program.