We show that the model, in violation of the design intention, does not support a compilation scheme to ARMv8 which is used in practice. We propose a correction, which also incorporates a previously proposed fix for a failure of the model to provide Sequential Consistency of Data-Race-Free programs (SC-DRF), an important correctness condition. We use model checking, in Alloy, to generate small counter-examples for these deficiencies, and investigate our correction. To accomplish this, we also develop a mixed-size extension to the existing ARMv8 axiomatic model.
Thu 18 Jun Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change
|05:00 - 05:20|
Conrad WattUniversity of Cambridge, UK, Christopher PulteUniversity of Cambridge, UK, Anton PodkopaevMPI-SWS, NRU HSE, JetBrains Research, Guillaume BarbierENS Rennes, France, Stephen DolanUniversity of Cambridge, UK, Shaked FlurGoogle, Jean Pichon-PharabodUniversity of Cambridge, UK, Shu-yu GuoBloomberg, USAPre-print
|05:20 - 05:40|
Sung-Hwan LeeSeoul National University, South Korea, Minki ChoSeoul National University, South Korea, Anton PodkopaevMPI-SWS, NRU HSE, JetBrains Research, Soham ChakrabortyIIT Delhi, India, Chung-Kil HurSeoul National University, South Korea, Ori LahavTel Aviv University, Israel, Viktor VafeiadisMPI-SWS, Germany
|05:40 - 06:00|