@Misc{ieee754-2008, key = "{IEEE}", title = "{ANSI/IEEE Std 754-2008}, {IEEE} standard for floating-point arithmetic", publisher = {"Institute of Electrical and Electronic Engineers"}, year = 2008 } @inproceedings{riscI-isca1981, title = {{RISC I}: {A} Reduced Instruction Set {VLSI} Computer}, author = {David A. Patterson and Carlo H. S\'{e}quin}, booktitle = {ISCA}, location = {Minneapolis, Minnesota, USA}, pages = {443-458}, year = {1981} } @InProceedings{Katevenis:1983, author = {Katevenis, Manolis G.H. and Sherburne,Jr., Robert W. and Patterson, David A. and S{\'e}quin, Carlo H.}, title = {The {RISC II} micro-architecture}, booktitle = {Proceedings VLSI 83 Conference}, year = 1983, month = {August}} @article{Katevenis:1984, author = {Katevenis, Manolis G.H. and Sherburne,Jr., Robert W. and Patterson, David A. and S{\'e}quin, Carlo H.}, title = {The {RISC II} micro-architecture}, journal = {Advances in VLSI and Computur Systems}, issue_date = {Fall 1984}, volume = {1}, number = {2}, month = October, year = {1984}, pages = {138--152}, publisher = {Computer Science Press, Inc.}, address = {New York, NY, USA}, } @inproceedings{Ungar:1984, author = {David Ungar and Ricki Blau and Peter Foley and Dain Samples and David Patterson}, title = {Architecture of {SOAR}: {Smalltalk} on a {RISC}}, booktitle = {ISCA}, address = {Ann Arbor, MI}, year = {1984}, pages = {188--197} } @Article{spur-jsscc1989, author = {David D. Lee and Shing I. Kong and Mark D. Hill and George S. Taylor and David A. Hodges and Randy H. Katz and David A. Patterson}, title = {A {VLSI} Chip Set for a Multiprocessor Workstation--{Part I}: An {RISC} Microprocessor with Coprocessor Interface and Support for Symbolic Processing}, journal = {IEEE JSSC}, year = 1989, volume = 24, number = 6, pages = {1688--1698}, month = {December}} @MastersThesis{waterman-ms, author = {Andrew Waterman}, title = {{Improving Energy Efficiency and Reducing Code Size with RISC-V Compressed}}, school = {University of California, Berkeley}, year = 2011, Number = {UCB/EECS-2011-63}, } @phdthesis{waterman-phd, Author = {Waterman, Andrew}, Title = {Design of the {RISC-V} Instruction Set Architecture}, School = {University of California, Berkeley}, Year = {2016}, Number = {UCB/EECS-2016-1}, } @TechReport{riscvtr, author = {Andrew Waterman and Yunsup Lee and David A. Patterson and Krste Asanovi\'{c}}, title = {The {RISC-V} Instruction Set Manual, {Volume I}: {Base} User-Level {ISA}}, institution = {EECS Department, University of California, Berkeley}, year = 2011, number = {UCB/EECS-2011-62}, month = {May}} @Book{kane:mips:1991, author = {G. Kane and J. Heinrich}, title = {MIPS RISC Architecture}, publisher = {Prentice Hall}, month = {September}, year = 1991, note = {ISBN 0135904722}, edition = {2nd} } @book{patterson:undergrad:2008, author = {D. A. Patterson and J. L. Hennessy}, title = {Computer Organization and Design: The Hardware/Software Interface}, edition = {4th}, publisher = {Morgan Kaufmann}, month = {November}, year = {2008}, note = {ISBN 0123744938} } @Book{sweetman:mips:2006, author = {D. Sweetman}, title = {See {MIPS} Run}, edition = {2nd}, publisher = {Morgan Kaufmann}, year = {2006}, month = {October}, note = {ISBN 0120884216} } @Misc{mips:arch:2010, author = {MIPS Technologies Inc.}, title = {{MIPS32} Architecture for Programmers}, year = {2010}, note = {\verb!https://www.imgtec.com/mips/architectures/mips32/!} } @Misc{sgi:mipspro:1997, author = {Silicon Graphics Inc.}, title = {{MIPSpro} 64-{B}it Porting and Translation Guide}, year = {1997}, note = {\verb!http://techpubs.sgi.com/!} } @Misc{openriscarch, author = {OpenCores}, title = {{OpenRISC} 1000 Architecture Manual, Architecture Version 1.0}, month = {December}, year = 2012} @ARTICLE{tremblay-vis-ieeemicro1996, author={Tremblay, M. and O'Connor, J.M. and Narayanan, V. and Liang He}, journal={IEEE Micro}, title={{VIS} speeds new media processing}, year={1996}, month=AUG, volume={16}, number={4}, pages={10 -20}, keywords={3D graphics environments;RISC-style instructions;UltraSparc;VIS;Visual Instruction Set;media processing;media-processing algorithms;computer graphics;instruction sets;reduced instruction set computing;}, ISSN={0272-1732},} @ARTICLE{lee-max-ieeemicro1996, author={Lee, R.B.}, journal={IEEE Micro}, title={Subword parallelism with {MAX-2}}, year={1996}, month=AUG, volume={16}, number={4}, pages={51 -59}, keywords={MAX-2;instruction extensions;media processing;parallel computation;subword parallelism;word-oriented general-purpose processor;instruction sets;multimedia computing;parallel processing;}, ISSN={0272-1732},} @ARTICLE{peleg-mmx-ieeemicro1996, author={Peleg, A. and Weiser, U.}, journal={IEEE Micro}, title={{MMX} technology extension to the {Intel} architecture}, year={1996}, month=AUG, volume={16}, number={4}, pages={42 -50}, keywords={Intel architecture;MMX;SIMD;communications;compatibility;multimedia;operating systems;microprocessor chips;parallel architectures;}, ISSN={0272-1732},} @ARTICLE{raman-sse-ieeemicro2000, author={Raman, S.K. and Pentkovski, V. and Keshava, J.}, journal={IEEE Micro}, title={Implementing streaming {SIMD} extensions on the {Pentium}-{III} processor }, year={2000}, month=JUL/AUG, volume={20}, number={4}, pages={47 -57}, keywords={Internet;Pentium III developers;demanding multimedia;die size constraints;streaming SIMD extensions;instruction sets;microprocessor chips;}, ISSN={0272-1732},} @misc{lomont-avx-irm2011, author={Chris Lomont}, title = {Introduction to {Intel Advanced Vector Extensions}}, howpublished = {Intel White Paper}, year = {2011}, } @ARTICLE{goodacre-armisa-computer2005, author={Goodacre, J. and Sloss, A.N.}, journal={Computer}, title={Parallelism and the {ARM} instruction set architecture}, year={2005}, month=JULY, volume={38}, number={7}, pages={ 42 - 50}, keywords={ ARM RISC processor; ARM chip design; ARM instruction set architecture; digital signal processor-like operations; exception handling; multiprocessing; reduced-instruction-set computing; subword parallelism; thread-level parallelism; variable execution time; instruction sets; microprocessor chips; parallel architectures; parallel programming; reduced instruction set computing;}, ISSN={0018-9162},} @ARTICLE{diefendorff-altivec-ieeemicro2000, author={Diefendorff, K. and Dubey, P.K. and Hochsprung, R. and Scale, H.}, journal={IEEE Micro}, title={{AltiVec} extension to {PowerPC} accelerates media processing}, year={2000}, month=MAR/APR, volume={20}, number={2}, pages={85 -95}, keywords={2D image processing;3D graphics;AltiVec extension;Apple G4;Hewlett-Packard added MAX;MDMX;MIPS architecture;MMX;Motorola's MPC 7400;PA-RISC architecture;PowerPC;PowerPC's AltiVec;SSE;Silicon Graphics;Sun enhanced Sparc;alias KNI;handwriting recognition;media mining;media processing;multimedia technologies;narrow/broadband signal processing;personal computing;digital signal processing chips;handwriting recognition;multimedia systems;parallel architectures;}, ISSN={0272-1732},} @misc{gwennap-mdmx-mpr1996, author={Linley Gwennap}, title={Digital, {MIPS} Add Multimedia Extensions}, howpublished = {Microprocessor Report}, year = {1996}, } @article{majc, author = {Tremblay, Marc and Chan, Jeffrey and Chaudhry, Shailender and Conigliaro, Andrew W. and Tse, Shing Sheung}, title = {The {MAJC} Architecture: {A} Synthesis of Parallelism and Scalability}, journal = {IEEE Micro}, issue_date = {November 2000}, volume = {20}, number = {6}, month = November, year = {2000}, pages = {12--25}, publisher = {IEEE Computer Society Press}, address = {Los Alamitos, CA, USA}, } @InProceedings{tx2, author = {John M. Frankovich and H. Philip Peterson}, title = {A functional description of the {Lincoln} {TX-2} computer}, booktitle = {Western Joint Computer Conference}, year = 1957, address = {Los Angeles, CA}, month = {February} } @TechReport{heil-tr1996, author = {Timothy H. Heil and James E. Smith}, title = {Selective Dual Path Execution}, institution = {University of Wisconsin - Madison}, year = 1996, month = {November}} @inproceedings{Klauser-1998, author = {Klauser, A. and Austin, T. and Grunwald, D. and Calder, B.}, title = {Dynamic Hammock Predication for Non-Predicated Instruction Set Architectures}, booktitle = {Proceedings of the 1998 International Conference on Parallel Architectures and Compilation Techniques}, series = {PACT '98}, year = {1998}, address = {Washington, DC, USA}, } @inproceedings{Kim-micro2005, author = {Kim, Hyesoon and Mutlu, Onur and Stark, Jared and Patt, Yale N.}, title = {Wish Branches: Combining Conditional Branching and Predication for Adaptive Predicated Execution}, booktitle = {Proceedings of the 38th annual IEEE/ACM International Symposium on Microarchitecture}, series = {MICRO 38}, year = {2005}, location = {Barcelona, Spain}, pages = {43--54}, } @INPROCEEDINGS{Gharachorloo90memoryconsistency, author = {Kourosh Gharachorloo and Daniel Lenoski and James Laudon and Phillip Gibbons and Anoop Gupta and John Hennessy}, title = {Memory Consistency and Event Ordering in Scalable Shared-Memory Multiprocessors}, booktitle = {In Proceedings of the 17th Annual International Symposium on Computer Architecture}, year = {1990}, pages = {15--26} } @inproceedings{Rajwar:2001:SLE, author = {Rajwar, Ravi and Goodman, James R.}, title = {Speculative lock elision: enabling highly concurrent multithreaded execution}, booktitle = {Proceedings of the 34th annual ACM/IEEE International Symposium on Microarchitecture}, series = {MICRO 34}, year = {2001}, location = {Austin, Texas}, pages = {294--305}, publisher = {IEEE Computer Society}, } @Misc{sparcieee1994, title = {{IEEE} Standard for a 32-bit microprocessor}, howpublished = {IEEE Std. 1754-1994}, year = 1994} @Book{parisckane1995, author = {Gerry Kane}, title = {PA-RISC 2.0 Architecture}, publisher = {Prentice Hall}, year = 1995, month = {December}, note = {ISBN 978-0131827349}} @article{ibmpower7, title={{IBM} {POWER7} multicore server processor}, author={Sinharoy, Balaram and Kalla, R. and Starke, W. J. and Le, H. Q. and Cargnoni, R. and Van Norstrand, J. A. and Ronchetti, B. J. and Stuecheli, J. and Leenstra, J. and Guthrie, G. L. and Nguyen, D. Q. and Blaner, B. and Marino, C. F. and Retter, E. and Williams, P.}, journal={IBM Journal of Research and Development}, volume={55}, number={3}, pages={1--1}, year={2011}, publisher={IBM} } @article{virtio, author = {Russell, Rusty}, title = {Virtio: {Towards} a De-facto Standard for Virtual {I/O} Devices}, journal = {SIGOPS Oper. Syst. Rev.}, issue_date = {July 2008}, volume = {42}, number = {5}, month = jul, year = {2008}, issn = {0163-5980}, pages = {95--103}, numpages = {9}, publisher = {ACM}, address = {New York, NY, USA}, } @ARTICLE{goldbergvm, author={Goldberg, Robert P.}, journal={Computer}, title={Survey of virtual machine research}, year={1974}, month={June}, volume={7}, number={6}, pages={34-45} } @Manual{alphapalcode, title = {{PALcode} for {Alpha} microprocessors: System Design Guide}, organization = {Digital Equipment Corporation}, address = {Maynard, Massachusetts}, note = {EC-QFGLC-TE}, month = {May}, year = 1996} @article{transparent-superpages, author = {Navarro, Juan and Iyer, Sitaram and Druschel, Peter and Cox, Alan}, title = {Practical, Transparent Operating System Support for Superpages}, journal = {SIGOPS Oper. Syst. Rev.}, issue_date = {Winter 2002}, volume = {36}, number = {SI}, month = dec, year = {2002}, issn = {0163-5980}, pages = {89--104}, numpages = {16}, url = {https://doi.org/10.1145/844128.844138}, doi = {10.1145/844128.844138}, acmid = {844138}, publisher = {ACM}, address = {New York, NY, USA}, } @Book{stretch, editor = {Werner Buchholz}, title = {Planning a computer system: {Project} {Stretch}}, publisher = {McGraw-Hill Book Company}, year = 1962} @Article{ibm360, author = {G. M. Amdahl and G. A. Blaauw and F. P. Brooks, Jr.}, title = {Architecture of the {IBM} {System/360}}, journal = {IBM Journal of R. \& D.}, year = 1964, volume = 8, number = 2 } @inproceedings{cdc6600, author = {Thornton, James E.}, title = {Parallel Operation in the {Control Data 6600}}, booktitle = {Proceedings of the October 27-29, 1964, Fall Joint Computer Conference, Part II: Very High Speed Computer Systems}, series = {AFIPS '64 (Fall, part II)}, year = {1965}, location = {San Francisco, California}, pages = {33--40} } @InProceedings{jtseng:sbbci, author = {J. Tseng and K. Asanovi\'c}, title = {Energy-Efficient Register Access}, booktitle = {Proc. of the 13th Symposium on Integrated Circuits and Systems Design}, address = {Manaus, Brazil}, month = {September}, year = 2000, pages = "377--384" } @TechReport{riscvtr2, author = {Andrew Waterman and Yunsup Lee and David A. Patterson and Krste Asanovi\'{c}}, title = {The {RISC-V} Instruction Set Manual, {Volume I}: {Base} User-Level {ISA} Version 2.0}, institution = {EECS Department, University of California, Berkeley}, year = 2014, number = {UCB/EECS-2014-54}, month = {May}} @Article{ibm370varch, author = {W. Buchholz}, title = "{The IBM System/370 vector architecture}", journal = {IBM Systems Journal}, year = 1986, volume = 25, number = 1, pages = {51--62} } @PhdThesis{krstephd, author = {Krste Asanovi\'c}, title = {Vector Microprocessors}, school = {University of California at Berkeley}, year = 1998, month = {May}, note = {Available as techreport UCB/CSD-98-1014} } @InProceedings{vp200, author = "Kenichi Miura and Keiichiro Uchida", title = "{FACOM Vector Processor System: VP-100/VP-200}", editor = "Kawalik", volume = "F7", booktitle = "Proceedings of NATO Advanced Research Workshop on High Speed Computing", year = 1984, publisher = "Springer-Verlag", note = "Also in: IEEE Tutorial Supercomputers: Design and Applications. Kai Hwang(editor), pp59-73" } @Manual{crayx1asm, title = {Cray Assembly Language {(CAL)} for {Cray} {X1} Systems Reference Manual}, organization = {Cray Inc.}, edition = {1.1}, month = {June}, year = 2003} } @misc{riscv-elf-psabi, title = {{RISC-V ELF psABI Specification}}, howpublished = {\url{https://github.com/riscv/riscv-elf-psabi-doc/}} } @misc{riscv-asm-manual, title = {{RISC-V Assembly Programmer's Manual}}, howpublished = {\url{https://github.com/riscv/riscv-asm-manual}} } @inproceedings{lithe-pan-hotpar09, author = {Heidi Pan and Benjamin Hindman and Krste Asanovi\'c}, title = {{Lithe}: Enabling Efficient Composition of Parallel Libraries}, booktitle = {Proceedings of the 1st USENIX Workshop on Hot Topics in Parallelism (HotPar~'09)}, month = {March}, year = {2009}, address = {Berkeley, CA}} @inproceedings{lithe-pan-pldi10, author = {Heidi Pan and Benjamin Hindman and Krste Asanovi\'c}, title = {Composing Parallel Software Efficiently with {Lithe}}, booktitle = {31st Conference on Programming Language Design and Implementation}, month = {June}, year = {2010}, address = {Toronto, Canada}} @article{roux:hal-01091186, TITLE = {{Innocuous Double Rounding of Basic Arithmetic Operations}}, AUTHOR = {Roux, Pierre}, URL = {https://hal.archives-ouvertes.fr/hal-01091186}, JOURNAL = {{Journal of Formalized Reasoning}}, PUBLISHER = {{ASDD-AlmaDL}}, VOLUME = {7}, NUMBER = {1}, PAGES = {131-142}, YEAR = {2014}, MONTH = Nov, DOI = {10.6092/issn.1972-5787/4359}, KEYWORDS = {Coq ; double rounding ; floating-point arithmetic}, PDF = {https://hal.archives-ouvertes.fr/hal-01091186/file/submission.pdf}, HAL_ID = {hal-01091186}, HAL_VERSION = {v1}, }