References

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 http://www.oreilly.de/catalog/understandlk/index.html.
5. devicetree.org (2016): Devicetree Specification. http://www.devicetree.org/specifications-pdf.
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. http://www.acpi.info/downloads/acpispec50.pdf.
8. UEFI Forum (2016): UEFI Specification 2.6. http://www.uefi.org/sites/default/files/UEFI Spec 2_6.pdf http://www.uefi.org/specifications.
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 http://dl.acm.org/citation.cfm?id=2831090.2831106.
11. Intel Corporation (2009): Reducing Interrupt Latency Through the Use of Message Signaled Interrupts. Online. Accessed 2017-01-13. White Paper 321070. http://www.intel.co.za/content/dam/www/public/us/en/documents/white-papers/msg-signaled-interrupts-paper.pdf.
12. Intel Corporation (2009): Single-chip Cloud Computer. Online. Accessed 2017-01-09. http://www.intel.com/content/dam/www/public/us/en/documents/technology-briefs/intel-labs-single-chip-cloud-overview-paper.pdf.
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 http://dl.acm.org/citation.cfm?id=3026877.3026881.
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 http://dl.acm.org/citation.cfm?id=2831090.2831107.
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, www.ti.com/lit/ug/swpu235ab/swpu235ab.pdf.
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: eptcs@eptcs.org

For website issues: webmaster@eptcs.org