HMC
Michalis Kokologiannakis, Viktor Vafeiadis
Abstract
Stateless Model Checking (SMC) is an effective technique for verifying safety properties of a concurrent program by systematically exploring all of its executions. While SMC has been extended to handle hardware memory models like x86-TSO, it does not adequately support models that allow load buffering behaviours, such as the POWER, ARMv7, ARMv8, and RISC-V models. Existing SMC tools either do not consider such behaviours in the name of efficiency, or do not scale so well due to the extra complexity induced by these behaviours.
Topics & Concepts
Computer scienceStateless protocolx86Model checkingParallel computingProgramming languageOperating systemDistributed computingEmbedded systemSoftwareState (computer science)Formal Methods in VerificationSoftware Testing and Debugging TechniquesReal-Time Systems Scheduling