Errata
These are the errors and mistakes in my publications which are known to me.
This does not include works whose technical content have been superseded where limitations were already known, but rather
errors in statements or proofs, and typographical mistakes.
If you find any errors other than those listed here, feel free to contact me.
Precise exceptions in relaxed architectures:
- p6. figure 7 (right). MP+dmb.sy+ctrlelr: in the listing, in T1 handler, instruction 5 should read
MSR ELR_EL1,X5. This was just a transcription error in the paper; the isla and system-litmus-harness versions have the correct code.
Arm systems semantics (PhD thesis):
- p7. Max is Max Aalling. Sorry Max!
- p7. I also wish to express gratitude to Warren A. Hunt, Anna Slobodova, Rob Sumners, and Shilpi Goel, for their hospitality during my visit to Austin and Centaur Technology.
- p21. in the last sentence: 'discussed' should be 'variously discussed'; 'and' should be 'and/or'. For the avoidance of doubt, there is no intent to imply contribution to or approval of this work by those mentioned.
- p204. figure 11.10 (right). MP+dmb.sy+ctrlelr: in the listing, in T1 handler, instruction 5 should read
MSR ELR_EL1,X5. This was just a transcription error in the paper; the isla and system-litmus-harness versions have the correct code.
ARMv8-A system semantics: instruction fetch in relaxed
architectures:
- p10. "dl_open" should read "dlopen"
- p25. "Cches" should read "Caches"
- p32. "(execute" should read "execute"
- In the extended version, in Appendix B.5 ('Model Transitions'), for the following transitions:
- "Fetch instruction"
- "Fetch instruction (unpredictable)"
- "Fetch instruction (B.cond)"
Their text should read "can be satisfied from the instruction cache" rather than "from the memory and abstract data cache", and "Fetch instruction"'s condition should say "the write-slices ws have the 4-byte footprint of the entry and can be constructed from a write in the instruction cache".