1. Jade Alglave (2012): A Formal Hierarchy of Weak Memory Models. Form. Methods Syst. Des. 41(2), pp. 178–210, doi:10.1007/s10703-012-0161-5.
  2. Jade Alglave, Luc Maranget, Susmit Sarkar & Peter Sewell (2010): Fences in Weak Memory Models. In: CAV'10, Edinburgh, UK, pp. 258–272, doi:10.1007/978-3-642-14295-6_25.
  3. John Baldwin (2008): PCI Interrupts for x86 Machines under FreeBSD. In: Proceedings of the BSDCan Conference, pp. 1–22.
  4. Daniel P. Bovet & Marco Cesati (2005): Understanding the Linux Kernel - from I/O ports to process management: covers version 2.6 (3. ed.), chapter 4.6. O'Reilly. Available at
  5. (2016): Devicetree Specification.
  6. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon & Peter Sewell (2016): Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA. In: POPL '16, St. Petersburg, FL, USA, pp. 608–621, doi:10.1145/2837614.2837615.
  7. UEFI Forum (2011): ACPI 5.0 Specification.
  8. UEFI Forum (2016): UEFI Specification 2.6. Spec 2_6.pdf
  9. Malay K. Ganai, Aarti Gupta & Pranav Ashar (2005): Verification of Embedded Memory Systems Using Efficient Memory Modeling. In: DATE '05, pp. 1096–1101, doi:10.1109/DATE.2005.325.
  10. Simon Gerber, Gerd Zellweger, Reto Achermann, Kornilios Kourtis, Timothy Roscoe & Dejan Milojicic (2015): Not Your Parents' Physical Address Space. In: HOTOS'15, Switzerland, pp. 16–16. Available at
  11. Intel Corporation (2009): Reducing Interrupt Latency Through the Use of Message Signaled Interrupts. Online. Accessed 2017-01-13. White Paper 321070.
  12. Intel Corporation (2009): Single-chip Cloud Computer. Online. Accessed 2017-01-09.
  13. Intel Corporation (2016): Intel Virtualization Technology for Directed I/O, revision 2.4 edition.
  14. Stefan Kaestle, Reto Achermann, Roni Haecki, Moritz Hoffmann, Sabela Ramos & Timothy Roscoe (2016): Machine-aware Atomic Broadcast Trees for Multicores. In: OSDI'16, Savannah, GA, USA, pp. 33–48. Available at
  15. Simon Peter, Adrian Schüpbach, Dominik Menzi & Timothy Roscoe (2011): Early experience with the Barrelfish OS and the Single-Chip Cloud Computer. In: MARC'11. KIT Scientific Reports, pp. 17–17. Available at
  16. Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave & Derek Williams (2012): Synchronising C/C++ and POWER. In: PLDI'12. ACM, New York, NY, USA, pp. 311–322, doi:10.1145/2254064.2254102.
  17. Adrian Schüpbach, Andrew Baumann, Timothy Roscoe & Simon Peter (2011): A Declarative Language Approach to Device Configuration. In: ASPLOS XVI, Newport Beach, California, USA, pp. 119–132, doi:10.1145/1950365.1950382.
  18. Texas Instruments (2014): OMAP44xx Multimedia Device Technical Reference Manual. Version AB,
  19. Miroslav N. Velev (2001): Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. In: TACAS 2001, pp. 252–267, doi:10.1007/3-540-45319-9_18.
  20. Foivos S. Zakkak & Polyvios Pratikakis (2016): DiSquawk: 512 Cores, 512 Memories, 1 JVM. In: PPPJ '16, Lugano, Switzerland, pp. 2:1–2:12, doi:10.1145/2972206.2972212.

Comments and questions to:
For website issues: