ARMv8-A system semantics: instruction fetch in relaxed architectures | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		ARMv8-A system semantics: instruction fetch in relaxed architectures (cam.ac.uk)
		65 points by matt_d on March 2, 2020 \| hide \| past \| favorite \| 1 comment

monocasa on March 2, 2020 [–]

Nice! Most of the formal models of architectures I've seen ignore the whole memory hierarchy thing. Even places you might expect, like the model used in sel4's proof.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact